From 9e5d2e761c48c5a8d3abf537bc34e0d08f247778 Mon Sep 17 00:00:00 2001 From: Jan Baudisch Date: Tue, 8 Oct 2024 18:44:09 +0200 Subject: [PATCH] feat: add projected compilation --- .github/workflows/CI.yaml | 2 +- 3rdParty/GPMC/CMakeLists.txt | 7 +- 3rdParty/GPMC/core/Component.h | 10 +- 3rdParty/GPMC/core/Counter.cc | 22 +- 3rdParty/GPMC/utils/Options.h | 6 +- 3rdParty/glucose-3.0/CMakeLists.txt | 2 +- 3rdParty/glucose-3.0/core/Main.cc | 5 - 3rdParty/glucose-3.0/simp/Main.cc | 5 - 3rdParty/glucose-3.0/utils/System.h | 4 - CMakeLists.txt | 15 +- cmake/FindGPMC.cmake | 54 + flake.lock | 6 +- flake.nix | 89 +- nix/cryptominisat.nix | 2 + nix/d4.nix | 14 + nix/glucose.nix | 29 + nix/gpmc.nix | 10 +- src/caching/CacheListLRU.hpp | 420 ++++++++ src/config/Config.cpp | 10 +- src/config/Config.hpp | 10 +- src/config/ConfigConverter.cpp | 10 +- src/heuristics/ProjBackupHeuristic.cpp | 29 + src/heuristics/ProjBackupHeuristic.hpp | 16 + src/heuristics/ScoringMethod.cpp | 72 +- src/heuristics/ScoringMethod.hpp | 17 +- .../cnf/ProjBackupHeuristicComponents.cpp | 143 +++ .../cnf/ProjBackupHeuristicComponents.hpp | 34 + .../cnf/ProjBackupHeuristicHypergraph.cpp | 116 +++ .../cnf/ProjBackupHeuristicHypergraph.hpp | 43 + .../HyperGraphExtractorDualProj.cpp | 175 ++++ .../HyperGraphExtractorDualProj.hpp | 49 + src/methods/CountingOperation.hpp | 304 +++++- src/methods/MethodManager.cpp | 14 + src/methods/ProjDpllStyleMethod.hpp | 704 +++++++++++++ src/option.dsc | 10 +- src/preprocs/PreprocManager.cpp | 15 +- src/preprocs/PreprocManager.hpp | 3 +- src/preprocs/cnf/PreprocGPMC.cpp | 61 ++ src/preprocs/cnf/PreprocGPMC.hpp | 35 + src/preprocs/cnf/PreprocProj.cpp | 142 +++ src/preprocs/cnf/PreprocProj.hpp | 25 + src/preprocs/cnf/util/PreprocGPMC.cpp | 946 ++++++++++++++++++ src/preprocs/cnf/util/PreprocGPMC.hpp | 154 +++ src/preprocs/cnf/util/TestSolver.cpp | 405 ++++++++ src/preprocs/cnf/util/TestSolver.hpp | 114 +++ src/preprocs/cnf/util/lib_sharpsat_td/LICENSE | 27 + .../cnf/util/lib_sharpsat_td/README.txt | 9 + .../cnf/util/lib_sharpsat_td/bitset.hpp | 304 ++++++ .../cnf/util/lib_sharpsat_td/subsumer.cpp | 197 ++++ .../cnf/util/lib_sharpsat_td/subsumer.hpp | 35 + .../cnf/util/lib_sharpsat_td/utils.hpp | 278 +++++ src/problem/ProblemManager.hpp | 13 + src/problem/cnf/ParserDimacs.cpp | 29 +- src/problem/cnf/ProblemManagerCnf.cpp | 97 +- src/problem/cnf/ProblemManagerCnf.hpp | 16 +- src/problem/cnf/ProblemManagerGPMC.hpp | 34 + src/solvers/WrapperSolver.hpp | 9 +- src/solvers/cnf/WrapperMinisat.cpp | 159 ++- src/solvers/cnf/WrapperMinisat.hpp | 8 +- src/specs/SpecManager.cpp | 16 +- src/specs/SpecManager.hpp | 34 +- src/specs/cnf/SpecManagerCnf.cpp | 187 +++- src/specs/cnf/SpecManagerCnf.hpp | 53 +- src/specs/cnf/SpecManagerCnfDyn.cpp | 92 +- src/specs/cnf/SpecManagerCnfDyn.hpp | 3 +- src/utils/IDIDFunc.hpp | 35 + src/utils/Proj.hpp | 15 + src/utils/UnionFind.hpp | 36 + 68 files changed, 5768 insertions(+), 276 deletions(-) create mode 100644 cmake/FindGPMC.cmake create mode 100644 nix/glucose.nix create mode 100644 src/caching/CacheListLRU.hpp create mode 100644 src/heuristics/ProjBackupHeuristic.cpp create mode 100644 src/heuristics/ProjBackupHeuristic.hpp create mode 100644 src/heuristics/cnf/ProjBackupHeuristicComponents.cpp create mode 100644 src/heuristics/cnf/ProjBackupHeuristicComponents.hpp create mode 100644 src/heuristics/cnf/ProjBackupHeuristicHypergraph.cpp create mode 100644 src/heuristics/cnf/ProjBackupHeuristicHypergraph.hpp create mode 100644 src/hyperGraph/HyperGraphExtractorDualProj.cpp create mode 100644 src/hyperGraph/HyperGraphExtractorDualProj.hpp create mode 100644 src/methods/ProjDpllStyleMethod.hpp create mode 100644 src/preprocs/cnf/PreprocGPMC.cpp create mode 100644 src/preprocs/cnf/PreprocGPMC.hpp create mode 100644 src/preprocs/cnf/PreprocProj.cpp create mode 100644 src/preprocs/cnf/PreprocProj.hpp create mode 100644 src/preprocs/cnf/util/PreprocGPMC.cpp create mode 100644 src/preprocs/cnf/util/PreprocGPMC.hpp create mode 100644 src/preprocs/cnf/util/TestSolver.cpp create mode 100644 src/preprocs/cnf/util/TestSolver.hpp create mode 100644 src/preprocs/cnf/util/lib_sharpsat_td/LICENSE create mode 100644 src/preprocs/cnf/util/lib_sharpsat_td/README.txt create mode 100644 src/preprocs/cnf/util/lib_sharpsat_td/bitset.hpp create mode 100644 src/preprocs/cnf/util/lib_sharpsat_td/subsumer.cpp create mode 100644 src/preprocs/cnf/util/lib_sharpsat_td/subsumer.hpp create mode 100644 src/preprocs/cnf/util/lib_sharpsat_td/utils.hpp create mode 100644 src/problem/cnf/ProblemManagerGPMC.hpp create mode 100644 src/utils/IDIDFunc.hpp create mode 100644 src/utils/Proj.hpp create mode 100644 src/utils/UnionFind.hpp diff --git a/.github/workflows/CI.yaml b/.github/workflows/CI.yaml index 69cefa62..e9cbc2ad 100644 --- a/.github/workflows/CI.yaml +++ b/.github/workflows/CI.yaml @@ -18,7 +18,7 @@ jobs: - double: x86_64-linux system: x86_64-linux runner: ubuntu-24.04 - flake: bundled + flake: d4 interpreter: /lib64/ld-linux-x86-64.so.2 - double: aarch64-darwin system: aarch64-darwin diff --git a/3rdParty/GPMC/CMakeLists.txt b/3rdParty/GPMC/CMakeLists.txt index da99ceb5..35373d46 100755 --- a/3rdParty/GPMC/CMakeLists.txt +++ b/3rdParty/GPMC/CMakeLists.txt @@ -21,11 +21,12 @@ add_subdirectory(flow-cutter-pace17) add_library(gpmc core/ComponentCache.cc core/ComponentManager.cc - core/Counter.cc core/Config.cc + core/Counter.cc + core/gpmc.cpp core/Instance.cc + core/Solver.cc ddnnf/DecisionTree.cc - core/Solver.cc utils/Options.cc utils/System.cc preprocessor/Preprocessor.cc @@ -33,8 +34,6 @@ add_library(gpmc preprocessor/lib_sharpsat_td/subsumer.cpp preprocessor/TreeDecomposition.cc preprocessor/IFlowCutter.cc - core/gpmc.cpp - core/Solver.h ) set_target_properties(gpmc PROPERTIES PUBLIC_HEADER include/gpmc.hpp) diff --git a/3rdParty/GPMC/core/Component.h b/3rdParty/GPMC/core/Component.h index e31bb540..8ab7e4eb 100644 --- a/3rdParty/GPMC/core/Component.h +++ b/3rdParty/GPMC/core/Component.h @@ -493,9 +493,9 @@ class ComponentCache { inline void cleanAllDescendantsOf(CacheEntryID id); void printStats() const { - printf("c o Cache lookup = %"PRIu64"\n", num_cache_look_ups_); - printf("c o Cache hit = %"PRIu64"\n", num_cache_hits_); - printf("c o Cache reduce = %"PRIu64"\n", num_cache_reduce_); + printf("c o Cache lookup = %" PRIu64"\n", num_cache_look_ups_); + printf("c o Cache hit = %" PRIu64"\n", num_cache_hits_); + printf("c o Cache reduce = %" PRIu64"\n", num_cache_reduce_); } // --- Added by k-hasimt --- END @@ -666,8 +666,8 @@ class ComponentManager { void printDimacs(const vec& clauses, const ClauseAllocator& ca, const vec& assign); void printStats() const { - printf("c o Components = %"PRIu64"\n", components); - printf("c o Split = %"PRIu64"\n", num_try_split); + printf("c o Components = %" PRIu64"\n", components); + printf("c o Split = %" PRIu64"\n", num_try_split); cache_.printStats(); } diff --git a/3rdParty/GPMC/core/Counter.cc b/3rdParty/GPMC/core/Counter.cc index e22c41cb..7fe31ef9 100644 --- a/3rdParty/GPMC/core/Counter.cc +++ b/3rdParty/GPMC/core/Counter.cc @@ -856,19 +856,19 @@ void Counter::printStats() const if(verbosity_c) { if(progress == COMPLETED || progress == FAILED) { printf("c o [Statistics]\n"); - printf("c o conflicts = %-11"PRIu64" (count %"PRIu64", sat %"PRIu64")\n", conflicts, conflicts-conflicts_sg, conflicts_sg); - printf("c o decisions = %-11"PRIu64" (count %"PRIu64", sat %"PRIu64")\n", decisions, decisions-decisions_sg, decisions_sg); - printf("c o propagations = %-11"PRIu64" (count %"PRIu64", sat %"PRIu64")\n", propagations, propagations-propagations_sg, propagations_sg); - printf("c o simp dbs = %-11"PRIu64" (%.3f s)\n", simp_dbs, simplify_time); - printf("c o reduce dbs = %-11"PRIu64"\n", nbReduceDB); - printf("c o learnts (uni/bin/lbd2)= %"PRIu64"/%"PRIu64"/%"PRIu64"\n", nbUn, nbBin, nbDL2); - printf("c o last learnts = %-11d (%"PRIu64" learnts removed, %4.2f%%)\n", learnts.size(), nbRemovedClauses, nbRemovedClauses * 100 / (double)conflicts); + printf("c o conflicts = %-11" PRIu64" (count %" PRIu64", sat %" PRIu64")\n", conflicts, conflicts-conflicts_sg, conflicts_sg); + printf("c o decisions = %-11" PRIu64" (count %" PRIu64", sat %" PRIu64")\n", decisions, decisions-decisions_sg, decisions_sg); + printf("c o propagations = %-11" PRIu64" (count %" PRIu64", sat %" PRIu64")\n", propagations, propagations-propagations_sg, propagations_sg); + printf("c o simp dbs = %-11" PRIu64" (%.3f s)\n", simp_dbs, simplify_time); + printf("c o reduce dbs = %-11" PRIu64"\n", nbReduceDB); + printf("c o learnts (uni/bin/lbd2)= %" PRIu64"/%" PRIu64"/%" PRIu64"\n", nbUn, nbBin, nbDL2); + printf("c o last learnts = %-11d (%" PRIu64" learnts removed, %4.2f%%)\n", learnts.size(), nbRemovedClauses, nbRemovedClauses * 100 / (double)conflicts); printStatsOfCM(); - printf("c o isolated_pvars = %"PRIu64"\n", nIsoPVars()); - printf("c o SAT calls = %-11"PRIu64" (SAT %"PRIu64", UNSAT %"PRIu64")\n", solves, sats, solves-sats); - printf("c o SAT starts = %"PRIu64"\n", starts); - printf("c o backjumps = %-11"PRIu64" (sp %"PRIu64") [init %s / final %s]\n", nbackjumps+nbackjumps_sp, nbackjumps_sp, config.backjump ? "on" : "off", on_bj ? "on" : "off"); + printf("c o isolated_pvars = %" PRIu64"\n", nIsoPVars()); + printf("c o SAT calls = %-11" PRIu64" (SAT %" PRIu64", UNSAT %" PRIu64")\n", solves, sats, solves-sats); + printf("c o SAT starts = %" PRIu64"\n", starts); + printf("c o backjumps = %-11" PRIu64" (sp %" PRIu64") [init %s / final %s]\n", nbackjumps+nbackjumps_sp, nbackjumps_sp, config.backjump ? "on" : "off", on_bj ? "on" : "off"); printf("c o\n"); } if(config.ddnnf) { diff --git a/3rdParty/GPMC/utils/Options.h b/3rdParty/GPMC/utils/Options.h index a89f94ba..f4459767 100644 --- a/3rdParty/GPMC/utils/Options.h +++ b/3rdParty/GPMC/utils/Options.h @@ -282,15 +282,15 @@ class Int64Option : public Option if (range.begin == INT64_MIN) fprintf(stderr, "imin"); else - fprintf(stderr, "%4"PRIi64, range.begin); + fprintf(stderr, "%4" PRIi64, range.begin); fprintf(stderr, " .. "); if (range.end == INT64_MAX) fprintf(stderr, "imax"); else - fprintf(stderr, "%4"PRIi64, range.end); + fprintf(stderr, "%4" PRIi64, range.end); - fprintf(stderr, "] (default: %"PRIi64")\n", value); + fprintf(stderr, "] (default: %" PRIi64")\n", value); if (verbose){ fprintf(stderr, "\n %s\n", description); fprintf(stderr, "\n"); diff --git a/3rdParty/glucose-3.0/CMakeLists.txt b/3rdParty/glucose-3.0/CMakeLists.txt index fc9d3828..e1d2ed49 100644 --- a/3rdParty/glucose-3.0/CMakeLists.txt +++ b/3rdParty/glucose-3.0/CMakeLists.txt @@ -56,6 +56,6 @@ set_target_properties(binary PROPERTIES OUTPUT_NAME glucose) target_link_libraries(binary glucose) install( - TARGETS glucose + TARGETS glucose binary FILE_SET HEADERS DESTINATION include/glucose ) diff --git a/3rdParty/glucose-3.0/core/Main.cc b/3rdParty/glucose-3.0/core/Main.cc index 3aece05c..dbe713e2 100644 --- a/3rdParty/glucose-3.0/core/Main.cc +++ b/3rdParty/glucose-3.0/core/Main.cc @@ -94,11 +94,6 @@ int main(int argc, char** argv) setUsageHelp("c USAGE: %s [options] \n\n where input may be either in plain or gzipped DIMACS.\n"); // printf("This is MiniSat 2.0 beta\n"); -#if defined(__linux__) - fpu_control_t oldcw, newcw; - _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw); - printf("c WARNING: for repeatability, setting FPU to use double precision\n"); -#endif // Extra options: // IntOption verb ("MAIN", "verb", "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2)); diff --git a/3rdParty/glucose-3.0/simp/Main.cc b/3rdParty/glucose-3.0/simp/Main.cc index 829f4cfe..02586f00 100644 --- a/3rdParty/glucose-3.0/simp/Main.cc +++ b/3rdParty/glucose-3.0/simp/Main.cc @@ -96,11 +96,6 @@ int main(int argc, char** argv) setUsageHelp("c USAGE: %s [options] \n\n where input may be either in plain or gzipped DIMACS.\n"); -#if defined(__linux__) - fpu_control_t oldcw, newcw; - _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw); - printf("WARNING: for repeatability, setting FPU to use double precision\n"); -#endif // Extra options: // IntOption verb ("MAIN", "verb", "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2)); diff --git a/3rdParty/glucose-3.0/utils/System.h b/3rdParty/glucose-3.0/utils/System.h index 47880705..bbf324fb 100644 --- a/3rdParty/glucose-3.0/utils/System.h +++ b/3rdParty/glucose-3.0/utils/System.h @@ -21,10 +21,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Glucose_System_h #define Glucose_System_h -#if defined(__linux__) -#include -#endif - #include "mtl/IntTypes.h" //------------------------------------------------------------------------------------------------- diff --git a/CMakeLists.txt b/CMakeLists.txt index 00083e83..792a657e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -18,6 +18,7 @@ if(NOT BUILD_SHARED_LIBS) set(GMP_USE_STATIC_LIBS ON) set(Boost_USE_STATIC_LIBS ON) set(MtKaHyPar_USE_STATIC_LIBS ON) + set(GPMC_USE_STATIC_LIBS ON) set(glucose_USE_STATIC_LIBS ON) endif() @@ -25,12 +26,8 @@ find_package(GMP REQUIRED) find_package(Boost REQUIRED COMPONENTS program_options) find_package(MtKaHyPar REQUIRED) find_package(arjun REQUIRED) - -# glucose is only needed when requested, which it is not by default. -if(USE_GLUCOSE) - find_package(glucose REQUIRED) - include_directories(${glucose_INCLUDE_DIRS}) -endif() +find_package(GPMC REQUIRED) +find_package(glucose REQUIRED) include_directories(${CMAKE_CURRENT_SOURCE_DIR}) include_directories(${CMAKE_CURRENT_SOURCE_DIR}/3rdParty/glucose-3.0) @@ -39,6 +36,8 @@ include_directories(${GMPXX_INCLUDE_DIRS}) include_directories(${Boost_INCLUDE_DIRS}) include_directories(${MtKaHyPar_INCLUDE_DIR}) include_directories(${arjun_INCLUDE_DIR}) +include_directories(${GMPC_INCLUDE_DIR}) +include_directories(${glucose_INCLUDE_DIRS}) add_library(caching OBJECT src/caching/BucketAllocator.cpp @@ -102,7 +101,9 @@ add_library(partitioner OBJECT ) add_library(preprocs OBJECT + src/preprocs/cnf/util/lib_sharpsat_td/subsumer.cpp src/preprocs/cnf/util/PreprocGPMC.cpp + src/preprocs/cnf/util/TestSolver.cpp src/preprocs/cnf/PreprocBackboneCnf.cpp src/preprocs/cnf/PreprocBasicCnf.cpp src/preprocs/cnf/PreprocGPMC.cpp @@ -154,7 +155,7 @@ add_library(core STATIC $ ) -target_link_libraries(core GMP::GMPXX GMP::GMP MtKaHyPar::MtKaHyPar arjun) +target_link_libraries(core MtKaHyPar::MtKaHyPar GPMC::GPMC arjun glucose::glucose GMP::GMPXX GMP::GMP cadiback cadical) if(USE_GLUCOSE) target_link_libraries(core glucose::glucose) diff --git a/cmake/FindGPMC.cmake b/cmake/FindGPMC.cmake new file mode 100644 index 00000000..df2ab512 --- /dev/null +++ b/cmake/FindGPMC.cmake @@ -0,0 +1,54 @@ +include(FindPackageHandleStandardArgs) + +# Keep track of the original library suffixes to reset them later. +set(_gpmc_ORIG_CMAKE_FIND_LIBRARY_SUFFIXES ${CMAKE_FIND_LIBRARY_SUFFIXES}) + +# Look for .a or .lib libraries in case of a static library. +if(GPMC_USE_STATIC_LIBS) + set(CMAKE_FIND_LIBRARY_SUFFIXES .a .lib) +endif() + +# Find libraries and headers. +find_library(GPMC_LIBRARY NAMES gpmc) +find_path(GPMC_INCLUDE_DIR NAMES gpmc.hpp) + +# Windows (dynamic): Also find import libraries. +if(WIN32 AND NOT GPMC_USE_STATIC_LIBS) + set(CMAKE_FIND_LIBRARY_SUFFIXES .dll.a .lib) + find_library(GPMC_IMPORT_LIBRARY NAMES gpmc) +endif() + +# Reset library suffixes. +set(CMAKE_FIND_LIBRARY_SUFFIXES ${_gpmc_ORIG_CMAKE_FIND_LIBRARY_SUFFIXES}) + +# Register the found package. +if(WIN32 AND NOT GPMC_USE_STATIC_LIBS) + # Windows (dynamic): also require import libraries. + find_package_handle_standard_args(GPMC REQUIRED_VARS GPMC_LIBRARY GPMC_IMPORT_LIBRARY GPMC_INCLUDE_DIR) +else() + find_package_handle_standard_args(GPMC REQUIRED_VARS GPMC_LIBRARY GPMC_INCLUDE_DIR) +endif() + +if(GPMC_FOUND) + mark_as_advanced(GPMC_LIBRARY) + mark_as_advanced(GPMC_IMPORT_LIBRARY) + mark_as_advanced(GPMC_INCLUDE_DIR) + + # Create targets in case not already done. + if(NOT TARGET GPMC::GPMC) + if(GPMC_USE_STATIC_LIBS) + add_library(GPMC::GPMC STATIC IMPORTED) + else() + add_library(GPMC::GPMC SHARED IMPORTED) + endif() + + # Set library and include paths. + set_target_properties(GPMC::GPMC PROPERTIES IMPORTED_LOCATION ${GPMC_LIBRARY}) + target_include_directories(GPMC::GPMC INTERFACE ${GPMC_INCLUDE_DIR}) + + # Windows (dynamic): Also set import library. + if(WIN32 AND NOT GPMC_USE_STATIC_LIBS) + set_target_properties(GPMC::GPMC PROPERTIES IMPORTED_IMPLIB ${GPMC_IMPORT_LIBRARY}) + endif() + endif() +endif() diff --git a/flake.lock b/flake.lock index 5e411f5d..a62cc105 100644 --- a/flake.lock +++ b/flake.lock @@ -2,11 +2,11 @@ "nodes": { "nixpkgs": { "locked": { - "lastModified": 1727540905, - "narHash": "sha256-40J9tW7Y794J7Uw4GwcAKlMxlX2xISBl6IBigo83ih8=", + "lastModified": 1728627514, + "narHash": "sha256-r+SF9AnHrTg+bk6YszoKfV9lgyw+yaFUQe0dOjI0Z2o=", "owner": "NixOS", "repo": "nixpkgs", - "rev": "fbca5e745367ae7632731639de5c21f29c8744ed", + "rev": "c505ebf777526041d792a49d5f6dd4095ea391a7", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 917c2420..1daeb774 100644 --- a/flake.nix +++ b/flake.nix @@ -16,6 +16,9 @@ "x86_64-linux" ]; + # If building for Windows, appends -windows, otherwise nothing. + windowsSuffix = pkgs: name: if pkgs.stdenv.hostPlatform.isWindows then "${name}-windows" else name; + # Different platforms require different TBB versions and the Windows one is not in upstream Nixpkgs yet. tbb = pkgs: @@ -26,23 +29,23 @@ else pkgs.tbb_2021_11; - mt-kahypar = pkgs: pkgs.callPackage ./nix/mt-kahypar.nix { tbb = tbb pkgs; }; - d4 = pkgs: pkgs.callPackage ./nix/d4.nix { mt-kahypar = mt-kahypar pkgs; }; - # All required runtime dependencies. dependencies = pkgs: + let + system = pkgs.buildPlatform.system; + windowsSuffix' = windowsSuffix pkgs; + in pkgs.buildEnv { name = "d4-dependencies"; paths = [ - (mt-kahypar pkgs) - (tbb pkgs) + self.packages.${system}.${windowsSuffix' "mt-kahypar"} + self.packages.${system}.${windowsSuffix' "tbb"} pkgs.hwloc.lib pkgs.gmp ] ++ lib.optionals pkgs.stdenv.cc.isClang [ pkgs.libcxx ]; }; - # A simple README explaining how to setup the built directories to run the binary. documentation = pkgs: pkgs.stdenv.mkDerivation { @@ -57,12 +60,16 @@ # The binary with all dependencies. bundled = pkgs: + let + system = pkgs.buildPlatform.system; + windowsSuffix' = windowsSuffix pkgs; + in pkgs.buildEnv { name = "d4"; paths = [ - (d4 pkgs) - (dependencies pkgs) - (documentation pkgs) + self.packages.${system}.${windowsSuffix' "d4"} + self.packages.${system}.${windowsSuffix' "dependencies"} + self.packages.${system}.${windowsSuffix' "documentation"} ]; }; in @@ -72,29 +79,57 @@ system: let pkgs = nixpkgs.legacyPackages.${system}; + pkgs-static = if pkgs.stdenv.isDarwin then pkgs else pkgs.pkgsStatic; pkgs-windows = pkgs.pkgsCross.mingwW64; in { default = self.packages.${system}.d4; - cadical = pkgs.pkgsStatic.callPackage ./nix/cadical.nix { }; - cadiback = pkgs.pkgsStatic.callPackage ./nix/cadiback.nix { + glucose = pkgs-static.callPackage ./nix/glucose.nix { }; + glucose-windows = pkgs-windows.callPackage ./nix/glucose.nix { }; + + cadical = pkgs-static.callPackage ./nix/cadical.nix { }; + cadical-windows = pkgs-windows.callPackage ./nix/cadical.nix { }; + + cadiback = pkgs-static.callPackage ./nix/cadiback.nix { cadical = self.packages.${system}.cadical; }; - cryptominisat = pkgs.pkgsStatic.callPackage ./nix/cryptominisat.nix { + cadiback-windows = pkgs-windows.callPackage ./nix/cadiback.nix { + cadical = self.packages.${system}.cadical-windows; + }; + + cryptominisat = pkgs-static.callPackage ./nix/cryptominisat.nix { + cadical = self.packages.${system}.cadical; cadiback = self.packages.${system}.cadiback; }; - sbva = pkgs.pkgsStatic.callPackage ./nix/sbva.nix { }; + cryptominisat-windows = pkgs-windows.callPackage ./nix/cryptominisat.nix { + cadical = self.packages.${system}.cadical-windows; + cadiback = self.packages.${system}.cadiback-windows; + }; + + sbva = pkgs-static.callPackage ./nix/sbva.nix { }; + sbva-windows = pkgs-windows.callPackage ./nix/sbva.nix { }; - arjun = pkgs.pkgsStatic.callPackage ./nix/arjun.nix { + arjun = pkgs-static.callPackage ./nix/arjun.nix { cryptominisat = self.packages.${system}.cryptominisat; sbva = self.packages.${system}.sbva; }; - gpmc = pkgs.pkgsStatic.callPackage ./nix/gpmc.nix { + arjun-windows = pkgs-windows.callPackage ./nix/arjun.nix { + cryptominisat = self.packages.${system}.cryptominisat-windows; + sbva = self.packages.${system}.sbva-windows; + }; + + gpmc = pkgs-static.callPackage ./nix/gpmc.nix { arjun = self.packages.${system}.arjun; + cryptominisat = self.packages.${system}.cryptominisat; + }; + + gpmc-windows = pkgs-windows.callPackage ./nix/gpmc.nix { + arjun = self.packages.${system}.arjun-windows; + cryptominisat = self.packages.${system}.cryptominisat-windows; }; tbb = tbb pkgs; @@ -108,13 +143,24 @@ d4 = pkgs.callPackage ./nix/d4.nix { mt-kahypar = self.packages.${system}.mt-kahypar; arjun = self.packages.${system}.arjun; + gpmc = self.packages.${system}.gpmc; + glucose = self.packages.${system}.glucose; + cryptominisat = self.packages.${system}.cryptominisat; + sbva = self.packages.${system}.sbva; + cadical = self.packages.${system}.cadical; + cadiback = self.packages.${system}.cadiback; }; - # TODO: arjun on windows - #d4-windows = pkgs-windows.callPackage ./nix/d4.nix { - # mt-kahypar = self.packages.${system}.mt-kahypar-windows; - # arjun = self.packages.${system}.arjun-windows; - #}; + d4-windows = pkgs-windows.callPackage ./nix/d4.nix { + mt-kahypar = self.packages.${system}.mt-kahypar-windows; + arjun = self.packages.${system}.arjun-windows; + gpmc = self.packages.${system}.gpmc-windows; + glucose = self.packages.${system}.glucose-windows; + cryptominisat = self.packages.${system}.cryptominisat-windows; + sbva = self.packages.${system}.sbva-windows; + cadical = self.packages.${system}.cadical-windows; + cadiback = self.packages.${system}.cadiback-windows; + }; container = pkgs.dockerTools.buildLayeredImage { name = "d4"; @@ -132,6 +178,9 @@ dependencies = dependencies pkgs; dependencies-windows = dependencies pkgs-windows; + documentation = documentation pkgs; + documentation-windows = documentation pkgs-windows; + bundled = bundled pkgs; bundled-windows = bundled pkgs-windows; } diff --git a/nix/cryptominisat.nix b/nix/cryptominisat.nix index 6deb6ea2..5bc9d521 100644 --- a/nix/cryptominisat.nix +++ b/nix/cryptominisat.nix @@ -5,6 +5,7 @@ cmake, gmp, zlib, + cadical, cadiback, }: stdenv.mkDerivation rec { @@ -30,6 +31,7 @@ stdenv.mkDerivation rec { buildInputs = [ zlib.dev + cadical.dev cadiback.dev gmp.dev ]; diff --git a/nix/d4.nix b/nix/d4.nix index 273e9c55..ec7ccf36 100644 --- a/nix/d4.nix +++ b/nix/d4.nix @@ -5,8 +5,15 @@ cmake, boost, gmp, + mpfr, mt-kahypar, arjun, + gpmc, + glucose, + cryptominisat, + sbva, + cadical, + cadiback, }: stdenv.mkDerivation rec { pname = "d4"; @@ -21,6 +28,13 @@ stdenv.mkDerivation rec { arjun.dev boost.dev gmp.dev + mpfr.dev + gpmc.dev + glucose.dev + cryptominisat.dev + sbva.dev + cadical.dev + cadiback.dev ]; meta = with lib; { diff --git a/nix/glucose.nix b/nix/glucose.nix new file mode 100644 index 00000000..2f6a3118 --- /dev/null +++ b/nix/glucose.nix @@ -0,0 +1,29 @@ +{ + lib, + stdenv, + cmake, + zlib, +}: +stdenv.mkDerivation { + pname = "glucose"; + version = "3.0.0"; + + outputs = [ + "out" + "lib" + "dev" + ]; + + src = ./../3rdParty/glucose-3.0; + + nativeBuildInputs = [ cmake ]; + + buildInputs = [ zlib.dev ]; + + meta = { + description = "SAT solver"; + homepage = "https://github.com/audemard/glucose"; + license = lib.licenses.mit; + platforms = lib.platforms.unix ++ lib.platforms.windows; + }; +} diff --git a/nix/gpmc.nix b/nix/gpmc.nix index a57d3071..13eab1db 100644 --- a/nix/gpmc.nix +++ b/nix/gpmc.nix @@ -3,10 +3,13 @@ stdenv, cmake, gmp, - arjun + zlib, + mpfr, + arjun, + cryptominisat, }: stdenv.mkDerivation { - pname = "gmpc"; + pname = "gpmc"; version = "1.0.1"; outputs = [ @@ -22,7 +25,10 @@ stdenv.mkDerivation { buildInputs = [ gmp.dev + mpfr.dev + zlib.dev arjun.dev + cryptominisat.dev ]; meta = { diff --git a/src/caching/CacheListLRU.hpp b/src/caching/CacheListLRU.hpp new file mode 100644 index 00000000..efe67df9 --- /dev/null +++ b/src/caching/CacheListLRU.hpp @@ -0,0 +1,420 @@ +/* + * d4 + * Copyright (C) 2020 Univ. Artois & CNRS + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with this program. If not, see . + */ +#pragma once + +#include "src/hashing/hasher.hpp" +#include +#include +#include +#include + +#include "BucketManager.hpp" +#include "CacheCleaningManager.hpp" +#include "CachedBucket.hpp" +#include "sparsepp/spp.h" +#include "src/caching/CacheCleaningManager.hpp" +#include "src/caching/cnf/BucketManagerCnf.hpp" +#include "src/hashing/HashString.hpp" +#include "src/specs/SpecManager.hpp" +#include + +namespace d4 { +// (Probalistic) LRU cache implementations, the integration into D4's +// interface is very cluncky and prone to bugs since it +// depends on depth-first free/alloc behavior from DPLL. +// Should be rewritten... + +namespace po = boost::program_options; +template class CacheListLRU : public CacheManager { +private: + const unsigned SIZE_HASH = 1024 * 1024; + struct Node { + CachedBucket bucket; + size_t last_use; + }; + + std::vector> hashTable; + size_t counter = 0; + size_t max_mem = (1ull << 30) * 5; // 5GB + +public: + /** + * @brief Construct a new Cache List object + * + * @param vm is a map to get the option. + * @param nbVar is the number of variables. + * @param specs is a structure to get data about the formula. + * @param out is the stream where are printed out the logs. + */ + CacheListLRU(po::variables_map &vm, unsigned nbVar, SpecManager *specs, + std::ostream &out) + : CacheManager(vm, nbVar, specs, out) { + out << "c [CACHE LIST CONSTRUCTOR]\n"; + max_mem = (1ull << 30ull) * vm["cache-fixed-size"].as(); + initHashTable(nbVar); + } // constructor + + /** + * @brief Destroy the Cache List object + */ + ~CacheListLRU() {} // destructor + + /** + * @brief Add an entry in the cache. + * + * @param cb is the bucket we want to add. + * @param hashValue is the hash value of the bucket. + * @param val is the value we associate with the bucket. + */ + inline void pushInHashTable(CachedBucket &cb, unsigned hashValue, T val) { + hashTable[hashValue % SIZE_HASH].push_back(Node{cb, counter}); + CachedBucket &cbIn = (hashTable[hashValue % SIZE_HASH].back().bucket); + cbIn.lockedBucket(val); + this->m_nbCreationBucket++; + this->m_sumDataSize += cb.szData(); + this->m_nbEntry++; + this->counter++; + if (this->m_bucketManager->usedMemory() > max_mem) { + + std::vector last_use; + for (auto &v : hashTable) { + for (auto &b : v) { + last_use.push_back(b.last_use); + } + } + if (last_use.size() < 1) { + return; + } + std::sort(last_use.begin(), last_use.end()); + size_t median = last_use[last_use.size() / 3]; + size_t removed = 0; + + for (auto &v : hashTable) { + for (auto &e : v) { + if (e.last_use < median) { + this->m_bucketManager->releaseMemory(e.bucket.data, + e.bucket.szData()); + removed++; + } + } + } + + for (auto &v : hashTable) { + std::erase_if(v, [&](const Node &n) { + if (n.last_use < median) { + return true; + } + return false; + }); + } + std::cout << "Removed: " << removed << " Mem" + << this->m_bucketManager->usedMemory() << std::endl; + } + + } // pushinhashtable + + /** + * @brief Research in the set of buckets if the bucket pointed by i already + * exist. + * + * @param cb is the bucket we are looking for. + * @param hashValue is the hash value computed from the bucket. + * @return a valid entry if it is in the cache, null otherwise. + */ + CachedBucket *bucketAlreadyExist(CachedBucket &cb, unsigned hashValue) { + char *refData = cb.data; + std::vector &listCollision = hashTable[hashValue % SIZE_HASH]; + for (auto &cbi : listCollision) { + if (!cb.sameHeader(cbi.bucket)) + continue; + + if (!memcmp(refData, cbi.bucket.data, cbi.bucket.szData())) { + this->m_nbPositiveHit++; + cbi.last_use = this->counter; + return &cbi.bucket; + } + } + + this->m_nbNegativeHit++; + return NULL; + } // bucketAlreadyExist + + /** + * Create a bucket and store it in the cache. + * + * @param varConnected is the set of variable. + * @param c is the value we want to store. + */ + inline void createAndStoreBucket(std::vector &varConnected, T &c) { + CachedBucket *formulaBucket = + this->m_bucketManager->collectBuckect(varConnected); + unsigned int hashValue = computeHash(*formulaBucket); + pushInHashTable(*formulaBucket, hashValue, c); + } // createBucket + + /** + * @brief Init the hashTable. + * + * @param maxVar is the number of variable. + */ + void initHashTable(unsigned maxVar) override { + this->setInfoFormula(maxVar); + // init hash tables + hashTable.clear(); + hashTable.resize(SIZE_HASH, {}); + } // initHashTable + + /** + * @brief Clean up the cache. + * + * @param test is a function that is used to decide if an entry must be + * removed. + * + * @return the number of entry we removed. + */ + unsigned removeEntry(std::function &c)> test) { + unsigned nbRemoveEntry = 0; + for (auto &list : hashTable) { + unsigned j = 0; + for (unsigned i = 0; i < list.size(); i++) { + CachedBucket &cb = list[i].bucket; + + if (test(cb)) { + assert((int)cb.szData() > 0); + this->releaseMemory(cb.data, cb.szData()); + cb.reset(); + nbRemoveEntry++; + } else + list[j++] = list[i]; + } + list.resize(j); + } + return nbRemoveEntry; + } // removeEntry +}; + +/** + * + */ +template class CacheListProbLRU : public CacheManager { +private: + struct Node { + unsigned key; + unsigned last_use; + T data; + }; + std::vector key_mem; + unsigned key_cnt = 0; + std::vector free_keys; + struct Hasher { + const CacheListProbLRU *owner; + size_t operator()(const Node &n) const { return owner->get_key(n.key)[0]; } + }; + + friend struct Hasher; + struct KeyEq { + const CacheListProbLRU *owner; + bool operator()(const Node &lhs, const Node &rhs) const { + return !memcmp(owner->get_key(lhs.key), owner->get_key(rhs.key), + owner->key_len * sizeof(uint64_t)); + } + }; + friend struct KeyEq; + spp::sparse_hash_set table; + size_t max_mem = (1ull << 30) * 8; // 8gb + unsigned max_elmts; + unsigned key_len = 2; + unsigned time = 0; + unsigned min_time = 0; + static std::mt19937_64 gen; + CLHasher hasher; + CachedBucket tmp; + +public: + const uint64_t *get_key(unsigned i) const { + size_t k = size_t(i) * key_len; + return key_mem.data() + k; + } + void destroy_key(unsigned i) { free_keys.push_back(i); } + std::pair create_key() { + if (free_keys.size()) { + unsigned idx = free_keys.back(); + free_keys.pop_back(); + return {idx, key_mem.data() + idx * key_len}; + } else { + if (key_cnt == key_mem.size() / key_len) { + std::cout << "Realloc keys" << std::endl; + key_mem.resize(key_mem.size() * 1.5); + } + unsigned idx = key_cnt++; + return {idx, key_mem.data() + idx * key_len}; + } + } + /** + * @brief Construct a new Cache List object + * + * @param vm is a map to get the option. + * @param nbVar is the number of variables. + * @param specs is a structure to get data about the formula. + * @param out is the stream where are printed out the logs. + */ + CacheListProbLRU(po::variables_map &vm, unsigned nbVar, SpecManager *specs, + std::ostream &out) + : CacheManager(vm, nbVar, specs, out), + table(0, Hasher{this}, KeyEq{this}) { + out << "c [CACHE LIST LRU PROB CONSTRUCTOR]\n"; + max_mem = (1ull << 30ull) * vm["cache-fixed-size"].as(); + max_elmts = max_mem / + (sizeof(unsigned) + sizeof(uint64_t) * key_len + sizeof(Node)); + key_mem.resize(max_elmts * 1.5); + out << "[CACH LIST LRU ]Fixed Cache: " << max_elmts << std::endl; + initHashTable(nbVar); + hasher.init(gen, key_len); + + } // constructor + CacheListProbLRU(const CacheListProbLRU &) = delete; + + CacheListProbLRU &operator=(const CacheListProbLRU &) = delete; + + /** + * @brief Destroy the Cache List object + */ + ~CacheListProbLRU() {} // destructor + + /** + * @brief Add an entry in the cache. + * + * @param cb is the bucket we want to add. + * @param hashValue is the hash value of the bucket. + * @param val is the value we associate with the bucket. + */ + size_t computeHash(CachedBucket &bucket) final { + auto [id, key] = create_key(); + hasher.Hash(bucket.data, bucket.szData(), key); + this->m_bucketManager->releaseMemory(bucket.data, bucket.szData()); + bucket.data = nullptr; + return id; + } + inline void pushInHashTable(CachedBucket &_cb, unsigned hashValue, T val) { + table.insert(Node{hashValue, time, val}); + this->m_nbCreationBucket++; + this->m_sumDataSize += 1; + this->m_nbEntry++; + this->time++; + if (table.size() > max_elmts) { + std::cout << "Start clean " << table.size() << std::endl; + + if (table.size() < 8) { + return; + } + std::array hist = {}; + double dist = time - min_time; + for (auto &b : table) { + unsigned rtime = b.last_use - min_time; + unsigned id = (rtime / dist) * hist.size(); + hist[id]++; + } + unsigned acc = 0; + unsigned i = 0; + while (acc < table.size() / 2 && i < hist.size()) { + acc += hist[i]; + i++; + } + size_t median = (i * (dist / 256)) + min_time; + size_t removed = 0; + for (auto it = table.begin(); it != table.end();) { + if (it->last_use < median) { + destroy_key(it->key); + it = table.erase(it); + removed++; + } else { + it++; + } + } + min_time = median; + std::cout << "Removed: " << removed << " Cnt" << table.size() + << std::endl; + } + + } // pushinhashtable + + /** + * @brief Research in the set of buckets if the bucket pointed by i already + * exist. + * + * @param cb is the bucket we are looking for. + * @param hashValue is the hash value computed from the bucket. + * @return a valid entry if it is in the cache, null otherwise. + */ + CachedBucket *bucketAlreadyExist(CachedBucket &_cb, + unsigned hashValue) { + auto it = table.find(Node{hashValue}); + if (it == table.end()) { + this->m_nbNegativeHit++; + return 0; + } else { + // remove const ... + *((unsigned *)&it->last_use) = time; + tmp.fc = it->data; + + this->m_nbPositiveHit++; + + destroy_key(hashValue); + + return &tmp; + } + return NULL; + } // bucketAlreadyExist + + /** + * Create a bucket and store it in the cache. + * + * @param varConnected is the set of variable. + * @param c is the value we want to store. + */ + inline void createAndStoreBucket(std::vector &varConnected, T &c) { + assert(0); + } // createBucket + + /** + * @brief Init the hashTable. + * + * @param maxVar is the number of variable. + */ + void initHashTable(unsigned maxVar) override { + this->setInfoFormula(maxVar); + } // initHashTable + + /** + * @brief Clean up the cache. + * + * @param test is a function that is used to decide if an entry must be + * removed. + * + * @return the number of entry we removed. + */ + unsigned removeEntry(std::function &c)> test) { + assert(0); + } // removeEntry +}; + +template +std::mt19937_64 CacheListProbLRU::gen = std::mt19937_64(43); + +} // namespace d4 + // diff --git a/src/config/Config.cpp b/src/config/Config.cpp index 1b73d751..886bb4bd 100644 --- a/src/config/Config.cpp +++ b/src/config/Config.cpp @@ -12,8 +12,9 @@ namespace d4 { config.maxsharpsat_heuristic_phase_random = 5; config.maxsharpsat_option_and_dig = true; config.maxsharpsat_option_greedy_init = false; - config.preproc = "basic"; + config.projddnnf_pure_lit_elim = true; config.scoring_method = "vsads"; + config.scoring_method_decay_freq = 300000; config.occurrence_manager = "dynamic"; config.phase_heuristic = "polarity"; config.partitioning_heuristic = "decomposition-static-dual"; @@ -23,6 +24,12 @@ namespace d4 { config.partitioning_heuristic_simplification_equivalence = true; config.partitioning_heuristic_simplification_hyperedge = true; config.partitioning_threads = 1; + config.preproc = "basic"; + config.preproc_equiv = true; + config.preproc_ve_check = false; + config.preproc_ve_only_simpical = true; + config.preproc_ve_prefer_simpical = false; + config.preproc_ve_limit = 4; config.cache_reduction_strategy = "expectation"; config.cache_reduction_strategy_cachet_limit = 10UL * (1<<21); config.cache_reduction_strategy_expectation_limit = 100000; @@ -44,6 +51,7 @@ namespace d4 { config.query = ""; config.projMC_refinement = false; config.keyword_output_format_solution = "s"; + config.output = ""; config.output_format = "classic"; return config; diff --git a/src/config/Config.hpp b/src/config/Config.hpp index fb2c6c1d..5fcf3e92 100644 --- a/src/config/Config.hpp +++ b/src/config/Config.hpp @@ -15,8 +15,9 @@ namespace d4 { unsigned maxsharpsat_heuristic_phase_random; bool maxsharpsat_option_and_dig; bool maxsharpsat_option_greedy_init; - string preproc; + bool projddnnf_pure_lit_elim; string scoring_method; + unsigned scoring_method_decay_freq; string occurrence_manager; string phase_heuristic; string partitioning_heuristic; @@ -26,6 +27,12 @@ namespace d4 { bool partitioning_heuristic_simplification_equivalence; bool partitioning_heuristic_simplification_hyperedge; unsigned partitioning_threads; + string preproc; + bool preproc_equiv; + bool preproc_ve_check; + bool preproc_ve_only_simpical; + bool preproc_ve_prefer_simpical; + int preproc_ve_limit; string cache_reduction_strategy; unsigned long cache_reduction_strategy_cachet_limit; unsigned long cache_reduction_strategy_expectation_limit; @@ -47,6 +54,7 @@ namespace d4 { string query; bool projMC_refinement; string keyword_output_format_solution; + string output; string output_format; static Config default_values(); diff --git a/src/config/ConfigConverter.cpp b/src/config/ConfigConverter.cpp index a364226b..c3a98486 100644 --- a/src/config/ConfigConverter.cpp +++ b/src/config/ConfigConverter.cpp @@ -18,8 +18,9 @@ namespace d4 { config.maxsharpsat_heuristic_phase_random = vm["maxsharpsat-heuristic-phase-random"].as(); config.maxsharpsat_option_and_dig = vm["maxsharpsat-option-and-dig"].as(); config.maxsharpsat_option_greedy_init = vm["maxsharpsat-option-greedy-init"].as(); - config.preproc = vm["preproc"].as(); + config.projddnnf_pure_lit_elim = vm["projddnnf-pure-lit-elim"].as(); config.scoring_method = vm["scoring-method"].as(); + config.scoring_method_decay_freq = vm["scoring-method-decay-freq"].as(); config.occurrence_manager = vm["occurrence-manager"].as(); config.phase_heuristic = vm["phase-heuristic"].as(); config.partitioning_heuristic = vm["partitioning-heuristic"].as(); @@ -29,6 +30,12 @@ namespace d4 { config.partitioning_heuristic_simplification_equivalence = vm["partitioning-heuristic-simplification-equivalence"].as(); config.partitioning_heuristic_simplification_hyperedge = vm["partitioning-heuristic-simplification-hyperedge"].as(); config.partitioning_threads = vm["partitioning-threads"].as(); + config.preproc = vm["preproc"].as(); + config.preproc_equiv = vm["preproc-equiv"].as(); + config.preproc_ve_check = vm["preproc-ve-check"].as(); + config.preproc_ve_only_simpical = vm["preproc-ve-only-simpical"].as(); + config.preproc_ve_prefer_simpical = vm["preproc-ve-prefer-simpical"].as(); + config.preproc_ve_limit = vm["preproc-ve-limit"].as(); config.cache_reduction_strategy = vm["cache-reduction-strategy"].as(); config.cache_reduction_strategy_cachet_limit = vm["cache-reduction-strategy-cachet-limit"].as(); config.cache_reduction_strategy_expectation_limit = vm["cache-reduction-strategy-expectation-limit"].as(); @@ -61,6 +68,7 @@ namespace d4 { config.projMC_refinement = vm["projMC-refinement"].as(); config.keyword_output_format_solution = vm["keyword-output-format-solution"].as(); + config.output = vm["output"].as(); config.output_format = vm["output-format"].as(); return config; diff --git a/src/heuristics/ProjBackupHeuristic.cpp b/src/heuristics/ProjBackupHeuristic.cpp new file mode 100644 index 00000000..d02eaed9 --- /dev/null +++ b/src/heuristics/ProjBackupHeuristic.cpp @@ -0,0 +1,29 @@ +#include "ProjBackupHeuristic.hpp" + +#include + +#include "src/heuristics/cnf/ProjBackupHeuristicHypergraph.hpp" +#include "src/heuristics/cnf/ProjBackupHeuristicComponents.hpp" + +namespace d4 { + +std::unique_ptr +ProjBackupHeuristic::make(Config &config, SpecManager &p, + WrapperSolver &s, std::ostream &out) { + std::string meth = "hypergraph"; // vm["proj-backup"].as(); + if (meth == "hypergraph") { + return std::make_unique(config, p, s, out); + + } else if (meth == "component") { + return std::make_unique(config, p, s, out); + + } else if (meth == "none") { + return std::make_unique(); + } + throw std::runtime_error("unknown proj-backup method"); +} +bool ProjBackupHeuristic::computeCutSetDyn(ProjVars &component, + std::vector &cutset) { + return false; +} +} // namespace d4 diff --git a/src/heuristics/ProjBackupHeuristic.hpp b/src/heuristics/ProjBackupHeuristic.hpp new file mode 100644 index 00000000..a12bc4e8 --- /dev/null +++ b/src/heuristics/ProjBackupHeuristic.hpp @@ -0,0 +1,16 @@ +#pragma once +#include "src/solvers/WrapperSolver.hpp" +#include "src/specs/cnf/SpecManagerCnf.hpp" +#include +namespace d4 { +//TODO delete this since its useless +class ProjBackupHeuristic { +public: + virtual ~ProjBackupHeuristic() {} + virtual bool computeCutSetDyn(ProjVars &component, std::vector &cutset); + static std::unique_ptr make(Config &config, + SpecManager &p, + WrapperSolver &s, + std::ostream &out); +}; +} // namespace d4 diff --git a/src/heuristics/ScoringMethod.cpp b/src/heuristics/ScoringMethod.cpp index 1cc9f7ce..708bb20e 100644 --- a/src/heuristics/ScoringMethod.cpp +++ b/src/heuristics/ScoringMethod.cpp @@ -27,9 +27,9 @@ namespace d4 { /** - Select from the arguments store in config the good scoring method and return it. + Select from the arguments store in vm the good scoring method and return it. - @param[in] config, the configuration. + @param[in] vm, the arguments on the command line. @pararm[in] p, the problem manager. \return the scoring method @@ -38,17 +38,23 @@ ScoringMethod *ScoringMethod::makeScoringMethod(Config &config, SpecManager &p, ActivityManager &am, std::ostream &out) { - out << "c [CONSTRUCTOR] Variable heuristic: " << config.scoring_method << "\n"; + std::string inType = config.input_type; + std::string meth = config.scoring_method; + out << "c [CONSTRUCTOR] Variable heuristic: " << meth << "\n"; - if (config.input_type == "cnf" || config.input_type == "dimacs") { + if (inType == "cnf" || inType == "dimacs") { try { SpecManagerCnf &ps = dynamic_cast(p); - - if (config.scoring_method == "mom") return new ScoringMethodMom(ps); - if (config.scoring_method == "dlcs") return new ScoringMethodDlcs(ps); - if (config.scoring_method == "vsids") return new ScoringMethodVsids(am); - if (config.scoring_method == "vsads") return new ScoringMethodVsads(ps, am); - if (config.scoring_method == "jwts") return new ScoringMethodJwts(ps); + if (meth == "mom") + return new ScoringMethodMom(ps); + if (meth == "dlcs") + return new ScoringMethodDlcs(ps); + if (meth == "vsids") + return new ScoringMethodVsids(am); + if (meth == "vsads") + return new ScoringMethodVsads(ps, am); + if (meth == "jwts") + return new ScoringMethodJwts(ps); return NULL; } catch (std::bad_cast &bc) { std::cerr << "bad_cast caught: " << bc.what() << '\n'; @@ -57,7 +63,7 @@ ScoringMethod *ScoringMethod::makeScoringMethod(Config &config, } throw(FactoryException("Cannot create a ScoringMethod", __FILE__, __LINE__)); -} // makeScoringMethod +} // makeScoringMethod /** Select the best variable in vars and return it. @@ -73,7 +79,30 @@ Var ScoringMethod::selectVariable(std::vector &vars, SpecManager &s, assert(isDecisionVariable.size() >= (unsigned)s.getNbVariable()); for (auto &v : vars) { - if (s.varIsAssigned(v) || !isDecisionVariable[v]) continue; + if (s.varIsAssigned(v) || !isDecisionVariable[v]) + continue; + if (ret != var_Undef && s.varIsAssigned(v)) { + break; + } + + double current = computeScore(v); + if (ret == var_Undef || current > bestScore) { + ret = v; + bestScore = current; + } + } + //sleep(1); + + return ret; +} // selectVariable + // +Var ScoringMethod::selectVariable(std::vector &vars, SpecManager &s) { + Var ret = var_Undef; + double bestScore = -1; + + for (auto &v : vars) { + if (s.varIsAssigned(v) || !s.isSelected(v)) + continue; double current = computeScore(v); if (ret == var_Undef || current > bestScore) { @@ -81,8 +110,23 @@ Var ScoringMethod::selectVariable(std::vector &vars, SpecManager &s, bestScore = current; } } + return ret; +} // selectVariable +Var ScoringMethod:: selectVariable(std::vector &vars,std::function can_select){ + Var ret = var_Undef; + double bestScore = -1; + for (auto &v : vars) { + if(!can_select(v)) + continue; + double current = computeScore(v); + if (ret == var_Undef || current > bestScore) { + ret = v; + bestScore = current; + } + } return ret; -} // selectVariable -} // namespace d4 +} + +} // namespace d4 diff --git a/src/heuristics/ScoringMethod.hpp b/src/heuristics/ScoringMethod.hpp index 1f23e219..e6496a29 100644 --- a/src/heuristics/ScoringMethod.hpp +++ b/src/heuristics/ScoringMethod.hpp @@ -16,18 +16,18 @@ * along with this program. If not, see . */ #pragma once - -#include - -#include +#include +#include #include #include #include #include +#include namespace d4 { +namespace po = boost::program_options; class ScoringMethod { - public: +public: static ScoringMethod *makeScoringMethod(Config &config, SpecManager &p, ActivityManager &am, std::ostream &out); @@ -37,5 +37,10 @@ class ScoringMethod { Var selectVariable(std::vector &vars, SpecManager &s, std::vector &isDecisionVariable); + + Var selectVariable(std::vector &vars, SpecManager &s); + virtual Var selectVariable(std::vector &vars, + std::function can_select); + virtual void decay(){} }; -} // namespace d4 +} // namespace d4 diff --git a/src/heuristics/cnf/ProjBackupHeuristicComponents.cpp b/src/heuristics/cnf/ProjBackupHeuristicComponents.cpp new file mode 100644 index 00000000..513aed64 --- /dev/null +++ b/src/heuristics/cnf/ProjBackupHeuristicComponents.cpp @@ -0,0 +1,143 @@ +#include "ProjBackupHeuristicComponents.hpp" +#include "src/hyperGraph/HyperGraphExtractorDualProj.hpp" +#include "src/utils/UnionFind.hpp" +#include + +namespace d4 { +ProjBackupHeuristicComponents::ProjBackupHeuristicComponents( + Config &config, SpecManager &om, WrapperSolver &s, std::ostream &out) + : m_om(dynamic_cast(om)), + m_current_component(m_om.getNbVariable() + 1), + m_uf(m_om.getNbVariable() + 1) { + + // FIXME: was not in original options, what shoud be the default values? + m_min_ccover = 1.0; // vm["proj-backup-min-cover"].as(); + m_scroing_method = 1; //vm["proj-backup-scoring-method"].as(); + +} // constructor + +bool ProjBackupHeuristicComponents::computeCutSetDyn(ProjVars &component, + std::vector &cutSet) { + + if (component.vars.size()/double(m_om.getNbVariable())<0.3||calls>20) { + return false; + } + calls++; + + m_uf.clear(); + for (auto v : component.vars) { + m_current_component[v] = true; + } + std::vector nproj_clauses; + std::vector clauses; + double clause_cnt = 0; + for (int i = 0; i < m_om.getNbClause(); i++) { + if (!m_om.isNotSatisfiedClauseAndInComponent(i, m_current_component)) { + continue; + } + clauses.push_back(i); + int set = -1; + clause_cnt++; + for (auto l : m_om.getClause(i)) { + if (m_om.isSelected(l.var()) || m_om.litIsAssigned(l)) + continue; + if (set == -1) { + set = m_uf.find_set(l.var()); + nproj_clauses.push_back(i); + } else { + m_uf.union_sets(l.var(), set); + } + } + } + for (auto v : component.vars) { + m_current_component[v] = false; + } + std::vector set2index(m_om.getNbVariable() + 1, -1); + std::vector nproj_sets; + for (auto i : nproj_clauses) { + int set = -1; + for (auto l : m_om.getClause(i)) { + if (m_om.isSelected(l.var()) || m_om.litIsAssigned(l)) + continue; + set = m_uf.find_set(m_om.getClause(i).back().var()); + } + if (set2index[set] == -1) { + set2index[set] = nproj_sets.size(); + nproj_sets.push_back(NProjComponent{}); + } + int idx = set2index[set]; + auto &inst = nproj_sets[idx]; + inst.ccover.insert(i); + inst.nproj_cnt += 1; + for (auto l : m_om.getClause(i)) { + if (m_om.litIsAssigned(l)) { + continue; + } + if (m_om.isSelected(l.var())) { + inst.neigh.insert(l.var()); + } else { + break; + } + } + } + if (nproj_sets.size() == 1) { + return false; + } + // std::cout << "Found " << nproj_sets.size() << " components" << std::endl; + for (auto &set : nproj_sets) { + for (auto n : set.neigh) { + Lit l = Lit::makeLitTrue(n); + for (int i = 0; i < 2; i++) { + auto iter = m_om.getVecIdxClause(l); + for (int *cli = iter.start; cli != iter.end; cli++) { + set.ccover.insert(*cli); + } + l = ~l; + } + } + } + int best_set = -1; + double best_score = 0; + for (int i = 0; i < nproj_sets.size(); i++) { + auto &set = nproj_sets[i]; + double size = set.ccover.size(); + double cover = set.ccover.size() / clause_cnt; + if (cover < m_min_ccover) { + continue; + } + double cover_nproj = double(set.nproj_cnt) / set.ccover.size(); + double cover_proj = + double(set.ccover.size() - set.nproj_cnt) / set.ccover.size(); + double score = 0; + + + double cut_size = set.neigh.size() / double(component.nbProj); + switch(m_scroing_method){ + case 0: + score = cover * (1 - cut_size); + case 1: + score = cover/cut_size; + } + assert(set.neigh.size() > 0); + + /*std::cout << "Component: Cut: " << cut_size << " Cover: " << cover + << " BalanaceProj: " << cover_proj + << " BalanaceNProj: " << cover_nproj<<"Score: "< best_score) { + + best_score = score; + best_set = i; + } + } + if (best_set == -1) { + return false; + + } else { + auto &neigh = nproj_sets[best_set].neigh; + cutSet = std::vector(neigh.begin(), neigh.end()); + return true; + } +} +} // namespace d4 diff --git a/src/heuristics/cnf/ProjBackupHeuristicComponents.hpp b/src/heuristics/cnf/ProjBackupHeuristicComponents.hpp new file mode 100644 index 00000000..2ce217df --- /dev/null +++ b/src/heuristics/cnf/ProjBackupHeuristicComponents.hpp @@ -0,0 +1,34 @@ +#pragma once +#include "PartitioningHeuristicStatic.hpp" +#include "src/heuristics/ProjBackupHeuristic.hpp" +#include "src/hyperGraph/HyperGraphExtractor.hpp" +#include "src/partitioner/PartitionerManager.hpp" +#include "src/solvers/WrapperSolver.hpp" +#include "src/specs/cnf/SpecManagerCnf.hpp" +#include "src/utils/EquivExtractor.hpp" +#include "src/utils/UnionFind.hpp" +#include +namespace d4 { +struct NProjComponent{ + std::unordered_set neigh; + std::unordered_set ccover; + int nproj_cnt= 0; +}; +class ProjBackupHeuristicComponents : public ProjBackupHeuristic { + SpecManagerCnf &m_om; + std::vector m_current_component; + UnionFind m_uf; + double m_min_ccover; + int m_scroing_method; + int calls=0; + + +public: + ProjBackupHeuristicComponents(Config &config, SpecManager &om, + WrapperSolver &s, std::ostream &out); + ~ProjBackupHeuristicComponents(){ + std::cout<<"Calls to BackupH "< &cutset) final; +}; +} // namespace d4 diff --git a/src/heuristics/cnf/ProjBackupHeuristicHypergraph.cpp b/src/heuristics/cnf/ProjBackupHeuristicHypergraph.cpp new file mode 100644 index 00000000..6a2ac171 --- /dev/null +++ b/src/heuristics/cnf/ProjBackupHeuristicHypergraph.cpp @@ -0,0 +1,116 @@ +#include "ProjBackupHeuristicHypergraph.hpp" +#include "src/hyperGraph/HyperGraphExtractorDualProj.hpp" + +namespace d4 { +ProjBackupHeuristicHypergraph::ProjBackupHeuristicHypergraph( + Config &config, SpecManager &om, WrapperSolver &s, std::ostream &out) + : m_om(dynamic_cast(om)), m_s(s) { + m_nbVar = m_om.getNbVariable(); + m_nbClause = m_om.getNbClause(); + + m_em.initEquivExtractor(m_nbVar + 1); + unsigned sumSize = m_om.getSumSizeClauses(); + + m_partition.resize(m_nbClause + 1, 0); + + m_pm = PartitionerManager::makePartitioner(m_nbClause, m_nbVar, sumSize, + out); + + m_hypergraph.init(m_nbVar + m_nbClause + sumSize + 1, m_nbClause + 1); + + // initialize the vectors. + m_markedVar.resize(m_nbVar + 1, false); + m_equivClass.resize(m_nbVar + 1, 0); + + // get the options. + m_reduceFormula = config.partitioning_heuristic_simplification_equivalence; + // FIXME: was not in original options, what shoud be the default value? + m_equivSimp = false; + m_hypergraphExtractor = + new HyperGraphExtractorDualProj(m_nbVar, m_nbClause, m_om); + +} // constructor +ProjBackupHeuristicHypergraph::~ProjBackupHeuristicHypergraph() { + if (m_hypergraphExtractor) { + delete m_hypergraphExtractor; + } + if (m_pm) { + delete m_pm; + } +} + +void ProjBackupHeuristicHypergraph::computeEquivClass( + std::vector &component, std::vector &unitEquiv, + std::vector &equivClass, std::vector> &equivVar) { + if (m_equivSimp) { + for (auto &v : component) { + assert(equivClass.size() >= (unsigned)v); + equivClass[v] = v; + } + + m_em.searchEquiv(m_s, component, equivVar); + m_s.whichAreUnits(component, unitEquiv); + + for (auto &c : equivVar) { + Var vi = c.back(); + for (auto &v : c) + equivClass[v] = vi; + } + + } else { + for (auto &v : component) + equivClass[v] = v; + } +} // computeEquivclass + +bool ProjBackupHeuristicHypergraph::computeCutSetDyn(ProjVars &component, + std::vector &cutSet) { + m_counter++; + + // search for equiv class if requiered. + std::vector unitEquiv; + std::vector> equivVar; + + computeEquivClass(component.vars, unitEquiv, m_equivClass, equivVar); + + // synchronize the SAT solver and the spec manager. + m_om.preUpdate(unitEquiv); + + // construct the hypergraph + std::vector considered; + m_hypergraphExtractor->constructHyperGraph(m_om, component.vars, m_equivClass, + equivVar, m_reduceFormula, + considered, m_hypergraph); + + if (m_hypergraph.getSize() < 5) + cutSet = component.vars; + else { + // set the level. + PartitionerManager::Level level = PartitionerManager::Level::NORMAL; + if (m_hypergraph.getSize() >= 200) + level = PartitionerManager::Level::QUALITY; + + m_pm->computePartition(m_hypergraph, level, m_partition); + m_hypergraphExtractor->extractCutFromHyperGraph(m_hypergraph, considered, + m_partition, cutSet); + + // extend with equivalence literals. + for (auto &v : cutSet) + m_markedVar[v] = true; + for (auto &v : component.vars) { + if (m_markedVar[v]) + continue; + if (m_markedVar[m_equivClass[v]]) + cutSet.push_back(v); + } + for (auto &v : cutSet) + m_markedVar[v] = false; + if (!cutSet.size()) + for (auto l : unitEquiv) + cutSet.push_back(l.var()); + } + + m_om.postUpdate(unitEquiv); + return true; +} +} // namespace d4 diff --git a/src/heuristics/cnf/ProjBackupHeuristicHypergraph.hpp b/src/heuristics/cnf/ProjBackupHeuristicHypergraph.hpp new file mode 100644 index 00000000..23a2df9b --- /dev/null +++ b/src/heuristics/cnf/ProjBackupHeuristicHypergraph.hpp @@ -0,0 +1,43 @@ +#pragma once +#include "PartitioningHeuristicStatic.hpp" +#include "src/hyperGraph/HyperGraphExtractor.hpp" +#include "src/partitioner/PartitionerManager.hpp" +#include "src/solvers/WrapperSolver.hpp" +#include "src/specs/cnf/SpecManagerCnf.hpp" +#include "src/utils/EquivExtractor.hpp" +#include "src/heuristics/ProjBackupHeuristic.hpp" +namespace d4 { +class ProjBackupHeuristicHypergraph:public ProjBackupHeuristic { +private: + SpecManagerCnf &m_om; + WrapperSolver &m_s; + EquivExtractor m_em; + PartitionerManager *m_pm; + + unsigned m_nbVar, m_nbClause; + unsigned m_counter = 0; + bool m_equivSimp; + bool m_reduceFormula; + bool m_useEquiv; + + // to store the hypergraph, and then avoid reallocated memory. + HyperGraph m_hypergraph; + HyperGraphExtractor *m_hypergraphExtractor; + + std::vector m_markedVar; + std::vector m_partition; + std::vector m_equivClass; + + void computeEquivClass(std::vector &component, + std::vector &unitEquiv, + std::vector &equivClass, + std::vector> &equivVar); + +public: + ProjBackupHeuristicHypergraph(Config &config, SpecManager &om, WrapperSolver &s, + std::ostream &out); + virtual ~ProjBackupHeuristicHypergraph(); + + bool computeCutSetDyn(ProjVars &component, std::vector &cutset) final; +}; +} // namespace d4 diff --git a/src/hyperGraph/HyperGraphExtractorDualProj.cpp b/src/hyperGraph/HyperGraphExtractorDualProj.cpp new file mode 100644 index 00000000..e4947ba7 --- /dev/null +++ b/src/hyperGraph/HyperGraphExtractorDualProj.cpp @@ -0,0 +1,175 @@ + +#include "HyperGraphExtractorDualProj.hpp" +namespace d4 { + +HyperGraphExtractorDualProj::HyperGraphExtractorDualProj(unsigned nbVar, + unsigned nbClause, + SpecManagerCnf &specs, + int nproj_cost) + : HyperGraphExtractorDual(nbVar, nbClause), m_specs(specs), + m_nproj_cost(nproj_cost) {} + +void HyperGraphExtractorDualProj::compute_stats(SpecManagerCnf &specs) { + m_cost.resize(specs.getNbVariable() + 1); + std::vector occurence_cnt(specs.getNbVariable() + 1); + double occurence_acc = 0; + for (Var v = 1; v <= specs.getNbVariable(); v++) { + if (!specs.isSelected(v)) { + break; + } + occurence_cnt[v] = specs.getNbOccurrence(Lit::makeLitTrue(v)) + + specs.getNbOccurrence(Lit::makeLitFalse(v)); + occurence_acc += occurence_cnt[v]; + } + double avg_occ = occurence_acc / specs.getNbVariable(); + double occ_var = 0; + int max_occ = 0; + for (Var v = 1; v <= specs.getNbVariable(); v++) { + if (!specs.isSelected(v)) { + break; + } + double diff = occurence_cnt[v] - avg_occ; + occ_var += diff * diff; + if (occurence_cnt[v] > max_occ) { + max_occ = occurence_cnt[v]; + } + } + occ_var = sqrt(occ_var / specs.getNbVariable()); + + int cost_nproj = 10; + + std::cout << "Avg " << avg_occ << std::endl; + std::cout << "Max " << max_occ << std::endl; + std::cout << "Var " << occ_var << std::endl; + std::cout << "NProj Cost: " << cost_nproj << std::endl; + for (Var v = 1; v <= specs.getNbVariable(); v++) { + if (specs.isSelected(v)) { + m_cost[v] = 1; + } else { + m_cost[v] = cost_nproj; + } + } +} +void HyperGraphExtractorDualProj::constructHyperGraph( + SpecManagerCnf &om, std::vector &component, + std::vector &equivClass, std::vector> &equivVar, + bool reduceFormula, std::vector &considered, HyperGraph &hypergraph) { + unsigned pos = 0; + m_idxClauses.resize(0); + hypergraph.setSize(0); + // std::cout << "Cost " << m_nProjCost << std::endl; + + // first considere the equivalence. + + for (auto &vec : equivVar) { + unsigned &size = hypergraph[pos++]; + size = 0; + int cost = m_nproj_cost; + + for (auto &v : vec) { + if (om.varIsAssigned(v)) + continue; + + cost = std::min(cost, m_specs.isSelected(v) ? 1 : m_nproj_cost); + assert(!m_markedVar[v]); + for (auto l : {Lit::makeLitFalse(v), Lit::makeLitTrue(v)}) { + IteratorIdxClause listIdx = om.getVecIdxClauseNotBin(l); + for (int *ptr = listIdx.start; ptr != listIdx.end; ptr++) { + int idx = *ptr; + if (!m_markedClauses[idx]) { + m_markedClauses[idx] = true; + m_unmarkSet.push_back(idx); + hypergraph[pos++] = idx; + size++; + } + } + + listIdx = om.getVecIdxClauseBin(l); + for (int *ptr = listIdx.start; ptr != listIdx.end; ptr++) { + int idx = *ptr; + if (!m_markedClauses[idx]) { + m_markedClauses[idx] = true; + m_unmarkSet.push_back(idx); + hypergraph[pos++] = idx; + size++; + } + } + } + m_markedVar[v] = true; + } + + for (auto &idx : m_unmarkSet) { + if (!m_keepClause[idx]) { + m_keepClause[idx] = true; + m_idxClauses.push_back(idx); + } + m_markedClauses[idx] = false; + } + m_unmarkSet.resize(0); + assert(equivClass[vec.back()] == vec.back()); + + if (!size) + pos--; + else { + + hypergraph.getCost()[hypergraph.getSize()] = cost; + hypergraph.incSize(); + considered.push_back(vec.back()); + } + } + + // next consider the remaining variables (unmarked). + for (auto &v : component) { + if (m_markedVar[v] || om.varIsAssigned(v)) + continue; + m_markedVar[v] = true; + + unsigned &size = hypergraph[pos++]; + size = 0; + + for (auto l : {Lit::makeLitFalse(v), Lit::makeLitTrue(v)}) { + IteratorIdxClause listIdx = om.getVecIdxClauseNotBin(l); + for (int *ptr = listIdx.start; ptr != listIdx.end; ptr++) { + int idx = *ptr; + if (!m_keepClause[idx]) { + m_keepClause[idx] = true; + m_idxClauses.push_back(idx); + } + hypergraph[pos++] = idx; + size++; + } + + listIdx = om.getVecIdxClauseBin(l); + for (int *ptr = listIdx.start; ptr != listIdx.end; ptr++) { + int idx = *ptr; + if (!m_keepClause[idx]) { + m_keepClause[idx] = true; + m_idxClauses.push_back(idx); + } + hypergraph[pos++] = idx; + size++; + } + } + + if (!size) + pos--; + else { + hypergraph.getCost()[hypergraph.getSize()] = m_specs.isSelected(v) ? 1 : m_nproj_cost; + hypergraph.incSize(); + considered.push_back(v); + } + } + + // unmark. + for (auto &v : component) + m_markedVar[v] = false; + + // remove useless edges. + if (reduceFormula) + reduceHyperGraph(om, hypergraph, considered, m_idxClauses, equivClass); + + // unmark. + for (auto &idx : m_idxClauses) + m_keepClause[idx] = false; +} +} // namespace d4 diff --git a/src/hyperGraph/HyperGraphExtractorDualProj.hpp b/src/hyperGraph/HyperGraphExtractorDualProj.hpp new file mode 100644 index 00000000..c992f167 --- /dev/null +++ b/src/hyperGraph/HyperGraphExtractorDualProj.hpp @@ -0,0 +1,49 @@ + +/* + * d4 + * Copyright (C) 2020 Univ. Artois & CNRS + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with this program. If not, see . + */ + +#pragma once + +#include +#include + +#include "HyperGraph.hpp" +#include "HyperGraphExtractor.hpp" +#include "HyperGraphExtractorDual.hpp" +#include "src/problem/ProblemTypes.hpp" +#include "src/specs/cnf/SpecManagerCnf.hpp" +namespace d4 { +class HyperGraphExtractorDualProj : public HyperGraphExtractorDual { +private: + void compute_stats(SpecManagerCnf& specs); + std::vector m_cost; + SpecManagerCnf& m_specs; + int m_nproj_cost; + +public: + HyperGraphExtractorDualProj(unsigned nbVar, unsigned nbClause, SpecManagerCnf& specs,int nproj_cost=100); + + void constructHyperGraph(SpecManagerCnf &om, std::vector &component, + std::vector &equivClass, + std::vector> &equivVar, + bool reduceFormula, std::vector &considered, + HyperGraph &hypergraph); + + +}; +} // namespace d4 diff --git a/src/methods/CountingOperation.hpp b/src/methods/CountingOperation.hpp index b1076a03..86f01569 100644 --- a/src/methods/CountingOperation.hpp +++ b/src/methods/CountingOperation.hpp @@ -16,25 +16,274 @@ * along with this program. If not, see . */ #pragma once + +#include #include #include #include #include "DataBranch.hpp" #include "src/exceptions/BadBehaviourException.hpp" +#include <3rdParty/glucose-3.0/mtl/Vec.h> +#include +#include +#include +#include +#include +#include +#include +#include + +using namespace std::chrono_literals; +template struct overloaded : Ts... { + using Ts::operator()...; +}; namespace d4 { -template -class Operation; -template -class CountingOperation : public Operation { - private: +template class Operation; +template +class PersistentNodesOperation : public Operation { +private: + ProblemManager *m_problem; + struct AndNode { + size_t id; + std::vector children; + }; + struct OrNode { + size_t id; + DataBranch b[2]; + }; + struct UnaryNode { + size_t id; + DataBranch b; + }; + enum NodeTypeID : char { + True = 1, + False = 2, + And = 3, + Or = 3, + Arc = 4, + ArcAnd = 4, + }; + using Node = std::variant; + std::vector out; + std::atomic *> to_write; + std::atomic end; + std::thread writer; + std::atomic_bool idx; + + size_t index = 3; + + const size_t top = 1; + const size_t bottom = 2; + +public: + PersistentNodesOperation() = delete; + ~PersistentNodesOperation() { + while (to_write.load() != nullptr) { + std::this_thread::sleep_for(10ms); + } + to_write.exchange(new std::vector(std::move(out))); + end.store(true); + writer.join(); + } + + /** + Constructor. + + @param[in] problem, allows to get information about the problem such as + weights. + */ + PersistentNodesOperation(ProblemManager *problem, std::string filename) + : m_problem(problem), to_write(0), end(false) { + writer = std::thread([&,filename] { + std::cout << "Start writer" << std::endl; + std::ofstream file = + std::ofstream(filename, std::ios_base::out | std::ios_base::binary); + boost::iostreams::filtering_streambuf outbuf; + outbuf.push(boost::iostreams::gzip_compressor()); + outbuf.push(file); + std::ostream out(&outbuf); + out << NodeTypeID::True << uint64_t(1); + out << NodeTypeID::False << uint64_t(2); + auto write_arc = [&](DataBranch &b, size_t parent) { + out << NodeTypeID::Arc << uint64_t(parent) << uint64_t(b.d) + << (uint32_t)b.unitLits.size(); + for (auto i : b.unitLits) { + if (i.sign()) { + out << -int32_t(i.var()); + } else { + out << int32_t(i.var()); + } + } + }; + auto try_write = [&](std::vector *buf) { + if (!buf) { + return; + } + for (Node &n : *buf) { + std::visit(overloaded{[&](AndNode &arg) { + out << NodeTypeID::And << arg.id; + for (unsigned i = 0; i < arg.children.size(); + i++) { + out << NodeTypeID::ArcAnd << arg.id + << arg.children[i] << std::endl; + } + }, + [&](OrNode &arg) { + out << NodeTypeID::Or << arg.id; + for (int i = 0; i < 2; i++) { + write_arc(arg.b[i], arg.id); + } + }, + [&](UnaryNode &arg) { + out << NodeTypeID::Or << arg.id; + write_arc(arg.b, arg.id); + }}, + n); + } + std::cout << "Writen chunck" << std::endl; + delete buf; + }; + while (!end.load()) { + std::vector *buf = to_write.exchange(nullptr); + if (!buf) { + std::this_thread::sleep_for(10ms); + continue; + } + try_write(buf); + } + try_write(to_write.load()); + boost::iostreams::close(outbuf); // Don't forget this! + file.close(); + std::cout << "Done writer" << std::endl; + }); + + } // constructor. + + /** + Compute the sum of the given elements. + + @param[in] elts, the elements we want to get the product. + @param[in] size, the number of elements. + + \return the product of each element of elts. + */ + size_t manageDeterministOr(DataBranch *elts, unsigned size) final { + assert(size == 2); + size_t id = index++; + OrNode data{id, {}}; + out.emplace_back(); + for (int i = 0; i < size; i++) { + data.b[i] = std::move(elts[i]); + } + if (out.size() > 1000000 && to_write.load() == nullptr) { + std::vector *tmp = new std::vector(std::move(out)); + to_write.exchange(tmp); + std::cout << "Swap Buffers" << std::endl; + } + out.push_back(std::move(data)); + return id; + } // manageDeterministOr + + /** + Compute the product of the given elements. + + @param[in] elts, the elements we want to get the product. + @param[in] size, the number of elements. + + \return the product of each element of elts. + */ + size_t manageDecomposableAnd(size_t *elts, unsigned size) final { + size_t id = index++; + AndNode node{id, std::vector(size)}; + for (unsigned i = 0; i < size; i++) { + node.children[i] = std::move(elts[i]); + } + out.push_back(std::move(node)); + return id; + } // manageDecomposableAnd + + /** + Manage the case where the problem is unsatisfiable. + + \return 0 as number of models. + */ + size_t manageBottom() final { return bottom; } // manageBottom + + /** + Return false, that is given by the value 1. + + \return T(0). + */ + inline size_t createBottom() { return bottom; } + + /** + Manage the case where the problem is a tautology. + + @param[in] component, the current set of variables (useless here). + + \return 0 as number of models. + */ + inline size_t manageTop(std::vector &component)final { return top; } + + /** + Return true, that is given by the value 1. + + \return T(1). + */ + inline size_t createTop() final { return top; } + + /** + Manage the case where we only have a branch in our OR gate. + + @param[in] e, the branch we are considering. + + \return the number of models associate to the given branch. + */ + size_t manageBranch(DataBranch &e) final { + size_t node = index++; + out.push_back(UnaryNode{node, std::move(e)}); + return node; + + } // manageBranch + + /** + Manage the final result compute. + + @param[in] result, the result we are considering. + @param[in] config, the configuration that describes what we want to do on the + given result. + @param[in] out, the output stream. + */ + void manageResult(size_t &result, Config &config, std::ostream &out) { + out.flush(); + } // manageResult + + /** + Count the number of model, for this case that means doing noting. + + \return the number of models. + */ + T count(size_t &result) { return 0; } // count + + /** + Cannot be called, then throws an exception! + */ + T count(size_t &result, std::vector &assum) { + throw(BadBehaviourException( + "This operation is not allowed in this context.", __FILE__, __LINE__)); + } // count +}; + +template class CountingOperation : public Operation { +private: ProblemManager *m_problem; const T top = T(1); const T bottom = T(0); - public: +public: CountingOperation() = delete; /** @@ -44,7 +293,7 @@ class CountingOperation : public Operation { weights. */ CountingOperation(ProblemManager *problem) - : m_problem(problem) {} // constructor. + : m_problem(problem) {} // constructor. /** Compute the sum of the given elements. @@ -60,7 +309,7 @@ class CountingOperation : public Operation { elts[0].freeVars) + elts[1].d * m_problem->computeWeightUnitFree(elts[1].unitLits, elts[1].freeVars); - } // manageDeterministOr + } // manageDeterministOr /** Compute the product of the given elements. @@ -71,20 +320,23 @@ class CountingOperation : public Operation { \return the product of each element of elts. */ T manageDecomposableAnd(T *elts, unsigned size) { - if (size == 1) return elts[0]; - if (size == 2) return elts[0] * elts[1]; + if (size == 1) + return elts[0]; + if (size == 2) + return elts[0] * elts[1]; T ret = 1; - for (unsigned i = 0; i < size; i++) ret = ret * elts[i]; + for (unsigned i = 0; i < size; i++) + ret = ret * elts[i]; return ret; - } // manageDecomposableAnd + } // manageDecomposableAnd /** Manage the case where the problem is unsatisfiable. \return 0 as number of models. */ - T manageBottom() { return bottom; } // manageBottom + T manageBottom() { return bottom; } // manageBottom /** Return false, that is given by the value 1. @@ -118,29 +370,33 @@ class CountingOperation : public Operation { */ T manageBranch(DataBranch &e) { return e.d * m_problem->computeWeightUnitFree(e.unitLits, e.freeVars); - } // manageBranch + } // manageBranch /** Manage the final result compute. @param[in] result, the result we are considering. - @param[in] config, the configuration. + @param[in] config, the configuration that describes what we want to do on the + given result. @param[in] out, the output stream. */ void manageResult(T &result, Config &config, std::ostream &out) { - if (config.output_format == "competition") { + std::string format = config.keyword_output_format_solution; + std::string outFormat = config.output_format; + + if (outFormat == "competition") { boost::multiprecision::mpf_float::default_precision(128); out.precision(std::numeric_limits< boost::multiprecision::cpp_dec_float_50>::digits10); if (result == 0) { out << "s UNSATISFIABLE\n"; - out << "c " << config.keyword_output_format_solution << "\n"; + out << "c " << format << "\n"; out << "c s log10-estimate -inf\n"; out << "c s exact quadruple int 0\n"; } else { out << "s SATISFIABLE\n"; - out << "c " << config.keyword_output_format_solution << "\n"; + out << "c " << format << "\n"; out << "c s log10-estimate " << boost::multiprecision::log10( boost::multiprecision::cpp_dec_float_100(result)) @@ -151,18 +407,18 @@ class CountingOperation : public Operation { out << "c s exact arb int " << result << "\n"; } } else { - assert(config.output_format == "classic"); - out << config.keyword_output_format_solution << " "; + assert(outFormat == "classic"); + out << format << " "; out << std::fixed << std::setprecision(50) << result << "\n"; } - } // manageResult + } // manageResult /** Count the number of model, for this case that means doing noting. \return the number of models. */ - T count(T &result) { return result; } // count + T count(T &result) { return result; } // count /** Cannot be called, then throws an exception! @@ -170,7 +426,7 @@ class CountingOperation : public Operation { T count(T &result, std::vector &assum) { throw(BadBehaviourException( "This operation is not allowed in this context.", __FILE__, __LINE__)); - } // count + } // count }; -} // namespace d4 +} // namespace d4 diff --git a/src/methods/MethodManager.cpp b/src/methods/MethodManager.cpp index 62b0a624..c00d6abb 100644 --- a/src/methods/MethodManager.cpp +++ b/src/methods/MethodManager.cpp @@ -25,6 +25,7 @@ #include "MaxSharpSAT.hpp" #include "MinSharpSAT.hpp" #include "OperationManager.hpp" +#include "ProjDpllStyleMethod.hpp" #include "ProjMCMethod.hpp" #include "src/exceptions/BadBehaviourException.hpp" #include "src/exceptions/FactoryException.hpp" @@ -99,6 +100,19 @@ MethodManager *MethodManager::makeMethodManager(Config &config, config, meth, isFloat, runProblem, out, lastBreath); } + if (meth == "proj-ddnnf-compiler") { + if (!isFloat) + return new ProjDpllStyleMethod< + mpz::mpz_int, Node *, + DecisionDNNFOperation *>>( + config, meth, isFloat, runProblem, out, lastBreath); + else + return new ProjDpllStyleMethod< + mpz::mpf_float, Node *, + DecisionDNNFOperation *>>( + config, meth, isFloat, runProblem, out, lastBreath); + } + if (meth == "projMC") { if (!isFloat) return new ProjMCMethod(config, isFloat, runProblem, diff --git a/src/methods/ProjDpllStyleMethod.hpp b/src/methods/ProjDpllStyleMethod.hpp new file mode 100644 index 00000000..dc01012a --- /dev/null +++ b/src/methods/ProjDpllStyleMethod.hpp @@ -0,0 +1,704 @@ + +/* + * d4 + * Copyright (C) 2020 Univ. Artois & CNRS + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with this program. If not, see . + */ +#pragma once + +#include "src/heuristics/cnf/PartitioningHeuristicBipartiteDual.hpp" +#include +#include +#include +#include +#include +#include +#include + +#include "Counter.hpp" +#include "DataBranch.hpp" +#include "MethodManager.hpp" +#include "src/caching/CacheManager.hpp" +#include "src/caching/CachedBucket.hpp" +#include "src/caching/TmpEntry.hpp" +#include "src/heuristics/PartitioningHeuristic.hpp" +#include "src/heuristics/PhaseHeuristic.hpp" +#include "src/heuristics/ProjBackupHeuristic.hpp" +#include "src/heuristics/ScoringMethod.hpp" +#include "src/preprocs/PreprocManager.hpp" +#include "src/problem/ProblemManager.hpp" +#include "src/problem/ProblemTypes.hpp" +#include "src/solvers/WrapperSolver.hpp" +#include "src/specs/SpecManager.hpp" +#include "src/utils/MemoryStat.hpp" +#include "src/utils/Proj.hpp" + +#define NB_SEP_MC 104 +#define MASK_SHOWRUN_MC ((2 << 13) - 1) +#define WIDTH_PRINT_COLUMN_MC 12 +#define MASK_HEADER 1048575 + +#include "CountingOperation.hpp" +#include "DecisionDNNFOperation.hpp" +#include "OperationManager.hpp" +#include +template +auto since(std::chrono::time_point const &start) { + return std::chrono::duration_cast(clock_t::now() - start); +} + +namespace d4 { +namespace po = boost::program_options; +template class Counter; + +template +class ProjDpllStyleMethod : public MethodManager, public Counter { +private: + bool optDomConst; + bool optReversePolarity; + unsigned m_failed_cuts = 0; + unsigned m_nb_pure_lits = 0; + unsigned m_nbCallCall; + unsigned m_nbSplit; + unsigned m_callPartitioner; + unsigned m_nbDecisionNode; + unsigned m_optCached; + unsigned m_stampIdx; + unsigned m_decay_frequency; + bool m_isProjectedMode; + + void createOperation(Config &config) { + if constexpr (std::is_same_v>) { + m_operation = + new DecisionDNNFOperation(m_problem, m_specs, m_solver); + } + if constexpr (std::is_same_v>) { + m_operation = new PersistentNodesOperation( + m_problem, config.output); + } + if constexpr (std::is_same_v>) { + m_operation = new CountingOperation(m_problem); + } + } + + std::vector m_stampVar; + std::vector> m_clauses; + + std::vector m_currentPrioritySet; + + ProblemManager *m_problem; + WrapperSolver *m_solver; + SpecManager *m_specs; + ScoringMethod *m_hVar; + PhaseHeuristic *m_hPhase; + PartitioningHeuristic *m_hCutSet; + + TmpEntry NULL_CACHE_ENTRY; + CacheManager *m_cache; + std::ostream m_out; + bool m_panicMode; + + O *m_operation; + std::vector m_var_sign; + int m_freevars; + int64_t max_depth = 0; + int root_comp = -1; + int m_frequency = 0; + int m_min_depth = 100000000; + bool m_pure_lit_elim; + std::vector m_pure_lits; + +public: + /** + Constructor. + + @param[in] config, the configuration. + */ + ProjDpllStyleMethod(Config &config, std::string &meth, bool isFloat, + ProblemManager *initProblem, std::ostream &out, + LastBreathPreproc &lastBreath) + : m_problem(initProblem), m_out(nullptr) { + // init the output stream + m_out.copyfmt(out); + m_out.clear(out.rdstate()); + m_out.basic_ios::rdbuf(out.rdbuf()); + m_freevars = initProblem->freeVars(); + + // we create the SAT solver. + m_solver = WrapperSolver::makeWrapperSolver(config, m_out); + assert(m_solver); + m_panicMode = lastBreath.panic; + + m_solver->initSolver(*m_problem, lastBreath.learnt); + m_solver->setCountConflict(lastBreath.countConflict, 1, + m_problem->getNbVar()); + m_solver->setNeedModel(true); + m_decay_frequency = config.scoring_method_decay_freq; + + // we initialize the object that will give info about the problem. + m_specs = SpecManager::makeSpecManager(config, *m_problem, m_out); + assert(m_specs); + + // we initialize the object used to compute score and partition. + m_hVar = ScoringMethod::makeScoringMethod(config, *m_specs, *m_solver, m_out); + m_hPhase = + PhaseHeuristic::makePhaseHeuristic(config, *m_specs, *m_solver, m_out); + + m_isProjectedMode = true; + + // select the partitioner regarding if it projected model counting or not. + /* + if ((m_isProjectedMode = m_problem->getNbSelectedVar())) { + m_out << "c [MODE] projected\n"; + m_hCutSet = PartitioningHeuristic::makePartitioningHeuristicNone(m_out); + } else { + m_out << "c [MODE] classic\n"; + m_hCutSet = PartitioningHeuristic::makePartitioningHeuristic( + vm, *m_specs, *m_solver, m_out); + } + */ + + m_currentPrioritySet.resize(m_problem->getNbVar() + 1, false); + double projected_ratio = + double(m_specs->nbSelected()) / double(m_specs->getNbVariable()); + double clause_var_ratio = double(m_specs->nbSelected()) / + ((SpecManagerCnf *)m_specs)->getNbClause(); + if (projected_ratio<0.10 | clause_var_ratio> 0.5) { + m_hCutSet = PartitioningHeuristic::makePartitioningHeuristicNone(m_out); + } else { + m_hCutSet = PartitioningHeuristic::makePartitioningHeuristic( + config, *m_specs, *m_solver, m_out); + } + + assert(m_hVar && m_hPhase && m_hCutSet); + m_cache = CacheManager::makeCacheManager(config, m_problem->getNbVar(), + m_specs, m_out); + + // init the clock time. + initTimer(); + + m_optCached = config.cache_activated; + m_callPartitioner = 0; + m_nbDecisionNode = m_nbSplit = m_nbCallCall = 0; + m_stampIdx = 0; + m_stampVar.resize(m_specs->getNbVariable() + 1, 0); + createOperation(config); + m_out << "c\n"; + m_var_sign.resize(m_specs->getNbVariable() + 1, 0); + m_pure_lit_elim = config.projddnnf_pure_lit_elim; + + } // constructor + + /** + Destructor. + */ + ~ProjDpllStyleMethod() { + delete m_operation; + delete m_problem; + delete m_solver; + delete m_specs; + delete m_hVar; + delete m_hPhase; + delete m_hCutSet; + delete m_cache; + } // destructor + +private: + /** + Expel from a set of variables the ones they are marked as being decidable. + + @param[out] vars, the set of variables we search to filter. + + @param[in] isDecisionvariable, a boolean vector that marks as true decision + variables. + */ + void expelNoDecisionVar(std::vector &vars) { + + unsigned j = 0; + for (unsigned i = 0; i < vars.size(); i++) + if (m_specs->isSelected(vars[i])) + vars[j++] = vars[i]; + vars.resize(j); + } // expelNoDecisionVar + + /** + Expel from a set of variables the ones they are marked as being decidable. + + @param[out] lits, the set of literals we search to filter. + + @param[in] isDecisionvariable, a boolean vector that marks as true decision + variables. + */ + void expelNoDecisionLit(std::vector &lits) { + if (!m_isProjectedMode) + return; + + unsigned j = 0; + for (unsigned i = 0; i < lits.size(); i++) + if (m_specs->isSelected(lits[i].var())) + lits[j++] = lits[i]; + lits.resize(j); + } // expelNoDecisionLit + + /** + Compute the current priority set. + + @param[in] connected, the current component. + @param[in] priorityVar, the current priority variables. + @param[out] currPriority, the intersection of the two previous sets. + */ + inline void computePrioritySubSet(std::vector &connected, + std::vector &priorityVar, + std::vector &currPriority) { + currPriority.resize(0); + m_stampIdx++; + for (auto &v : connected) + m_stampVar[v] = m_stampIdx; + for (auto &v : priorityVar) + if (m_stampVar[v] == m_stampIdx && !m_specs->varIsAssigned(v)) + currPriority.push_back(v); + } // computePrioritySet + + /** + Print out information about the solving process. + + @param[in] out, the stream we use to print out information. + */ + inline void showInter(std::ostream &out) { + out << "c " << std::fixed << std::setprecision(2) << "|" + << std::setw(WIDTH_PRINT_COLUMN_MC) << getTimer() << "|" + << std::setw(WIDTH_PRINT_COLUMN_MC) << m_cache->getNbPositiveHit() + << "|" << std::setw(WIDTH_PRINT_COLUMN_MC) + << m_cache->getNbNegativeHit() << "|" + << std::setw(WIDTH_PRINT_COLUMN_MC) << m_cache->usedMemory() << "|" + << std::setw(WIDTH_PRINT_COLUMN_MC) << m_nbSplit << "|" + << std::setw(WIDTH_PRINT_COLUMN_MC) << MemoryStat::memUsedPeak() << "|" + << std::setw(WIDTH_PRINT_COLUMN_MC) << m_nbDecisionNode << "|" + << std::setw(WIDTH_PRINT_COLUMN_MC) << m_callPartitioner << "|" + << std::setw(WIDTH_PRINT_COLUMN_MC) << m_failed_cuts << "|" + << std::setw(WIDTH_PRINT_COLUMN_MC) << max_depth << "|" + << std::setw(WIDTH_PRINT_COLUMN_MC) << m_min_depth << "|\n"; + m_min_depth = 10000000; + } // showInter + + /** + Print out a line of dashes. + + @param[in] out, the stream we use to print out information. + */ + inline void separator(std::ostream &out) { + out << "c "; + for (int i = 0; i < NB_SEP_MC; i++) + out << "-"; + out << "\n"; + } // separator + + /** + Print out the header information. + + @param[in] out, the stream we use to print out information. + */ + inline void showHeader(std::ostream &out) { + separator(out); + out << "c " + << "|" << std::setw(WIDTH_PRINT_COLUMN_MC) << "time" + << "|" << std::setw(WIDTH_PRINT_COLUMN_MC) << "#posHit" + << "|" << std::setw(WIDTH_PRINT_COLUMN_MC) << "#negHit" + << "|" << std::setw(WIDTH_PRINT_COLUMN_MC) << "memory" + << "|" << std::setw(WIDTH_PRINT_COLUMN_MC) << "#split" + << "|" << std::setw(WIDTH_PRINT_COLUMN_MC) << "mem(MB)" + << "|" << std::setw(WIDTH_PRINT_COLUMN_MC) << "#dec. Node" + << "|" << std::setw(WIDTH_PRINT_COLUMN_MC) << "#cutter" + << "|" << std::setw(WIDTH_PRINT_COLUMN_MC) << "#bad cuts" + << "|" << std::setw(WIDTH_PRINT_COLUMN_MC) << "#depth" + << "|" << std::setw(WIDTH_PRINT_COLUMN_MC) << "#min depth" + << "|\n"; + separator(out); + } // showHeader + + /** + Print out information when it is requiered. + + @param[in] out, the stream we use to print out information. + */ + inline void showRun(std::ostream &out) { + if (!(m_nbCallCall & (MASK_HEADER))) + showHeader(out); + if (m_nbCallCall && !(m_nbCallCall & MASK_SHOWRUN_MC)) + showInter(out); + } // showRun + + /** + Print out the final stat. + + @param[in] out, the stream we use to print out information. + */ + inline void printFinalStats(std::ostream &out) { + separator(out); + out << "c\n"; + out << "c \033[1m\033[31mStatistics \033[0m\n"; + out << "c \033[33mCompilation Information\033[0m\n"; + out << "c Number of recursive call: " << m_nbCallCall << "\n"; + out << "c Number of split formula: " << m_nbSplit << "\n"; + out << "c Number of decision: " << m_nbDecisionNode << "\n"; + out << "c Number of paritioner calls: " << m_callPartitioner << "\n"; + out << "c Number of bad cuts " << m_failed_cuts << "\n"; + out << "c Number of pure lits " << m_nb_pure_lits << "\n"; + + out << "c\n"; + m_cache->printCacheInformation(out); + if (m_hCutSet) { + out << "c\n"; + m_hCutSet->displayStat(out); + } + out << "c Final time: " << getTimer() << "\n"; + out << "c\n"; + } // printFinalStat + + /** + Initialize the assumption in order to compute compiled formula under this + one. + + @param[in] assums, the assumption + */ + inline void initAssumption(std::vector &assums) { + m_solver->restart(); + m_solver->popAssumption(m_solver->getAssumption().size()); + m_solver->setAssumption(assums); + } // initAssumption + + /** + Decide if the cache is realized or not. + */ + bool cacheIsActivated(std::vector &connected) { + if (!m_optCached) + return false; + return m_cache->isActivated(connected.size()); + } // cacheIsActivated + + /** + Call the CNF formula into a FBDD. + + @param[in] setOfVar, the current set of considered variables + @param[in] unitsLit, the set of unit literal detected at this level + @param[in] freeVariable, the variables which become free + @param[in] out, the stream we use to print out information. + + \return an element of type U that sums up the given CNF sub-formula using a + DPLL style algorithm with an operation manager. + */ + bool onlyExtra(const std::vector &connected, + const std::vector &isDecisionVariable) { + bool ok = true; + for (int i = 0; i < connected.size(); i++) { + ok &= !isDecisionVariable[connected[i]]; + } + + return ok; + } + U compute_(ProjVars &setOfVar, std::vector &unitsLit, + std::vector &freeVariable, std::ostream &out) { + showRun(out); + m_nbCallCall++; + + if (!m_solver->solve(setOfVar.vars)) { + + return m_operation->manageBottom(); + } + + m_solver->whichAreUnits(setOfVar.vars, unitsLit); // collect unit literals + + m_pure_lits.clear(); + if (m_pure_lit_elim && setOfVar.nbProj > 10) { + m_specs->preUpdate(unitsLit, m_pure_lits); + + } else { + m_specs->preUpdate(unitsLit); + } + + int nbPure = 0; + if (m_pure_lits.size()) { + for (auto l : m_pure_lits) { + if (!m_specs->litIsAssigned(l)) { + m_solver->pushAssumption(l); + nbPure++; + m_nb_pure_lits++; + } + } + } + + // compute the connected composant + std::vector varConnected; + int nbComponent = m_specs->computeConnectedComponent( + varConnected, setOfVar.vars, freeVariable); + expelNoDecisionVar(freeVariable); + if (setOfVar.nbProj != setOfVar.vars.size()) { + varConnected.erase( + std::partition(varConnected.begin(), varConnected.end(), + [&](const ProjVars &comp) { return comp.nbProj > 0; }), + varConnected.end()); + } + /* + std::sort(varConnected.begin(), varConnected.end(), + [](ProjVars &a, ProjVars &b) { + bool clean_a = a.vars.size() == a.nbProj; + bool clean_b = b.vars.size() == b.nbProj; + return clean_a > clean_b; + }); + */ + nbComponent = varConnected.size(); + + // consider each connected component. + if (nbComponent) { + U tab[nbComponent]; + m_nbSplit += (nbComponent > 1) ? nbComponent : 0; + max_depth += 1; + for (int cp = 0; cp < nbComponent; cp++) { + ProjVars &connected = varConnected[cp]; + bool cacheActivated = cacheIsActivated(connected.vars); + + TmpEntry cb = cacheActivated ? m_cache->searchInCache(connected.vars) + : NULL_CACHE_ENTRY; + + if (cacheActivated && cb.defined) { + tab[cp] = cb.getValue(); + } else { + // recursive call + tab[cp] = computeDecisionNode(connected, out); + + if (cacheActivated) + m_cache->addInCache(cb, tab[cp]); + } + } + max_depth -= 1; + m_min_depth = std::min(max_depth, m_min_depth); + + if (nbPure) { + m_solver->popAssumption(nbPure); + } + + m_specs->postUpdate(unitsLit); + expelNoDecisionLit(unitsLit); + + return m_operation->manageDecomposableAnd(tab, nbComponent); + } // else we have a tautology + + if (nbPure) { + m_solver->popAssumption(nbPure); + } + + m_specs->postUpdate(unitsLit); + expelNoDecisionLit(unitsLit); + + return m_operation->createTop(); + } // compute_ + + /** + * @brief Set the Current Priority. + * + * @param cutSet is the set of variables that become decision variables. + */ + inline void setCurrentPriority(std::vector &cutSet) { + for (auto &v : cutSet) + if (m_specs->isSelected(v)) + m_currentPrioritySet[v] = true; + } // setCurrentPriority + + /** + * @brief Unset the Current Priority. + + * @param cutSet is the set of variables that become decision variables. + */ + inline void unsetCurrentPriority(std::vector &cutSet) { + for (auto &v : cutSet) + if (m_specs->isSelected(v)) + m_currentPrioritySet[v] = false; + } // setCurrentPriority + + /** + This function select a variable and compile a decision node. + + @param[in] connected, the set of variable present in the current problem. + @param[in] out, the stream whare are printed out the logs. + + \return the compiled formula. + */ + U computeDecisionNode(ProjVars &connected, std::ostream &out) { + std::vector cutSet; + bool hasPriority = false, hasVariable = false; + for (auto v : connected.vars) { + if (m_specs->varIsAssigned(v) || !m_specs->isSelected(v)) + continue; + hasVariable = true; + if ((hasPriority = m_currentPrioritySet[v])) + break; + } + bool cut_valid = false; + + if (hasVariable && !hasPriority && m_hCutSet->isReady(connected.vars)) { + m_hCutSet->computeCutSet(connected.vars, cutSet); + + for (int i = 0; i < cutSet.size(); i++) { + cut_valid |= m_specs->isSelected(cutSet[i]) && + !m_specs->varIsAssigned(cutSet[i]); + } + + // cut_valid = cutset_ok(connected, cutSet); + if (cut_valid) { + setCurrentPriority(cutSet); + } + m_callPartitioner++; + } + + // search the next variable to branch on + Var v; + if (cut_valid || hasPriority) { + v = m_hVar->selectVariable(connected.vars, [&](Var v) { + return m_currentPrioritySet[v] && !m_specs->varIsAssigned(v); + }); + } else { + m_failed_cuts += 1; + v = m_hVar->selectVariable(connected.vars, [&](Var v) { + return m_specs->isSelected(v) && !m_specs->varIsAssigned(v); + }); + } + + if (v == var_Undef) { + unsetCurrentPriority(cutSet); + return m_operation->manageTop(connected.vars); + } + + assert(m_specs->isSelected(v)); + + Lit l = Lit::makeLit(v, m_hPhase->selectPhase(v)); + m_nbDecisionNode++; + // manual decay frequency take from sharpsat-TD + // not sure if this is useful... + if (m_nbDecisionNode % m_decay_frequency == 0) { + m_hVar->decay(); + } + + // compile the formula where l is assigned to true + DataBranch b[2]; + + assert(!m_solver->isInAssumption(l.var())); + m_solver->pushAssumption(l); + b[0].d = compute_(connected, b[0].unitLits, b[0].freeVars, out); + m_solver->popAssumption(); + + if (m_solver->isInAssumption(l)) + b[1].d = m_operation->manageBottom(); + else if (m_solver->isInAssumption(~l)) + b[1].d = compute_(connected, b[1].unitLits, b[1].freeVars, out); + else { + m_solver->pushAssumption(~l); + b[1].d = compute_(connected, b[1].unitLits, b[1].freeVars, out); + m_solver->popAssumption(); + } + + unsetCurrentPriority(cutSet); + return m_operation->manageDeterministOr(b, 2); + } // computeDecisionNode + + /** + Compute U using the trace of a SAT solver. + + @param[in] setOfVar, the set of variables of the considered problem. + @param[in] out, the stream are is print out the logs. + @param[in] warmStart, to activate/deactivate the warm start strategy. + /!\ When the warm start is activated the assumptions are reset. + + \return an element of type U that sums up the given CNF formula using a + DPLL style algorithm with an operation manager. + */ + U compute(ProjVars &setOfVar, std::ostream &out, bool warmStart = true) { + if (setOfVar.nbProj == 0) { + + DataBranch b = {}; + b.d = m_operation->createTop(); + for (int i = m_problem->getNbVar() + 1; + i < m_problem->getNbVar() + 1 + m_freevars; i++) { + b.freeVars.push_back(i); + } + return m_operation->manageBranch(b); + } + if (m_problem->isUnsat() || + (warmStart && !m_panicMode && + !m_solver->warmStart(29, 11, setOfVar.vars, m_out))) + return m_operation->manageBottom(); + + DataBranch b; + b.d = compute_(setOfVar, b.unitLits, b.freeVars, out); + for (int i = m_problem->getNbVar() + 1; + i < m_problem->getNbVar() + 1 + m_freevars; i++) { + b.freeVars.push_back(i); + } + return m_operation->manageBranch(b); + } // compute + +public: + /** + Given an assumption, we compute the number of models. That is different + from the query strategy, where we first compute and then condition the + computed structure. + + @param[in] setOfVar, the set of variables of the considered problem. + @param[in] assumption, the set of literals we want to assign. + @param[in] out, the stream where are print out the log. + + \return the number of models when the formula is simplified by the given + assumption. + */ + T count(std::vector &setOfVar, std::vector &assumption, + std::ostream &out) { + initAssumption(assumption); + + // get the unit not in setOfVar. + std::vector shadowUnits; + m_stampIdx++; + for (auto &v : setOfVar) + m_stampVar[v] = m_stampIdx; + for (auto &l : assumption) + if (m_stampVar[l.var()] != m_stampIdx) + shadowUnits.push_back(l); + + m_specs->preUpdate(shadowUnits); + + ProjVars setOfVar_{setOfVar, m_specs->nbSelected()}; + U result = compute(setOfVar_, out, false); + m_specs->postUpdate(shadowUnits); + + return m_operation->count(result); + } // count + + /** + Run the DPLL style algorithm with the operation manager. + + @param[in] vm, the set of options. + */ + void run(Config &config) { + ProjVars setOfVar; + setOfVar.nbProj = m_specs->nbSelected(); + for (int i = 1; i <= m_specs->getNbVariable(); i++) + setOfVar.vars.push_back(i); + + U result = compute(setOfVar, m_out); + printFinalStats(m_out); + m_operation->manageResult(result, config, m_out); + } // run +}; +} // namespace d4 diff --git a/src/option.dsc b/src/option.dsc index a906259b..c0e67813 100644 --- a/src/option.dsc +++ b/src/option.dsc @@ -8,7 +8,14 @@ ("maxsharpsat-option-and-dig",boost::program_options::value()->default_value(true),"When a decomposable AND node occurs we search for an instantiation to be able to get a bound.") ("maxsharpsat-option-greedy-init",boost::program_options::value()->default_value(false),"Search for a first max interpretation greedily.") ("preproc,p",boost::program_options::value()->default_value("basic"), "The preprocessing technique we will use (basic, backbone).") +("preproc-equiv",boost::program_options::value()->default_value(true), "Dont allow variable elimination on none projected variables") +("preproc-ve-check",boost::program_options::value()->default_value(false), "recheck if a ve candidate") +("preproc-ve-only-simpical",boost::program_options::value()->default_value(true), "only apply ve to simpical") +("preproc-ve-prefer-simpical",boost::program_options::value()->default_value(false), "only apply ve to simpical") +("preproc-ve-limit",boost::program_options::value()->default_value(4), "ve occurrence limit") +("projddnnf-pure-lit-elim",boost::program_options::value()->default_value(true), "pure lit elim") ("scoring-method,sm",boost::program_options::value()->default_value("vsads"),"The scoring method used for selecting the next variable. [mom, dlcs, vsids, vsads, jwts]") +("scoring-method-decay-freq",boost::program_options::value()->default_value(300000),"decay ferquency") ("occurrence-manager,om",boost::program_options::value()->default_value("dynamic"),"The occurrence manager used. [add a description]") ("phase-heuristic,ph",boost::program_options::value()->default_value("polarity"),"The way the phase of the next decision is selected (false, true, polarity or occurrence).") ("partitioning-heuristic,pvh",boost::program_options::value()->default_value("decomposition-static-dual"),"The method used to compute a cut. [none, decomposition-static, bipartition-primal or bipartition-dual]") @@ -39,4 +46,5 @@ ("query,q", boost::program_options::value(), "Perform the queries given in a file (m l1 l2 ... ln 0 for a model counting query, and d l1 l2 ... ln 0 for a satisfiability query).") ("projMC-refinement", boost::program_options::value()->default_value(false), "Try to reduce the set of selector by computing a MSS.") ("keyword-output-format-solution", boost::program_options::value()->default_value("s"), "The keyword prints in front of the solution when it is printed out.") -("output-format", boost::program_options::value()->default_value("classic"), "The way the solution is printed out ('classic' only gives the number of solution after printing 's', 'competition' follows the MC competition 2021).") \ No newline at end of file +("output,o", boost::program_options::value()->default_value("a.ddnnf"), "Path to get the output file") +("output-format", boost::program_options::value()->default_value("classic"), "The way the solution is printed out ('classic' only gives the number of solution after printing 's', 'competition' follows the MC competition 2021).") diff --git a/src/preprocs/PreprocManager.cpp b/src/preprocs/PreprocManager.cpp index 2ed4ccd8..acf053d2 100644 --- a/src/preprocs/PreprocManager.cpp +++ b/src/preprocs/PreprocManager.cpp @@ -19,7 +19,9 @@ #include "cnf/PreprocBackboneCnf.hpp" #include "cnf/PreprocBasicCnf.hpp" +#include "cnf/PreprocProj.hpp" #include "src/exceptions/FactoryException.hpp" +#include "cnf/PreprocGPMC.hpp" namespace d4 { @@ -30,11 +32,16 @@ namespace d4 { */ PreprocManager *PreprocManager::makePreprocManager(Config &config, std::ostream &out) { - out << "c [CONSTRUCTOR] Preproc: " << config.method << " " << config.input_type << "\n"; + std::string meth = config.preproc; + std::string inputType = config.input_type; - if (config.input_type == "cnf" || config.input_type == "dimacs") { - if (config.preproc == "basic") return new PreprocBasicCnf(config, out); - if (config.preproc == "backbone") return new PreprocBackboneCnf(config, out); + out << "c [CONSTRUCTOR] Preproc: " << meth << " " << inputType << "\n"; + + if (inputType == "cnf" || inputType == "dimacs") { + if (meth == "basic") return new PreprocBasicCnf(config, out); + if (meth == "backbone") return new PreprocBackboneCnf(config, out); + if (meth == "proj") return new PreprocProj(config, out); + if (meth == "gpmc") return new PreprocGPMC(config, out); } throw(FactoryException("Cannot create a PreprocManager", __FILE__, __LINE__)); diff --git a/src/preprocs/PreprocManager.hpp b/src/preprocs/PreprocManager.hpp index 1fdfe274..9d1ec8da 100644 --- a/src/preprocs/PreprocManager.hpp +++ b/src/preprocs/PreprocManager.hpp @@ -16,16 +16,15 @@ * along with this program. If not, see . */ #pragma once - #include -#include "src/config/Config.hpp" #include "src/problem/ProblemManager.hpp" #include "src/problem/ProblemTypes.hpp" namespace d4 { struct LastBreathPreproc { std::vector countConflict; + std::vector> learnt; bool panic; inline void fitSizeCountConflict(unsigned size) { diff --git a/src/preprocs/cnf/PreprocGPMC.cpp b/src/preprocs/cnf/PreprocGPMC.cpp new file mode 100644 index 00000000..a64a8e09 --- /dev/null +++ b/src/preprocs/cnf/PreprocGPMC.cpp @@ -0,0 +1,61 @@ + +#include "PreprocGPMC.hpp" +#include "gpmc.hpp" + +namespace d4 { + +PreprocGPMC::PreprocGPMC(Config &config, std::ostream &out) { + + + + + ws = WrapperSolver::makeWrapperSolverPreproc(config, out); +} + +PreprocGPMC::~PreprocGPMC() { delete ws; } +ProblemManager *PreprocGPMC::run(ProblemManager *pin, + LastBreathPreproc &lastBreath) { + + ProblemManagerCnf *cnf = (ProblemManagerCnf *)pin; + + + + int vars = cnf->getNbVar(); + int pvars = cnf->getSelectedVar().size(); + int freevars =0; + std::vector asignes; + std::vector gmap; + std::vector> clauses = cnf->getClauses(); + if (!GPMC::simplify(clauses,pin->getSelectedVar(),lastBreath.learnt,vars,pvars,freevars,asignes,gmap,false,true)){ + return pin->getUnsatProblem(); + } + std::vector weight(vars+1+freevars,1.0); + std::vector weightLit((vars+1+freevars)*2,1.0); + std::vector selected; + for(Var i = 1;igetClauses() = std::move(clauses); + + ws->initSolver(*out); + lastBreath.panic = 0; + lastBreath.countConflict.resize(out->getNbVar() + 1, 0); + + if (!ws->solve()) return out->getUnsatProblem(); + lastBreath.panic = ws->getNbConflict() > 100000; + + // get the activity given by the solver. + for (unsigned i = 1; i <= out->getNbVar(); i++) + lastBreath.countConflict[i] = ws->getCountConflict(i); + + std::vector units; + ws->getUnits(units); + auto final = out->getConditionedFormula(units); + + delete out; + return final; +} + +} // namespace d4 diff --git a/src/preprocs/cnf/PreprocGPMC.hpp b/src/preprocs/cnf/PreprocGPMC.hpp new file mode 100644 index 00000000..3c4efd22 --- /dev/null +++ b/src/preprocs/cnf/PreprocGPMC.hpp @@ -0,0 +1,35 @@ +#pragma once +#include + +#include "src/preprocs/PreprocManager.hpp" +#include "3rdParty/glucose-3.0/core/Solver.h" +#include "src/problem/cnf/ProblemManagerCnf.hpp" + + + +namespace d4{ +// Use GPMCs preproc in D4 +class PreprocGPMC:public PreprocManager{ + + WrapperSolver *ws; + +public: + PreprocGPMC(Config &config, std::ostream &out); + virtual ~PreprocGPMC(); + + virtual ProblemManager *run(ProblemManager *pin, + LastBreathPreproc &lastBreath) override; + +}; +} + + + + +namespace gpmc { + + + + + +} diff --git a/src/preprocs/cnf/PreprocProj.cpp b/src/preprocs/cnf/PreprocProj.cpp new file mode 100644 index 00000000..c6ee898c --- /dev/null +++ b/src/preprocs/cnf/PreprocProj.cpp @@ -0,0 +1,142 @@ + +#include "PreprocProj.hpp" +#include "src/problem/cnf/ProblemManagerCnf.hpp" + +namespace d4 { + +/** + The constructor. + + @param[in] vm, the options used (solver). + */ +PreprocProj::PreprocProj(Config &d4Config, std::ostream &out) { + + ws = WrapperSolver::makeWrapperSolverPreproc(d4Config, out); + config.ve_dve = d4Config.preproc_equiv; + config.ve_check = d4Config.preproc_ve_check; + config.ve_only_simpical = d4Config.preproc_ve_only_simpical; + config.ve_prefer_simpical = d4Config.preproc_ve_prefer_simpical; + config.ve_limit = d4Config.preproc_ve_limit; + keep_map = false; +} // constructor + +/** + Destructor. + */ +PreprocProj::~PreprocProj() { delete ws; } // destructor + +/** + * @brief The preprocessing itself. + * @param[out] p, the problem we want to preprocess. + * @param[out] lastBreath gives information about the way the preproc sees + * the problem. + */ + +ProblemManager *PreprocProj::run(ProblemManager *pin, + LastBreathPreproc &lastBreath) { + + // TODO remove, only for testing + if (pin->getSelectedVar().empty()) { + for (int i = 1; i <= pin->getNbVar(); i++) { + pin->getSelectedVar().push_back(i); + } + } + ProblemManagerCnf *in = (ProblemManagerCnf *)pin; + using namespace PRE; + Instance ins; + ins.weighted = false; + ins.vars = in->getNbVar(); + ins.npvars = in->getNbSelectedVar(); + ins.projected = ins.vars != ins.npvars; + ins.ispvars.resize(ins.vars, false); + ins.assigns.resize(ins.vars, Glucose::l_Undef); + for (auto v : in->getSelectedVar()) { + ins.pvars.push_back(v - 1); + ins.ispvars[v - 1] = true; + } + for (auto &cl : in->getClauses()) { + std::vector lits(cl.size()); + for (int i = 0; i < cl.size(); i++) { + lits[i] = Glucose::mkLit(cl[i].var() - 1, cl[i].sign()); + } + ins.addClause(lits, false); + } + if (ins.projected) { + for (auto v : ins.pvars) + ins.gmap.push_back(Glucose::mkLit(v)); + } else { + for (int i = 0; i < ins.npvars; i++) + ins.gmap.push_back(Glucose::mkLit(i)); + } + ins.keepVarMap = keep_map; + + + Preprocessor preproc; + preproc.setConfig(config); + + preproc.Simplify(&ins); + if (ins.unsat) { + return in->getUnsatProblem(); + } + std::vector weight(ins.vars + ins.freevars + 2, 2.0); + std::vector weightLit((ins.vars + ins.freevars + 2) << 2, 1.0); + for (unsigned i = 0; i <= ins.vars + ins.freevars; i++) + weight[i] = weightLit[i << 1] + weightLit[(i << 1) + 1]; + std::vector selected; + for (Var i = 1; i <= ins.npvars; i++) { + selected.push_back(i); + } + ProblemManagerCnf *out = new ProblemManagerCnf(ins.vars, weightLit, weight, + selected, ins.freevars); + + if (keep_map) { + out->gmap().resize(ins.gmap.size()); + for (int i = 0; i < ins.gmap.size(); i++) { + if (ins.gmap[i] == Glucose::lit_Undef) { + out->gmap()[i] = lit_Undef; + } else { + out->gmap()[i] = Lit::makeLit(Glucose::var(ins.gmap[i]) + 1, + Glucose::sign(ins.gmap[i])); + } + } + std::cout<<"Fixed Lits: "< clause(cl.size()); + for (int i = 0; i < cl.size(); i++) { + clause[i] = Lit::makeLit(Glucose::var(cl[i]) + 1, Glucose::sign(cl[i])); + } + out->getClauses().push_back(clause); + } + for (auto &cl : ins.learnts) { + std::vector clause(cl.size()); + for (int i = 0; i < cl.size(); i++) { + clause[i] = Lit::makeLit(Glucose::var(cl[i]) + 1, Glucose::sign(cl[i])); + } + lastBreath.learnt.push_back(clause); + } + ws->initSolver(*out); + lastBreath.panic = 0; + lastBreath.countConflict.resize(out->getNbVar() + 1, 0); + + if (!ws->solve()) + return out->getUnsatProblem(); + lastBreath.panic = ws->getNbConflict() > 100000; + + // get the activity given by the solver. + for (unsigned i = 1; i <= out->getNbVar(); i++) + lastBreath.countConflict[i] = ws->getCountConflict(i); + + std::vector units; + ws->getUnits(units); + auto final = out->getConditionedFormula(units); + + delete out; + return final; + +} // run +} // namespace d4 diff --git a/src/preprocs/cnf/PreprocProj.hpp b/src/preprocs/cnf/PreprocProj.hpp new file mode 100644 index 00000000..5adf74fd --- /dev/null +++ b/src/preprocs/cnf/PreprocProj.hpp @@ -0,0 +1,25 @@ +#include + +#pragma once + +#include + +#include "../PreprocManager.hpp" +#include "src/solvers/WrapperSolver.hpp" +#include "util/PreprocGPMC.hpp" +// Preprocessor based on gpmc and sharpsat-td with +// custom partial resolution as explained in the thesis +namespace d4 { +class PreprocProj : public PreprocManager { +private: + WrapperSolver *ws; + PRE::ConfigPreprocessor config; + bool keep_map; + +public: + PreprocProj(Config &config, std::ostream &out); + ~PreprocProj(); + virtual ProblemManager *run(ProblemManager *pin, + LastBreathPreproc &lastBreath) override; +}; +} // namespace d4 diff --git a/src/preprocs/cnf/util/PreprocGPMC.cpp b/src/preprocs/cnf/util/PreprocGPMC.cpp new file mode 100644 index 00000000..4ee5ed96 --- /dev/null +++ b/src/preprocs/cnf/util/PreprocGPMC.cpp @@ -0,0 +1,946 @@ +#include "PreprocGPMC.hpp" +#include "arjun/arjun.h" +#include "3rdParty/glucose-3.0/utils/System.h" +#include "lib_sharpsat_td/subsumer.hpp" + +#include +#include +#include + + + +using namespace PRE; +using namespace Glucose; +using namespace std; + +template +inline Glucose::lbool Instance::value(Glucose::Var x) const { + return assigns[x]; +} +template +inline Glucose::lbool Instance::value(Glucose::Lit p) const { + return assigns[var(p)] ^ sign(p); +} + +template +Instance::Instance() + : vars(0), weighted(false), projected(false), npvars(0), freevars(0), + gweight(1), keepVarMap(false), unsat(false) {} + +template +bool Instance::addClause(vector &ps, bool learnt) { + sort(ps.begin(), ps.end()); + + vec oc; + oc.clear(); + + Lit p; + int i, j, flag = 0; + + for (i = j = 0, p = lit_Undef; i < ps.size(); i++) + if (value(ps[i]) == l_True || ps[i] == ~p) + return true; + else if (value(ps[i]) != l_False && ps[i] != p) + ps[j++] = p = ps[i]; + ps.resize(j); + + if (ps.size() == 0) { + unsat = true; + return false; + } else if (ps.size() == 1) { + assigns[var(ps[0])] = lbool(!sign(p)); + assignedLits.push_back(ps[0]); + // No check by UP here. Preprocessor will do later. + } else { + clauses.push_back({}); + copy(ps.begin(), ps.end(), back_inserter(clauses.back())); + } + return true; +} + +const Var var_Determined = {-2}; + +// Preprocessor +template +bool Preprocessor::Simplify(Instance *instance) { + ins = instance; + + printCNFInfo("Init", true); + + if (ins->unsat || !SAT_FLE()) + return false; + + if (ins->vars > config.varlimit) + return true; + + if (config.cs) + Strengthen(); + + int start_cls = ins->clauses.size(); + + for (int i = 0; i < config.reps; i++) { + int vars = ins->vars; + int cls = ins->clauses.size(); + + if (cpuTime() > config.timelim) + break; + + if (config.ee) + MergeAdjEquivs(); + if (config.ve) { + if (ins->projected) + VariableEliminate(false); + if (config.ve_dve) { + VariableEliminate(true); + } + } + if (config.cs) + Strengthen(); + + if (cpuTime() > config.timelim || + ((vars == ins->vars) && (cls == ins->clauses.size())) || + (ins->clauses.size() > (double)1.1 * start_cls)) + break; + } + + int learnts = ins->learnts.size(); + for (int i = ins->learnts.size() - 1; i >= 0; i--) { + vector &clause = ins->learnts[i]; + if (clause.size() > 3) + sharpsat_td::SwapDel(ins->learnts, i); + } + if (cpuTime() < config.timelim) + SAT_FLE(); + + if (learnts * 3 / 2 < ins->learnts.size()) { + if (ins->vars > 0) { + int m = ins->clauses.size() / ins->vars; + int len = std::max(m + 1, 3); + for (int i = ins->learnts.size() - 1; i >= 0; i--) { + vector &clause = ins->learnts[i]; + if (clause.size() > len) + sharpsat_td::SwapDel(ins->learnts, i); + } + } + } + + printCNFInfo("Simp"); + + ins = NULL; + + return true; +} + +template bool Preprocessor::SAT_FLE() { + TestSolver S(ins->vars, ins->clauses, ins->learnts, ins->assignedLits); + + if (!S.okay()) + return false; + + if (!S.FailedLiterals() || S.Solve() == l_False) { + ins->unsat = true; + return false; + } + + S.exportLearnts(ins->learnts); + Compact(S.getAssigns()); + sharpsat_td::SortAndDedup(ins->clauses); + sharpsat_td::SortAndDedup(ins->learnts); + Subsume(); + + if (config.verb >= 1) + printCNFInfo("SAT_FLE"); + + return true; +} + +template bool Preprocessor::Strengthen() { + TestSolver S(ins->vars, ins->clauses, ins->learnts, ins->assignedLits); + bool removecl = false; + bool removelit = false; + + for (int i = ins->clauses.size() - 1; i >= 0; i--) { + vec assump; + + for (int j = ins->clauses[i].size() - 1; j >= 0; j--) { + assump.clear(); + removelit = false; + + for (int k = 0; k < ins->clauses[i].size(); k++) { + Lit l = ins->clauses[i][k]; + if (S.value(l) == l_True) { + removecl = true; + break; + } + if (k == j) { + if (S.value(l) == l_False) { + removelit = true; + break; + } + } else if (S.value(l) == l_Undef) { + assump.push(~l); + } + } + if (removecl) + break; + + if (removelit || S.falsifiedBy(assump)) { + for (int k = j + 1; k < ins->clauses[i].size(); k++) + ins->clauses[i][k - 1] = ins->clauses[i][k]; + ins->clauses[i].pop_back(); + + if (ins->clauses[i].size() == 1) { + S.assign(ins->clauses[i][0]); + S.bcp(); // no conflict because SAT test was already passed. + removecl = true; + break; + } + } + } + if (removecl) { + sharpsat_td::SwapDel(ins->clauses, i); + removecl = false; + } + } + + S.exportLearnts(ins->learnts); + Compact(S.getAssigns()); + sharpsat_td::SortAndDedup(ins->clauses); + sharpsat_td::SortAndDedup(ins->learnts); + Subsume(); + + if (config.verb >= 1) + printCNFInfo("ClStrg"); + + return true; +} + +template bool Preprocessor::MergeAdjEquivs() { + // This merges equivalent adjacent literals. + // The equivalence check is lazy, using unit propagation not Sat solving. + + Identifier Id(ins->vars); + { + vector adjmat; + adjmat.resize(ins->vars); + for (int i = 0; i < ins->vars; i++) + adjmat[i] = sharpsat_td::Bitset(ins->vars); + + for (const auto &cls : {ins->clauses, ins->learnts}) { + for (const auto &clause : cls) + for (int i = 0; i < clause.size(); i++) + for (int j = i + 1; j < clause.size(); j++) { + Var v1 = var(clause[i]); + Var v2 = var(clause[j]); + if (!adjmat[v1].Get(v2)) { + adjmat[v1].SetTrue(v2); + adjmat[v2].SetTrue(v1); + } + } + } + + // + // assert: any projected var idx < any non-projceted var idx + // + + TestSolver S(ins->vars, ins->clauses, ins->learnts, ins->assignedLits); + Glucose::vec &trail = S.getTrail(); + + for (Var v1 = 0; v1 < ins->vars; v1++) { + for (Var v2 = v1 + 1; v2 < ins->vars; v2++) { + if (!adjmat[v1].Get(v2)) + continue; + + Lit l1 = mkLit(v1); + Lit l2 = mkLit(v2); + + if (S.value(l1) != l_Undef) + break; + if (S.value(l2) != l_Undef) + continue; + + int pos = trail.size(); + + if (S.falsifiedBy(l1, l2) && S.falsifiedBy(~l1, ~l2)) { + Id.identify(l1, ~l2); + } else if (S.falsifiedBy(l1, ~l2) && S.falsifiedBy(~l1, l2)) { + Id.identify(l1, l2); + } + + if (trail.size() - pos > 0) { + int ppos = pos; + int cpos = trail.size(); + + while (ppos < cpos) { + for (int i = ppos; i < cpos; i++) { + int idx = Id.getIndex(trail[i]); + if (idx == -1) { + S.assign(trail[i]); + } else { + for (Lit l : Id.getEquivClasses()[idx]) + S.assign(l); + } + S.bcp(); + + Id.removeEquivClass(trail[i]); + } + ppos = cpos; + cpos = trail.size(); + } + for (int i = pos; i < trail.size(); i++) + ins->assignedLits.push_back(trail[i]); + } + } + } + } + + bool subsump = false; + if (Id.hasEquiv()) { + vector map(2 * ins->vars); + int new_id = 0; + for (int i = 0; i < ins->vars; i++) { + Lit dl = Id.delegateLit(mkLit(i)); + Lit l = mkLit(i); + + if (mkLit(i) == dl) { + Lit newlit = mkLit(new_id); + map[toInt(l)] = newlit; + map[toInt(~l)] = ~newlit; + if (ins->weighted && i < ins->npvars) { + ins->lit_weights[toInt(newlit)] = ins->lit_weights[toInt(l)]; + ins->lit_weights[toInt(~newlit)] = ins->lit_weights[toInt(~l)]; + } + new_id++; + } else { + Lit newlit = map[toInt(dl)]; + map[toInt(l)] = newlit; + map[toInt(~l)] = ~newlit; + if (ins->weighted && i < ins->npvars) { + ins->lit_weights[toInt(newlit)] *= ins->lit_weights[toInt(l)]; + ins->lit_weights[toInt(~newlit)] *= ins->lit_weights[toInt(~l)]; + } + } + if (i == ins->npvars - 1) + ins->npvars = new_id; + } + ins->vars = new_id; + ins->ispvars.clear(); + ins->ispvars.resize(ins->npvars, true); + ins->ispvars.resize(ins->vars, false); + + if (ins->assignedLits.size() > 0) { + vector assignedLits_new; + for (Lit l : ins->assignedLits) + assignedLits_new.push_back(map[toInt(l)]); + ins->assignedLits = assignedLits_new; + } + + RewriteClauses(ins->clauses, map); + RewriteClauses(ins->learnts, map); + + // update the variable map + if (ins->keepVarMap) { + for (int i = 0; i < ins->gmap.size(); i++) { + Lit l = ins->gmap[i]; + if (l == lit_Undef) + continue; + ins->gmap[i] = map[toInt(l)]; + } + } + + subsump = true; + } + + if (ins->assignedLits.size() > 0) { + sharpsat_td::SortAndDedup(ins->assignedLits); + + TestSolver S(ins->vars, ins->clauses, ins->learnts, ins->assignedLits); + Compact(S.getAssigns()); + sharpsat_td::SortAndDedup(ins->clauses); + sharpsat_td::SortAndDedup(ins->learnts); + + subsump = true; + } + + if (subsump) + Subsume(); + + if (config.verb >= 1) + printCNFInfo("EquivEl"); + return true; +} + +template bool Preprocessor::VariableEliminate(bool dve) { + vector vars; + int origclssz = ins->clauses.size(); + int reps = dve ? config.dve_reps : config.ve_reps; + int times = 0; + while (times < reps) { + vars.clear(); + if (dve) + pickDefVars(vars); + else + pickVars(vars); + + if (vars.size() == 0) + break; + + int lastidx = ElimVars(vars); + + vec cassign; + if (ins->assignedLits.size() > 0) { + sharpsat_td::SortAndDedup(ins->assignedLits); + TestSolver S(ins->vars, ins->clauses, ins->learnts, ins->assignedLits); + S.getAssigns().copyTo(cassign); + } else { + cassign.growTo(ins->vars, l_Undef); + } + + // Here we abuse Compact, assuming that deleted vars was assigned. + // We can assume that the deleted vars are non-projected vars or the + // counting mode is not a weighted one. + assert(lastidx <= vars.size()); + vars.resize(lastidx); + for (int i = 0; i < lastidx; i++) { + Var v = vars[i]; + if (cassign[v] == l_Undef) + cassign[v] = l_True; // just want to treat v as not a free variable and + // eliminate... + } + + Compact(cassign, vars); + Subsume(); + + times++; + if (times % 1000 == 0 && config.verb >= 1) + printCNFInfo(dve ? "DefVE" : "VE"); + if (ins->clauses.size() > origclssz) + break; + } + + if (config.verb >= 1) + printCNFInfo(dve ? "DefVE" : "VE"); + + return true; +} + +template +inline bool +Preprocessor::isVECandidate(Graph &G, bool def, vector &freq, + std::vector &cl_size, int i) const { + return (((!def&& !config.ve_only_simpical) || G.isSimplical(i)) && + min(freq[toInt(mkLit(i))], freq[toInt(~mkLit(i))]) <= + config.ve_limit) || + (config.ve_more && (freq[toInt(mkLit(i))] * freq[toInt(~mkLit(i))] <= + freq[toInt(mkLit(i))] + freq[toInt(~mkLit(i))])); +} + +template void Preprocessor::pickVars(vector &vars) { + vars.clear(); + + vector freq; + vector cl_size; + vector is_simpical(ins->vars); + Graph G(ins->vars, ins->clauses, ins->learnts, freq, cl_size); + + for (int i = ins->npvars; i < ins->vars; i++) { // for only projected vars + if (isVECandidate(G, false, freq, cl_size, i)) { + vars.push_back(i); + if (config.ve_prefer_simpical) { + is_simpical[i] = G.isSimplical(i); + } + } + } + sort(vars.begin(), vars.end(), [&](int a, int b) { + int ca = freq[toInt(mkLit(a))] * freq[toInt(~mkLit(a))]; + int cb = freq[toInt(mkLit(b))] * freq[toInt(~mkLit(b))]; + if (config.ve_prefer_simpical) { + if ((ca == 0) ^ (cb == 0)) { + return ca < cb; + } + if (is_simpical[a] ^ is_simpical[b]) { + return is_simpical[a] > is_simpical[b]; + } + } + if (ca == cb) { + return cl_size[a] > cl_size[b]; + } + return ca < cb; + }); +} + +template +void Preprocessor::pickDefVars(vector &vars) { + vars.clear(); +#if 0 + vector map(ins->vars); + vector candv; + + double stime = cpuTime(); + vector freq; + { + Graph G(ins->vars, ins->clauses, ins->learnts, freq); + + int count = 0; + for (int i = 0; i < ins->npvars; i++) { + map[i] = i; + + if (isVECandidate(G, true, freq, i)) { + if (ins->weighted && ins->lit_weights[toInt(mkLit(i))] != + ins->lit_weights[toInt(~mkLit(i))]) + continue; + + map[i] = ((ins->vars << 1) - ins->npvars) + candv.size(); + candv.push_back(i); + } + } + } + + if (candv.size() == 0) + return; + + int newvars = + ((ins->vars + candv.size()) << 1) - + ins->npvars; // ins->vars + candv.size()*2 + ins->vars - ins->npvars; + TestSolver S(newvars); + for (const auto &clause : ins->clauses) { + S.addClauseWith(clause); // add the existing clause + + bool toduplicate = false; + for (Lit l : clause) + if (var(l) >= ins->npvars || map[var(l)] >= ins->vars) { + toduplicate = true; + break; + } + + if (toduplicate) { + vector newc; + for (Lit l : clause) { + Lit nl; + if (var(l) >= ins->npvars) + nl = mkLit((ins->vars - ins->npvars) + var(l), sign(l)); + else if (map[var(l)] >= ins->vars) + nl = mkLit(map[var(l)], sign(l)); + else + nl = l; + assert(var(nl) < newvars); + newc.push_back(nl); + } + S.addClauseWith(newc); + } + } + for (int v : candv) { + S.addClauseWith({~mkLit(map[v] + candv.size()), mkLit(v), ~mkLit(map[v])}); + S.addClauseWith({~mkLit(map[v] + candv.size()), ~mkLit(v), mkLit(map[v])}); + } + + vector def(ins->npvars, false); + vec assumptions; + for (int v : candv) { + assumptions.clear(); + assumptions.push(mkLit(v)); + assumptions.push(~mkLit(map[v])); + for (int w : candv) { + if (w != v && !def[w]) { + assumptions.push(mkLit(map[w] + candv.size())); + } + } + if (S.Solve(assumptions) == l_False) { + def[v] = true; + vars.push_back(v); + } + + if (cpuTime() - stime > config.dve_timelimit) + break; + } +#endif + + ArjunNS::Arjun arjun; + arjun.new_vars(ins->vars); + for (auto cl : ins->clauses) { + std::vector cl_conf; + for (auto l : cl) { + cl_conf.push_back(CMSat::Lit(var(l), sign(l))); + } + arjun.add_clause(cl_conf); + } + std::vector sample; + for (int i = 0; i < ins->npvars; i++) { + sample.push_back(i); + } + arjun.set_sampl_vars(sample); + std::vector indpendent = arjun.run_backwards(); + std::unordered_set set(indpendent.begin(), indpendent.end()); + + vector freq; + vector cl_size; + vector is_simpical(ins->vars); + Graph G(ins->vars, ins->clauses, ins->learnts, freq, cl_size); + + for (int i = 0; i < ins->npvars; i++) { + if (set.find(i) == set.end() && isVECandidate(G,false,freq,cl_size,i)) { + vars.push_back(i); + is_simpical[i] = G.isSimplical(i); + } + } + sort(vars.begin(), vars.end(), [&](int a, int b) { + int ca = freq[toInt(mkLit(a))] * freq[toInt(~mkLit(a))]; + int cb = freq[toInt(mkLit(b))] * freq[toInt(~mkLit(b))]; + if (config.ve_prefer_simpical) { + if ((ca == 0) ^ (cb == 0)) { + return ca < cb; + } + if (is_simpical[a] ^ is_simpical[b]) { + return is_simpical[a] > is_simpical[b]; + } + } + if (ca == cb) { + return cl_size[a] > cl_size[b]; + } + return ca < cb; + }); +} + +template +int Preprocessor::ElimVars(const vector &vars) { + int idx = 0; + int origclssz = ins->clauses.size(); + + vector deleted(ins->vars, false); + for (; idx < vars.size(); idx++) { + Var v = vars[idx]; + if (ins->clauses.size() > origclssz) + break; + + if (config.ve_check) { + int p = 0, n = 0; + for (int i = ins->clauses.size() - 1; i >= 0; i--) { + vector &clause = ins->clauses[i]; + for (int j = 0; j < clause.size(); j++) { + if (var(clause[j]) == v) { + bool negative = sign(clause[j]); + if (negative) { + n++; + } else { + p++; + } + break; + } + } + } + if (!(min(p, n) <= config.ve_limit|| p * n <= n + p)) { + break; + } + } + vector> pos; + vector> neg; + + // find clauses with literals of v + for (int i = ins->clauses.size() - 1; i >= 0; i--) { + vector &clause = ins->clauses[i]; + for (int j = 0; j < clause.size(); j++) { + if (var(clause[j]) == v) { + bool negative = sign(clause[j]); + sharpsat_td::ShiftDel(clause, j); + + if (negative) { + neg.push_back(clause); + } else { + pos.push_back(clause); + } + sharpsat_td::SwapDel(ins->clauses, i); + break; + } + } + } + + // var elimination by resolution + for (const auto &c1 : pos) { + for (const auto &c2 : neg) { + vector newc; + bool taut = false; + int i = 0; + int j = 0; + + while (i < c1.size()) { + while (j < c2.size() && var(c2[j]) < var(c1[i])) { + newc.push_back(c2[j]); + j++; + } + if (j < c2.size() && var(c2[j]) == var(c1[i])) { + if (c2[j] == c1[i]) { + newc.push_back(c2[j]); + i++, j++; + continue; + } else { + taut = true; + break; + } + } else { + newc.push_back(c1[i]); + i++; + } + } + while (j < c2.size()) { + newc.push_back(c2[j]); + j++; + } + if (!taut) { + if (newc.size() == 1) + ins->assignedLits.push_back(newc[0]); + else + ins->clauses.push_back(newc); + } + } + } + + if (neg.size() == 0) { + // MEMO: v is defined by others. Thus, v must be true on all models. + ins->assignedLits.push_back(mkLit(v)); + } else if (pos.size() == 0) { + ins->assignedLits.push_back(~mkLit(v)); + } else { + deleted[v] = true; + } + } + + for (int i = ins->learnts.size() - 1; i >= 0; i--) { + vector &clause = ins->learnts[i]; + for (int j = 0; j < clause.size(); j++) { + if (deleted[var(clause[j])]) { + sharpsat_td::SwapDel(ins->learnts, i); + break; + } + } + } + return idx; +} + +static inline lbool val(const vec &assigns, Lit p) { + return assigns[var(p)] ^ sign(p); +} + +template +void Preprocessor::Compact(const vec &assigns, + const vector &elimvars) { + int varnum = 0; + vector occurred; + occurred.resize(ins->vars, false); + + // Compact Clauses + CompactClauses(assigns, ins->clauses, occurred, varnum); + CompactClauses(assigns, ins->learnts, occurred, varnum); + + // Compact Variables + int new_idx = 0; + vector map; + vector nonpvars; + + map.clear(); + map.resize(ins->vars, var_Undef); + if (ins->keepVarMap) + for (auto v : elimvars) + if (v < ins->npvars) + map[v] = var_Determined; + + nonpvars.reserve(ins->vars - ins->npvars); + + vector lit_weights2; + if (ins->weighted) { + lit_weights2 = ins->lit_weights; + ins->lit_weights.resize(varnum * 2); + } + + for (Var v = 0; v < ins->vars; v++) { + if (occurred[v]) { + if (ins->ispvars[v]) { + map[v] = new_idx; + if (ins->weighted) { + ins->lit_weights[toInt(mkLit(new_idx))] = + lit_weights2[toInt(mkLit(v))]; + ins->lit_weights[toInt(~mkLit(new_idx))] = + lit_weights2[toInt(~mkLit(v))]; + } + new_idx++; + } else + nonpvars.push_back(v); + } else { + if (ins->ispvars[v]) { + if (assigns[v] == l_Undef) { + ins->freevars++; + if (ins->weighted) + ins->gweight *= lit_weights2[toInt(mkLit(v, true))] + + lit_weights2[toInt(mkLit(v, false))]; + } else { + if (ins->weighted) + ins->gweight *= + lit_weights2[toInt(mkLit(v, assigns[v] == l_False))]; + } + } + } + } + + ins->npvars = new_idx; + for (int i = 0; i < nonpvars.size(); i++) { + map[nonpvars[i]] = new_idx; + new_idx++; + } + ins->vars = new_idx; + + ins->ispvars.clear(); + ins->ispvars.resize(ins->npvars, true); + ins->ispvars.resize(ins->vars, false); + + // Replace literals according to map + RewriteClauses(ins->clauses, map); + RewriteClauses(ins->learnts, map); + + // update the variable map + if (ins->keepVarMap) { + std::unordered_map table; + + for (int i = 0; i < ins->gmap.size(); i++) { + Lit l = ins->gmap[i]; + if (l == lit_Undef) + continue; + + Var x = var(ins->gmap[i]); + if (assigns[x] == l_Undef) { + Var newv = map[var(l)]; + if (newv >= 0) { + ins->gmap[i] = mkLit(newv, sign(l)); + } else { + assert(newv == var_Undef); + auto itr = table.find(x); + if (itr == table.end()) { + table[x] = ins->freeLitClasses.size(); + ins->freeLitClasses.push_back({mkLit(i, sign(l))}); + } else { + ins->freeLitClasses[itr->second].push_back(mkLit(i, sign(l))); + } + ins->gmap[i] = lit_Undef; + } + } else if (map[var(l)] == var_Determined) { + ins->definedVars.push_back(i); + ins->gmap[i] = lit_Undef; + } else { + bool lsign = ((assigns[x] == l_False) != sign(l)); + ins->fixedLits.push_back(mkLit(i, lsign)); + ins->gmap[i] = lit_Undef; + } + } + } + + ins->assignedLits.clear(); +} + +template +void Preprocessor::CompactClauses(const vec &assigns, + vector> &cls, + vector &occurred, int &varnum) { + int i1, i2; + int j1, j2; + + for (i1 = 0, i2 = 0; i1 < cls.size(); i1++) { + vector &c = cls[i1]; + for (j1 = 0, j2 = 0; j1 < c.size(); j1++) { + if (val(assigns, c[j1]) == l_Undef) + c[j2++] = c[j1]; + else if (val(assigns, c[j1]) == l_True) { + goto NEXTC; + } + } + c.resize(j2); + assert(c.size() == j2); + assert(c.size() > 1); + + for (auto l : c) { + Var v = var(l); + if (!occurred[v]) { + occurred[v] = true; + varnum++; + } + } + + cls[i2++] = cls[i1]; + NEXTC:; + } + cls.resize(i2); +} + +template +void Preprocessor::RewriteClauses(vector> &cls, + const vector &map) { + // We assume that map is injective for active variables, i.e., this does not + // change the length of clauses. + + for (int i = 0; i < cls.size(); i++) { + vector &c = cls[i]; + for (int j = 0; j < c.size(); j++) + c[j] = mkLit(map[var(c[j])], sign(c[j])); + sort(c.begin(), c.end()); + } +} + +template +void Preprocessor::RewriteClauses(vector> &cls, + const vector &map) { + // map may not be injective, i.e., this may strengthen clauses. + + for (int i = 0; i < cls.size(); i++) { + vector &c = cls[i]; + for (int j = 0; j < c.size(); j++) + c[j] = map[toInt(c[j])]; + + sharpsat_td::SortAndDedup(c); + + bool unit = false; + bool taut = false; + if (c.size() == 1) { + ins->assigns[var(c[0])] = sign(c[0]) ? l_False : l_True; + ins->assignedLits.push_back(c[0]); + unit = true; + } else { + for (int j = 1; j < c.size(); j++) + if (var(c[j]) == var(c[j - 1])) { + taut = true; + break; + } + } + if (unit || taut) { + sharpsat_td::SwapDel(cls, i); + i--; + } + } +} + +template void Preprocessor::Subsume() { + { + sharpsat_td::Subsumer subsumer; + ins->clauses = subsumer.Subsume(ins->clauses); + sharpsat_td::SortAndDedup(ins->clauses); + } + + if (ins->learnts.empty()) + return; + for (const auto &clause : ins->clauses) { + ins->learnts.push_back(clause); + } + + { + sharpsat_td::Subsumer subsumer_lrnt; + ins->learnts = subsumer_lrnt.Subsume(ins->learnts); + sharpsat_td::SortAndDedup(ins->learnts); + } + + for (int i = 0; i < ins->learnts.size(); i++) { + if (std::binary_search(ins->clauses.begin(), ins->clauses.end(), + ins->learnts[i])) { + sharpsat_td::SwapDel(ins->learnts, i); + i--; + } + } +} + +template class PRE::Preprocessor; +template class PRE::Instance; diff --git a/src/preprocs/cnf/util/PreprocGPMC.hpp b/src/preprocs/cnf/util/PreprocGPMC.hpp new file mode 100644 index 00000000..c5ac5ba1 --- /dev/null +++ b/src/preprocs/cnf/util/PreprocGPMC.hpp @@ -0,0 +1,154 @@ +#pragma once +#include "3rdParty/glucose-3.0/core/Solver.h" + +#include "3rdParty/glucose-3.0/utils/System.h" +#include "lib_sharpsat_td/utils.hpp" +#include "TestSolver.hpp" +#include +// largely based on gpmc https://git.trs.css.i.nagoya-u.ac.jp/k-hasimt/GPMC +namespace PRE { + +struct ConfigPreprocessor { + int varlimit; + double timelim; + double reps; + int verb; + + // EE + bool ee; + int ee_varlim; + + // VE/DefVE + bool ve; + bool ve_dve; + int ve_reps; + int dve_reps; + int ve_limit; + bool ve_only_simpical; + bool ve_more; + bool ve_check; + bool ve_prefer_simpical; + double dve_timelimit; + + + // CS + bool cs; + ConfigPreprocessor(){ + varlimit = 200000; + timelim = 120; + reps = 20; + verb = 0; + ee = true; + ee_varlim = 150000; + ve = true; + ve_reps = 400; + dve_reps = 10; + ve_more = true; + ve_dve = false; + ve_check = true; + ve_prefer_simpical=true; + dve_timelimit = 60; + cs = true; + ve_limit = 4; + ve_only_simpical = false; + } +}; + +template +class Instance { +public: + Instance(); + bool addClause (std::vector& lits, bool learnt=false); + + Glucose::lbool value (Glucose::Var x) const; + Glucose::lbool value (Glucose::Lit p) const; + + // CNF formula + int vars; + std::vector> clauses; + std::vector> learnts; + + // Counter Mode + bool weighted; + bool projected; + + // For WMC/WPMC + std::vector lit_weights; + + // For PMC/WPMC + int npvars; + std::vector ispvars; + std::vector pvars; + + // Instance keeps temporal fixed literals. Preprocessor will eliminate fixed variables. + std::vector assigns; + std::vector assignedLits; + + // additional information + int freevars; + T_data gweight; + + // information about correspondence with a given CNF + bool keepVarMap; + std::vector gmap; // variable renaming (original (Var) -> simplified (Lit)) + std::vector fixedLits; // fixed Literals + std::vector definedVars; // variables defined by the other variables + std::vector> freeLitClasses; // equivalence classes of free literals + + // extra var score + std::vector score; + + // State + bool unsat; + +}; +template +class Preprocessor { + friend class Solver; +public: + Preprocessor() : ins(NULL) { }; + + void setConfig(ConfigPreprocessor& conf) { this->config = conf; } + + bool Simplify(Instance* ins); + +private: + bool SAT_FLE(); + bool Strengthen(); + bool MergeAdjEquivs(); + bool VariableEliminate(bool dve); + void pickVars(std::vector& vars); + + void pickDefVars(std::vector& vars); + + int ElimVars(const std::vector& del); + + void Compact(const Glucose::vec& assigns, const std::vector& elimvars={}); + void CompactClauses(const Glucose::vec& assigns, std::vector>& cls, + std::vector& occurred, int& varnum); + void RewriteClauses(std::vector>& cls, const std::vector& map); + void RewriteClauses(std::vector>& cls, const std::vector& map); + void Subsume(); + + bool isVECandidate(Graph& G,bool simple, std::vector& freq,std::vector& cl_size, int i) const; + + void printCNFInfo(const char* ppname = "", bool initial = false); + + + Instance *ins; + ConfigPreprocessor config; +}; +template +inline void Preprocessor::printCNFInfo(const char* ppname, bool initial) +{ + if(initial) + printf("c o [%-7s] %d vars (%d pvars), %d cls\n", ppname, ins->vars, ins->npvars, ins->clauses.size()); + else + printf("c o [%-7s] %d vars (%d pvars), %d cls, %d lrnts, %d fvars, elap. %.2lf s\n", ppname, ins->vars, ins->npvars, ins->clauses.size(), ins->learnts.size(), ins->freevars, Glucose::cpuTime()); + + if(ins->weighted) + std::cout << "c o gweight " << ins->gweight << std::endl; + + fflush(stdout); +} +} diff --git a/src/preprocs/cnf/util/TestSolver.cpp b/src/preprocs/cnf/util/TestSolver.cpp new file mode 100644 index 00000000..82d3d2c0 --- /dev/null +++ b/src/preprocs/cnf/util/TestSolver.cpp @@ -0,0 +1,405 @@ + +#include "TestSolver.hpp" +#include + +namespace PRE{ +using namespace std; +using namespace Glucose; + + +void Identifier::identify(Lit l1, Lit l2) { + if (cidx[toInt(l1)] == -1 && cidx[toInt(l2)] == -1) { + cidx[toInt(l1)] = cidx[toInt(l2)] = eqc.size(); + eqc.push_back({l1, l2}); + cidx[toInt(~l1)] = cidx[toInt(~l2)] = eqc.size(); + eqc.push_back({~l1, ~l2}); + num_elem += 2; + } else if (cidx[toInt(l1)] == -1) { + eqc[cidx[toInt(l2)]].push_back(l1); + eqc[cidx[toInt(~l2)]].push_back(~l1); + cidx[toInt(l1)] = cidx[toInt(l2)]; + cidx[toInt(~l1)] = cidx[toInt(~l2)]; + + if (var(eqc[cidx[toInt(l2)]][0]) > var(l1)) { + vector &eq = eqc[cidx[toInt(l2)]]; + std::swap(eq[0], eq.back()); + eq = eqc[cidx[toInt(~l2)]]; + std::swap(eq[0], eq.back()); + } + } else if (cidx[toInt(l2)] == -1) { + eqc[cidx[toInt(l1)]].push_back(l2); + eqc[cidx[toInt(~l1)]].push_back(~l2); + cidx[toInt(l2)] = cidx[toInt(l1)]; + cidx[toInt(~l2)] = cidx[toInt(~l1)]; + } else { + if (cidx[toInt(l1)] == cidx[toInt(l2)]) + return; + assert(cidx[toInt(l1)] != cidx[toInt(l2)]); + + Var d1 = var(eqc[cidx[toInt(l1)]][0]); + Var d2 = var(eqc[cidx[toInt(l2)]][0]); + + if (d1 < d2) { + MergeEquivClasses(cidx[toInt(l1)], cidx[toInt(l2)]); + MergeEquivClasses(cidx[toInt(~l1)], cidx[toInt(~l2)]); + } else { + MergeEquivClasses(cidx[toInt(l2)], cidx[toInt(l1)]); + MergeEquivClasses(cidx[toInt(~l2)], cidx[toInt(~l1)]); + } + } +} +void Identifier::removeEquivClass(Lit l) { + if (cidx[toInt(l)] >= 0) { + for (Lit s : {l, ~l}) { + int idx = cidx[toInt(s)]; + for (Lit le : eqc[idx]) + cidx[toInt(le)] = -1; + eqc[idx].clear(); + } + num_elem -= 2; + } +} +void Identifier::MergeEquivClasses(int c1, int c2) { + for (Lit l : eqc[c2]) { + eqc[c1].push_back(l); + cidx[toInt(l)] = c1; + } + eqc[c2].clear(); + num_elem--; +} +TestSolver::TestSolver(int nvars, + vector> clauses_, + vector> learnts_, + vector assignedLits) +{ + + newVars(nvars); + for(auto l : assignedLits) { + uncheckedEnqueue(l); + } + for(auto c : clauses_) + addClauseWith(c); + for(auto c : learnts_) + addClauseWith(c, true); + + if(!assignedLits.empty()) { + CRef confl = propagate(); + ok = (propagate() == CRef_Undef); + } +} + +void TestSolver::newVars(int nvars) +{ + watches .init(mkLit(nvars-1, true )); + watchesBin .init(mkLit(nvars-1, true )); + assigns .growTo(nvars, l_Undef); + vardata .growTo(nvars, mkVarData(CRef_Undef, 0)); + activity .growTo(nvars, 0); + scoreActivity.growTo(nvars,0.0); + seen .growTo(nvars, 0); + permDiff .growTo(nvars, 0); + polarity .growTo(nvars, true); + decision .growTo(nvars); + trail .capacity(nvars); + for(int i=0; i& ps, bool learnt) +{ + CRef cr = ca.alloc(ps, learnt); + if(!learnt) + clauses.push(cr); + else + learnts.push(cr); + attachClause(cr); +} + +inline void TestSolver::backTo(int pos) +{ + for(int c = trail.size()-1; c >= pos; c--){ + Var x = var(trail[c]); + assigns[x] = l_Undef; + } + qhead = pos; + trail.shrink(trail.size() - pos); +} + +bool TestSolver::falsifiedBy(Lit assump) +{ + int sz = trail.size(); + uncheckedEnqueue(assump); + CRef confl = propagate(); + backTo(sz); + + return confl != CRef_Undef; +} + +bool TestSolver::falsifiedBy(Lit l1, Lit l2) +{ + vec ps; + + ps.push(l1); + ps.push(l2); + return falsifiedBy(ps); +} + +bool TestSolver::falsifiedBy(vec& assump) +{ + int backtrack_level; + vec learnt_clause, selectors; + unsigned int nblevels,szWoutSelectors; + lbool result = l_Undef; + + for (;;){ + CRef confl = propagate(); + if (confl != CRef_Undef){ + // CONFLICT + if (decisionLevel() == 0) { + result = l_False; + break; + } + + learnt_clause.clear(); + selectors.clear(); + analyze(confl, learnt_clause, selectors, backtrack_level, nblevels, szWoutSelectors); + + cancelUntil(backtrack_level); + + if (learnt_clause.size() == 1) { + assert(value(learnt_clause[0])==l_Undef); + uncheckedEnqueue(learnt_clause[0]); + }else{ + CRef cr = ca.alloc(learnt_clause, true); + ca[cr].setLBD(nblevels); + ca[cr].setSizeWithoutSelectors(szWoutSelectors); + learnts.push(cr); + attachClause(cr); + + claBumpActivity(ca[cr]); + uncheckedEnqueue(learnt_clause[0], cr); + } + claDecayActivity(); + + }else{ + Lit next = lit_Undef; + + assert(decisionLevel() <= assump.size()); + + while (decisionLevel() < assump.size()) { + Lit p = assump[decisionLevel()]; + if (value(p) == l_True){ + newDecisionLevel(); + }else if (value(p) == l_False){ + learnt_clause.clear(); + analyzeFinal(~p, learnt_clause); + + if (learnt_clause.size() == 1){ + cancelUntil(0); + enqueue(learnt_clause[0]); + propagate(); + }else{ + CRef cr = ca.alloc(learnt_clause, true); + ca[cr].setLBD(nblevels); + ca[cr].setSizeWithoutSelectors(szWoutSelectors); + learnts.push(cr); + attachClause(cr); + claBumpActivity(ca[cr]); + } + claDecayActivity(); + result = l_False; + goto End; + }else{ + next = p; + break; + } + } + + if (decisionLevel() == assump.size()) break; + + newDecisionLevel(); + uncheckedEnqueue(next); + } + } + +End: + cancelUntil(0); + return result == l_False; +} + + +bool TestSolver::FailedLiterals() +{ + assert(decisionLevel()==0); + int minv = min(nVars(), 1000000); + + int last_size; + do { + last_size = trail.size(); + + for (Var v = 0; v < minv; v++) + if (value(v) == l_Undef) { + if(falsifiedBy(mkLit(v,true))) { + uncheckedEnqueue(mkLit(v, false)); + if(propagate() != CRef_Undef) return false; + } else if(falsifiedBy(mkLit(v,false))) { + uncheckedEnqueue(mkLit(v, true)); + if(propagate() != CRef_Undef) return false; + } + } + + } while (trail.size() > last_size); + + return true; +} + +void TestSolver::exportLearnts(vector>& ilearnts) +{ + ilearnts.clear(); + + if(learnts.size() == 0) return; + + if (learnts.size() >= clauses.size()) + reduceDB(); + + for(int i=0; i>& cls) +{ + for(int i=0; i 0); + vec tmp; + for(auto l : c) + tmp.push(l); + addClause_(tmp); + } +} +// Graph +Graph::Graph(int vars, const vector>& clauses) +{ + clear(); + init(vars); + for(const auto& clause : clauses) + for(int i=0; i>& clauses, const vector>& learnts, vector& freq) +{ + clear(); + init(vars); + freq.resize(vars*2, 0); + + for(const auto& cls : {clauses, learnts}) { + for(const auto& clause : cls) { + for(int i=0; i>& clauses, const vector>& learnts, vector& freq,std::vector& cl_size) +{ + clear(); + init(vars); + freq.resize(vars*2, 0); + cl_size.resize(vars,0); + + for(const auto& cls : {clauses, learnts}) { + for(const auto& clause : cls) { + for(int i=0; i0){ + cl_size[i] /=sum; + } + + } + +} +void Graph::init(int n) +{ + nodes = n; + + adj_list.clear(); + adj_list.resize(nodes, {}); + + adj_mat.clear(); + adj_mat.resize(n); + for(int i=0; i& adj) +{ + for(int i=0; i=j) continue; + out << (i+1) << " " << (j+1) << endl; + } + } +} + +} diff --git a/src/preprocs/cnf/util/TestSolver.hpp b/src/preprocs/cnf/util/TestSolver.hpp new file mode 100644 index 00000000..79e8ada4 --- /dev/null +++ b/src/preprocs/cnf/util/TestSolver.hpp @@ -0,0 +1,114 @@ +#pragma once +#include "3rdParty/glucose-3.0/core/Solver.h" +#include "3rdParty/glucose-3.0/core/SolverTypes.h" +#include "3rdParty/glucose-3.0/mtl/Vec.h" +#include "lib_sharpsat_td/bitset.hpp" + +#include +// This code was stolen straight from gpmc +namespace PRE { +class Graph { +public: + Graph() : nodes(0), edges(0) {} + Graph(int vars, const std::vector> &clauses); + Graph(int vars, const std::vector> &clauses, + const std::vector> &learnts, + std::vector &freq); + + Graph(int vars, const std::vector> &clauses, + const std::vector> &learnts, + std::vector &freq, std::vector &cl_size); + + void init(int n); + void clear(); + + int numNodes() { return this->nodes; } + int numEdges() { return this->edges; } + + void addEdge(int v1, int v2); + bool hasEdge(int v1, int v2) { return adj_mat[v1].Get(v2); } + const std::vector Neighbors(int v) const { return adj_list[v]; } + + bool isSimplical(int v, int proj) { + bool clean = true; + for (auto v : adj_list[v]) { + clean &= v >= proj; + } + if (clean) { + return true; + } + + return isClique(adj_list[v]); + } + + bool isSimplical(int v) { return isClique(adj_list[v]); } + bool isClique(const std::vector &adj); + + // Debug + void toDimacs(std::ostream &out, bool withHeader = true); + +protected: + int nodes; + int edges; + std::vector> adj_list; + std::vector adj_mat; +}; +class Identifier { +public: + Identifier(int vars) { + cidx.resize(2 * vars, -1); + num_elem = 0; + } + + void identify(Glucose::Lit l1, Glucose::Lit l2); + + bool hasEquiv() { return num_elem > 0; } + std::vector> &getEquivClasses() { return eqc; } + Glucose::Lit delegateLit(Glucose::Lit l) { + return (cidx[toInt(l)] == -1) ? l : eqc[cidx[toInt(l)]][0]; + } + int getIndex(Glucose::Lit l) { return cidx[toInt(l)]; } + void removeEquivClass(Glucose::Lit l); + +private: + void MergeEquivClasses(int c1, int c2); + + std::vector> eqc; + std::vector cidx; + int num_elem; +}; +class TestSolver : public Glucose::Solver { +public: + TestSolver(int nvars) { newVars(nvars); } + TestSolver(int nvars, std::vector> clauses, + std::vector> learnts, + std::vector assignedLits); + + void addClauseWith(const std::vector &ps, bool learnt = false); + void resetClauses(std::vector> &clauses); + + Glucose::lbool Solve() { return solve_(); } + Glucose::lbool Solve(const Glucose::vec &assumptions) { + budgetOff(); + setConfBudget(clauses.size() * 10); + return solveLimited(assumptions); + } + + bool falsifiedBy(Glucose::Lit l); + bool falsifiedBy(Glucose::Lit l1, Glucose::Lit l2); + bool falsifiedBy(Glucose::vec &assump); + bool FailedLiterals(); + + void exportLearnts(std::vector> &learnts); + + void assign(Glucose::Lit l) { enqueue(l); } + bool bcp() { return propagate() == Glucose::CRef_Undef; } + + Glucose::vec &getAssigns() { return assigns; } + Glucose::vec &getTrail() { return trail; } + +private: + void newVars(int nvars); + void backTo(int pos); +}; +} // namespace PPMC diff --git a/src/preprocs/cnf/util/lib_sharpsat_td/LICENSE b/src/preprocs/cnf/util/lib_sharpsat_td/LICENSE new file mode 100644 index 00000000..8701d473 --- /dev/null +++ b/src/preprocs/cnf/util/lib_sharpsat_td/LICENSE @@ -0,0 +1,27 @@ +SharpSAT-TD is a modification of SharpSAT (MIT License, 2019 Marc Thurley). + +See licenses of other components in: + +flowcutter/LICENSE +src/clhash/LICENSE + + +SharpSAT-TD -- Copyright (c) 2021 Tuukka Korhonen + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. +IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR +OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE +OR OTHER DEALINGS IN THE SOFTWARE. \ No newline at end of file diff --git a/src/preprocs/cnf/util/lib_sharpsat_td/README.txt b/src/preprocs/cnf/util/lib_sharpsat_td/README.txt new file mode 100644 index 00000000..a857ffd0 --- /dev/null +++ b/src/preprocs/cnf/util/lib_sharpsat_td/README.txt @@ -0,0 +1,9 @@ +The four files in this directory are copies of source code files of the preprocessor of SharpSAT-TD. +- bitset.cpp +- subsumer.cpp +- subsumer.hpp +- utils.hpp + +https://github.com/Laakeri/sharpsat-td + +2022 Kenji Hashimoto \ No newline at end of file diff --git a/src/preprocs/cnf/util/lib_sharpsat_td/bitset.hpp b/src/preprocs/cnf/util/lib_sharpsat_td/bitset.hpp new file mode 100644 index 00000000..3f306922 --- /dev/null +++ b/src/preprocs/cnf/util/lib_sharpsat_td/bitset.hpp @@ -0,0 +1,304 @@ +#pragma once + +#include +#include +#include +#include +#include +#include +#include +#include + +#define BITS 64 + +namespace sharpsat_td { +class Bitset { + public: + uint64_t* data_; + size_t chunks_; + Bitset() { + chunks_ = 0; + data_ = nullptr; + } + explicit Bitset(size_t size) { + chunks_ = (size + BITS - 1) / BITS; + data_ = (uint64_t*)std::malloc(chunks_*sizeof(uint64_t)); + for (size_t i=0;iother.data_[i]) return false; + } + return false; + } + bool operator==(const Bitset& other) const { + for (size_t i=0;i& v) { + for (size_t x : v) { + SetTrue(x); + } + } + void SetTrue(const std::vector& v) { + for (int x : v) { + SetTrue(x); + } + } + void SetFalse(const std::vector& v) { + for (int x : v) { + SetFalse(x); + } + } + void FillTrue() { + for (size_t i=0;i Elements() const { + std::vector ret; + for (size_t i=0;ichunks_) { + pos_++; + if (pos_ < bitset_->chunks_) { + tb_ = bitset_->data_[pos_]; + } + } + return *this; + } + int operator*() const { + return pos_*BITS + __builtin_ctzll(tb_); + } + }; + + BitsetIterator begin() const { + size_t pos = 0; + while (pos < chunks_ && data_[pos] == 0) { + pos++; + } + if (pos < chunks_) { + return BitsetIterator(this, pos, data_[pos]); + } else { + return BitsetIterator(this, pos, 0); + } + } + BitsetIterator end() const { + return BitsetIterator(this, chunks_, 0); + } +}; +} // namespace sharpsat_td \ No newline at end of file diff --git a/src/preprocs/cnf/util/lib_sharpsat_td/subsumer.cpp b/src/preprocs/cnf/util/lib_sharpsat_td/subsumer.cpp new file mode 100644 index 00000000..a1c19779 --- /dev/null +++ b/src/preprocs/cnf/util/lib_sharpsat_td/subsumer.cpp @@ -0,0 +1,197 @@ +#include "subsumer.hpp" + +#include +#include +#include + +//#include "utils.hpp" + +#define getD(e,i) data[(e.B) + (i)] + +namespace sharpsat_td { + +void Subsumer::assumeSize(size_t size) { + if (data.size() < size) { + data.resize(size); + } +} + +bool Subsumer::isPrefix(const vecP a, const vecP b) { + for (size_t i = 0; i < a.size(); i++) { + if (getD(a, i) != getD(b, i)) return false; + } + return true; +} + +bool Subsumer::CSO1(const vector& D, size_t b, size_t e, const vecP S, + size_t j, size_t d, const vector& d0Index) { + while (j < S.size() && getD(S, j) < getD(D[b], d)) j++; + if (j >= S.size()) return false; + + if (getD(S, j) == getD(D[b], d)) { + size_t ee = b; + if (d == 0) { + ee = d0Index[getD(S, j) + 1] - 1; + } + else if (e - b < BSconst) { + while (ee + 1 <= e && getD(D[ee + 1], d) == getD(S, j)) ee++; + } + else { + int mi = b; + int ma = e - 1; + while (mi <= ma) { + int mid = (mi+ma)/2; + if (getD(D[mid + 1], d) == getD(S, j)) { + ee = mid + 1; + mi = mid + 1; + } + else { + ma = mid - 1; + } + } + } + if (S.size() > d + 1 && D[b].size() == d + 1) { + return true; + } + if (j + 1 <= S.size()) { + if (CSO1(D, b, ee, S, j + 1, d + 1, d0Index)) { + return true; + } + } + b = ee + 1; + } + else { + if (d == 0) { + b = d0Index[getD(S, j)]; + } + else if (e - b < BSconst) { + while (b <= e && getD(D[b], d) < getD(S, j)) b++; + } + else { + int mi = b; + int ma = e; + while (mi <= ma) { + int mid = (mi+ma)/2; + if (getD(D[mid], d) < getD(S, j)) { + b = mid + 1; + mi = mid + 1; + } + else { + ma = mid - 1; + } + } + } + } + if (b <= e) return CSO1(D, b, e, S, j, d, d0Index); + return false; +} + +vector> Subsumer::Subsume(const vector>& clauses) { + vector D(clauses.size()); + vector d0Index; + ALIt++; + int pid = 0; + int maxFreq = 0; + size_t dataP = 0; + for (size_t i = 0; i < clauses.size(); i++) { + if (clauses[i].empty()) { + return {{}}; + } + for (size_t j = 0; j < clauses[i].size(); j++) { + data.push_back(toInt(clauses[i][j])); + } + D[i].B = dataP; + D[i].E = dataP + clauses[i].size(); + D[i].O = i; + dataP += D[i].size(); + + for (size_t j = D[i].B; j < D[i].E; j++) { + if ((int)ALU.size() <= data[j]) { + ALU.resize(data[j] + 1); + ALI.resize(data[j] + 1); + } + if (ALU[data[j]] != ALIt) { + ALU[data[j]] = ALIt; + if (pid >= (int)ALF.size()) ALF.resize(pid + 1); + ALF[pid] = 0; + ALI[data[j]] = pid++; + } + data[j] = ALI[data[j]]; + ALF[data[j]]++; + maxFreq = max(maxFreq, ALF[data[j]]); + } + } + vector > cSort(maxFreq + 1); + for (int i = 0; i < pid; i++) { + cSort[ALF[i]].push_back(i); + } + vector perm(pid); + size_t i2 = 0; + for (int i = 0; i <= maxFreq; i++) { + for (int t : cSort[i]) { + perm[t] = i2++; + } + } + for (size_t i = 0; i < D.size(); i++) { + for (size_t j = D[i].B; j < D[i].E; j++) { + data[j] = perm[data[j]]; + } + std::sort(data.data() + D[i].B, data.data() + D[i].E); + } + auto cmp = [&](vecP a, vecP b) { + if (getD(a, 0) < getD(b, 0)) return true; + else if (getD(a, 0) > getD(b, 0)) return false; + size_t sz = min(a.size(), b.size()); + for (size_t i = 1; i < sz; i++) { + if (getD(a, i) < getD(b, i)) return true; + else if (getD(a, i) > getD(b, i)) return false; + } + return a.size() < b.size(); + }; + vector > cSort2(pid); + for (size_t i = 0; i < D.size(); i++) { + cSort2[getD(D[i], 0)].push_back(D[i]); + } + size_t di = 0; + for (int i = 0; i < pid; i++) { + sort(cSort2[i].begin(), cSort2[i].end(), cmp); + for (size_t j = 0; j < cSort2[i].size(); j++) { + D[di++] = cSort2[i][j]; + } + } + d0Index.resize(pid + 1); + int idx = 0; + for (size_t i = 0; i < D.size(); i++) { + if (i == 0 || getD(D[i], 0) > getD(D[i - 1], 0)) { + while (idx <= getD(D[i], 0)) { + d0Index[idx++] = i; + } + } + } + while (idx <= pid) { + d0Index[idx++] = (int)D.size(); + } + vector subsumed(D.size()); + size_t S = 0; + for (size_t i = 1; i < D.size(); i++) { + if (D[S].size() <= D[i].size() && isPrefix(D[S], D[i])) { + subsumed[i] = true; + } + else { + S = i; + } + } + for (size_t i = 0; i + 1 < D.size(); i++) { + if (!subsumed[i] && CSO1(D, i + 1, D.size() - 1, D[i], 0, 0, d0Index)) { + subsumed[i] = true; + } + } + vector> ret; + for (size_t i = 0; i < D.size(); i++) { + if (!subsumed[i]) { + ret.push_back(clauses[D[i].O]); + } + } + return ret; +} +} // namespace sharpsat_td diff --git a/src/preprocs/cnf/util/lib_sharpsat_td/subsumer.hpp b/src/preprocs/cnf/util/lib_sharpsat_td/subsumer.hpp new file mode 100644 index 00000000..9ed43bff --- /dev/null +++ b/src/preprocs/cnf/util/lib_sharpsat_td/subsumer.hpp @@ -0,0 +1,35 @@ +#pragma once + +#include +#include + +#include "../lib_sharpsat_td/utils.hpp" +#include "3rdParty/glucose-3.0/core/SolverTypes.h" + +namespace sharpsat_td { +class Subsumer{ +private: + vector ALU; + vector ALI; + int ALIt = 1; + vector ALF; + const size_t BSconst = 18; // magic constant + + struct vecP { + size_t B, E, O; + size_t size() const { + return E - B; + } + }; + + vector data; + + bool isPrefix(vecP a, vecP b); + void assumeSize(size_t size); + bool CSO1(const vector& D, size_t b, size_t e, const vecP S, + size_t j, size_t d, const vector& d0Index); + +public: + vector> Subsume(const vector>& clauses); +}; +} // namespace sharpsat_td diff --git a/src/preprocs/cnf/util/lib_sharpsat_td/utils.hpp b/src/preprocs/cnf/util/lib_sharpsat_td/utils.hpp new file mode 100644 index 00000000..a08aaeda --- /dev/null +++ b/src/preprocs/cnf/util/lib_sharpsat_td/utils.hpp @@ -0,0 +1,278 @@ +#pragma once + +#include +#include +#include +#include +#include +#include +#include +#include + +#include "../lib_sharpsat_td/bitset.hpp" + +namespace sharpsat_td { +#define F first +#define S second +typedef int Lit; +typedef int Var; + +using std::vector; +using std::string; +using std::cout; +using std::cerr; +using std::endl; +using std::max; +using std::min; +using std::pair; +using std::to_string; +using std::swap; + +inline bool Subsumes(const vector& a, const vector& b) { + if (a.size() == b.size()) return a == b; + int j = 0; + for (int i = 0; i < (int)a.size(); i++) { + while (j < (int)b.size() && b[j] < a[i]) { + j++; + } + if (j == (int)b.size()) return false; + assert(b[j] >= a[i]); + if (b[j] > a[i]) return false; + } + return true; +} + +inline Lit Neg(Lit x) { + return x^1; +} + +inline Var VarOf(Lit x) { + return x/2; +} + +inline Lit PosLit(Var x) { + return x*2; +} + +inline Lit NegLit(Var x) { + return x*2+1; +} + +inline Lit MkLit(Var var, bool phase) { + if (phase) { + return PosLit(var); + } else { + return NegLit(var); + } +} + +inline bool IsPos(Lit x) { + return !(x&1); +} + +inline bool IsNeg(Lit x) { + return x&1; +} + +inline Lit FromDimacs(int64_t x) { + assert(x != 0); + assert(std::llabs(x) < (1ll << 30ll)); + if (x > 0) { + return PosLit(x); + } else { + return NegLit(-x); + } +} + +inline int64_t ToDimacs(Lit x) { + assert(x >= 2); + if (x&1) { + return -(int64_t)VarOf(x); + } else { + return VarOf(x); + } +} + +inline bool IsInt(const string& s, int64_t lb=std::numeric_limits::min(), int64_t ub=std::numeric_limits::max()) { + try { + int x = std::stoll(s); + return lb <= x && x <= ub; + } catch (...) { + return false; + } +} + +inline bool IsDouble(const string& s, double lb=std::numeric_limits::min(), double ub=std::numeric_limits::max()) { + try { + double x = std::stod(s); + return lb <= x && x <= ub; + } catch (...) { + return false; + } +} + +inline vector Negate(vector vec) { + for (Lit& lit : vec) { + lit = Neg(lit); + } + return vec; +} + +inline vector VarsOf(vector vec) { + for (Lit& lit : vec) { + lit = VarOf(lit); + } + return vec; +} + + +template +void Shuffle(vector& vec, std::mt19937& gen) { + std::shuffle(vec.begin(), vec.end(), gen); +} + +inline bool RandBool(std::mt19937& gen) { + return std::uniform_int_distribution(0,1)(gen); +} + +template +inline T RandInt(T a, T b, std::mt19937& gen) { + return std::uniform_int_distribution(a,b)(gen); +} + +template +T Power2(int p) { + assert(p >= 0); + if (p == 0) return 1; + if (p%2 == 0) { + T x = Power2(p/2); + return x*x; + } else { + return Power2(p-1)*2; + } +} + +inline bool IsClause(const vector& clause) { + for (size_t i = 1; i < clause.size(); i++) { + if (VarOf(clause[i]) <= VarOf(clause[i-1])) return false; + } + return true; +} + +template +bool IsSorted(const vector& vec) { + for (size_t i = 1; i < vec.size(); i++) { + if (vec[i] < vec[i-1]) return false; + } + return true; +} + +template +void Append(std::vector& a, const std::vector& b) { + a.reserve(a.size() + b.size()); + for (const T& x : b) { + a.push_back(x); + } +} + +template +std::vector PermInverse(const std::vector& perm) { + std::vector ret(perm.size()); + for (int i = 0; i < (int)perm.size(); i++) { + ret[perm[i]] = i; + } + return ret; +} + +inline Bitset ToBitset(const std::vector& a, int n) { + assert(n>=0); + Bitset bs(n); + for (int x : a) { + assert(x>=0&&x +void SortAndDedup(vector& vec) { + std::sort(vec.begin(), vec.end()); + vec.erase(std::unique(vec.begin(), vec.end()), vec.end()); +} + +template +void SwapDel(vector& vec, size_t i) { + assert(i < vec.size()); + std::swap(vec[i], vec.back()); + vec.pop_back(); +} + +template +void ShiftDel(vector& vec, size_t i) { + assert(i < vec.size()); + for (; i+1 < vec.size(); i++) { + vec[i] = std::move(vec[i+1]); + } + vec.pop_back(); +} + +template +int Ind(const std::vector& a, const T& x) { + int ind = std::lower_bound(a.begin(), a.end(), x) - a.begin(); + assert(a[ind] == x); + return ind; +} + +template +bool BS(const std::vector& a, const T x) { + return std::binary_search(a.begin(), a.end(), x); +} + +class Timer { + private: + bool timing; + std::chrono::duration elapsedTime; + std::chrono::time_point startTime; + public: + Timer(); + void start(); + void stop(); + void clear(); + double get() const; +}; + +inline Timer::Timer() { + timing = false; + elapsedTime = std::chrono::duration(std::chrono::duration_values::zero()); +} + +inline void Timer::start() { + if (timing) return; + timing = true; + startTime = std::chrono::steady_clock::now(); +} + +inline void Timer::stop() { + if (!timing) return; + timing = false; + std::chrono::time_point endTime = std::chrono::steady_clock::now(); + elapsedTime += (endTime - startTime); +} + +inline double Timer::get() const { + if (timing) { + auto tela = elapsedTime; + tela += (std::chrono::steady_clock::now() - startTime); + return tela.count(); + } + else { + return elapsedTime.count(); + } +} + +inline void Timer::clear() { + elapsedTime = std::chrono::duration(std::chrono::duration_values::zero()); +} +#undef S +#undef F +} // namespace sharpsat_td diff --git a/src/problem/ProblemManager.hpp b/src/problem/ProblemManager.hpp index 3abac5cb..cdc071fd 100644 --- a/src/problem/ProblemManager.hpp +++ b/src/problem/ProblemManager.hpp @@ -27,11 +27,13 @@ namespace d4 { class ProblemManager { protected: unsigned m_nbVar; + unsigned m_nbFreeVars; std::vector m_weightLit; std::vector m_weightVar; std::vector m_selected; std::vector m_maxVar; std::vector m_indVar; + std::vector m_gmap; bool m_isUnsat = false; public: @@ -42,6 +44,17 @@ class ProblemManager { unsigned getNbVar() { return m_nbVar; } void setNbVar(int n) { m_nbVar = n; } + unsigned& freeVars(){ + return m_nbFreeVars; + } + + std::vector& gmap() { + return m_gmap; + } + + virtual void normalize() = 0; + virtual void normalizeInner() = 0; + virtual void display(std::ostream &out) = 0; virtual void displayStat(std::ostream &out, std::string startLine) = 0; virtual ProblemManager *getUnsatProblem() = 0; diff --git a/src/problem/cnf/ParserDimacs.cpp b/src/problem/cnf/ParserDimacs.cpp index 9fb0b3d8..7cef7b2f 100644 --- a/src/problem/cnf/ParserDimacs.cpp +++ b/src/problem/cnf/ParserDimacs.cpp @@ -37,9 +37,10 @@ void ParserDimacs::readListIntTerminatedByZero(BufferRead &in, int v = -1; do { v = in.nextInt(); - if (v) list.push_back(v); + if (v) + list.push_back(v); } while (v); -} // readListIntTerminatedByZero +} // readListIntTerminatedByZero /** * @brief Parse a literal index and a weight and store the result in the given @@ -57,7 +58,7 @@ void ParserDimacs::parseWeightedLit(BufferRead &in, weightLit[lit << 1] = w; else weightLit[((-lit) << 1) + 1] = w; -} // parseWeightedLit +} // parseWeightedLit /** * @brief Parse the dimacs format in order to extract CNF formula and @@ -82,7 +83,8 @@ int ParserDimacs::parse_DIMACS_main(BufferRead &in, for (;;) { in.skipSpace(); - if (in.eof()) break; + if (in.eof()) + break; if (in.currentChar() == 'p') { in.consumeChar(); @@ -93,7 +95,8 @@ int ParserDimacs::parse_DIMACS_main(BufferRead &in, vpActivated = true; in.consumeChar(); } - if (in.currentChar() == 'w') in.consumeChar(); + if (in.currentChar() == 'w') + in.consumeChar(); if (in.nextChar() != 'c' || in.nextChar() != 'n' || in.nextChar() != 'f') std::cerr << "PARSE ERROR! Unexpected char: " << in.currentChar() @@ -107,7 +110,8 @@ int ParserDimacs::parse_DIMACS_main(BufferRead &in, std::cout << "c Some variable are marked: " << in.nextInt() << "\n"; weightLit.resize(((nbVars + 1) << 1), 1); - if (nbClauses < 0) printf("parse error\n"), exit(2); + if (nbClauses < 0) + printf("parse error\n"), exit(2); } else if (in.currentChar() == 'v') { in.consumeChar(); assert(in.currentChar() == 'p'); @@ -125,7 +129,7 @@ int ParserDimacs::parse_DIMACS_main(BufferRead &in, if (in.canConsume("max")) { readListIntTerminatedByZero(in, problemManager->getMaxVar()); } else if (in.canConsume("ind")) - readListIntTerminatedByZero(in, problemManager->getIndVar()); + readListIntTerminatedByZero(in, problemManager->getSelectedVar()); else in.skipLine(); } else { @@ -138,7 +142,9 @@ int ParserDimacs::parse_DIMACS_main(BufferRead &in, assert(!endLine); } else if (in.canConsume("show")) readListIntTerminatedByZero(in, problemManager->getSelectedVar()); - else + else if (in.canConsume("ind")) { + readListIntTerminatedByZero(in, problemManager->getSelectedVar()); + } else in.skipLine(); } } else { @@ -163,7 +169,8 @@ int ParserDimacs::parse_DIMACS_main(BufferRead &in, unsigned j = 1; bool isSat = false; for (unsigned i = 1; !isSat && i < lits.size(); i++) { - if (lits[i] == lits[j - 1]) continue; + if (lits[i] == lits[j - 1]) + continue; isSat = lits[i] == ~lits[j - 1]; lits[j++] = lits[i]; } @@ -183,5 +190,5 @@ int ParserDimacs::parse_DIMACS(std::string input_stream, ProblemManagerCnf *problemManager) { BufferRead in(input_stream); return parse_DIMACS_main(in, problemManager); -} // parse_DIMACS -} // namespace d4 +} // parse_DIMACS +} // namespace d4 diff --git a/src/problem/cnf/ProblemManagerCnf.cpp b/src/problem/cnf/ProblemManagerCnf.cpp index 2fd0e082..2854330f 100644 --- a/src/problem/cnf/ProblemManagerCnf.cpp +++ b/src/problem/cnf/ProblemManagerCnf.cpp @@ -20,6 +20,7 @@ #include "ParserDimacs.hpp" #include "src/problem/ProblemManager.hpp" +#include namespace d4 { /** @@ -34,13 +35,15 @@ ProblemManagerCnf::ProblemManagerCnf(std::string &nameFile) { m_weightVar.resize(m_nbVar + 1, 0); for (unsigned i = 0; i <= m_nbVar; i++) m_weightVar[i] = m_weightLit[i << 1] + m_weightLit[(i << 1) + 1]; -} // constructor + + normalize(); +} // constructor /** Constructor. Construct an empty formula. */ -ProblemManagerCnf::ProblemManagerCnf() { m_nbVar = 0; } // constructor +ProblemManagerCnf::ProblemManagerCnf() { m_nbVar = 0; } // constructor /** * @brief Construct a new Problem Manager Cnf:: Problem Manager Cnf object @@ -55,7 +58,11 @@ ProblemManagerCnf::ProblemManagerCnf(ProblemManager *problem) { m_maxVar = problem->getMaxVar(); m_indVar = problem->getIndVar(); m_isUnsat = false; -} // constructor + m_nbFreeVars = problem->freeVars(); + m_gmap = problem->gmap(); + + +} // constructor /** * @brief Construct a new Problem Manager Cnf:: Problem Manager Cnf object @@ -68,13 +75,14 @@ ProblemManagerCnf::ProblemManagerCnf(ProblemManager *problem) { */ ProblemManagerCnf::ProblemManagerCnf(int nbVar, std::vector &weightLit, std::vector &weightVar, - std::vector &selected) { + std::vector &selected, int freevars) { m_nbVar = nbVar; m_weightLit = weightLit; m_weightVar = weightVar; m_selected = selected; m_isUnsat = false; -} // constructor + m_nbFreeVars = freevars; +} // constructor /** Destructor. @@ -82,8 +90,47 @@ ProblemManagerCnf::ProblemManagerCnf(int nbVar, std::vector &weightLit, ProblemManagerCnf::~ProblemManagerCnf() { m_clauses.clear(); m_nbVar = 0; -} // destructor +} // destructor + +void ProblemManagerCnf::normalize() { + if (m_selected.size() != m_nbVar) { + std::vector marked(m_nbVar+1); + std::vector remap(m_nbVar+1); + int i = 1; + for (Var v : m_selected) { + marked[v] = true; + } + for (Var v = 1; v <= m_nbVar; v++) { + if (marked[v]) { + remap[v] = i; + i++; + } + } + for (Var v = 1; v <= m_nbVar; v++) { + if (!marked[v]) { + remap[v] = i; + i++; + } + } + for (auto &c : m_clauses) { + for (auto &l : c) { + l = Lit::makeLit(remap[l.var()], l.sign()); + } + } + int sel = m_selected.size(); + m_selected.clear(); + for (int i = 1; i <= sel; i++) { + m_selected.push_back(i); + } + } +} +void ProblemManagerCnf::normalizeInner() { + for (auto &cl : m_clauses) { + std::sort(cl.begin(), cl.end(), + [](Lit a, Lit b) { return a.var() < b.var(); }); + } +} /** * @brief Get the Unsat ProblemManager object. * @@ -103,7 +150,7 @@ ProblemManager *ProblemManagerCnf::getUnsatProblem() { ret->getClauses().push_back(cl); return ret; -} // getUnsatProblem +} // getUnsatProblem /** * @brief Simplify the formula by unit propagation and return the resulting CNF @@ -112,8 +159,8 @@ ProblemManager *ProblemManagerCnf::getUnsatProblem() { * @param units is the set of unit literals we want to condition with. * @return the simplified formula. */ -ProblemManager *ProblemManagerCnf::getConditionedFormula( - std::vector &units) { +ProblemManager * +ProblemManagerCnf::getConditionedFormula(std::vector &units) { ProblemManagerCnf *ret = new ProblemManagerCnf(this); std::vector value(m_nbVar + 1, 0); @@ -127,24 +174,28 @@ ProblemManager *ProblemManagerCnf::getConditionedFormula( std::vector scl; bool isSAT = false; for (auto l : cl) { - if (!value[l.var()]) scl.push_back(l); + if (!value[l.var()]) + scl.push_back(l); isSAT = l.sign() + 1 == value[l.var()]; - if (isSAT) break; + if (isSAT) + break; } // add the simplified clause if needed. - if (!isSAT) ret->getClauses().push_back(cl); + if (!isSAT) + ret->getClauses().push_back(cl); } return ret; -} // getConditionedFormula +} // getConditionedFormula /** Display the problem. @param[out] out, the stream where the messages are redirected. */ + void ProblemManagerCnf::display(std::ostream &out) { out << "weight list: "; for (unsigned i = 1; i <= m_nbVar; i++) { @@ -157,10 +208,11 @@ void ProblemManagerCnf::display(std::ostream &out) { out << "p cnf " << m_nbVar << " " << m_clauses.size() << "\n"; for (auto cl : m_clauses) { - for (auto &l : cl) out << l << " "; + for (auto &l : cl) + out << l << " "; out << "0\n"; } -} // diplay +} // diplay /** Print out some statistic about the problem. Each line will start with the @@ -177,11 +229,14 @@ void ProblemManagerCnf::displayStat(std::ostream &out, std::string startLine) { for (auto &c : m_clauses) { nbLits += c.size(); - if (c.size() == 2) nbBin++; - if (c.size() == 3) nbTer++; - if (c.size() > 3) nbMoreThree++; + if (c.size() == 2) + nbBin++; + if (c.size() == 3) + nbTer++; + if (c.size() > 3) + nbMoreThree++; } - + out << startLine << "Number of selected: " << m_selected.size() << "\n"; out << startLine << "Number of variables: " << m_nbVar << "\n"; out << startLine << "Number of clauses: " << m_clauses.size() << "\n"; out << startLine << "Number of binary clauses: " << nbBin << "\n"; @@ -189,6 +244,6 @@ void ProblemManagerCnf::displayStat(std::ostream &out, std::string startLine) { out << startLine << "Number of clauses larger than 3: " << nbMoreThree << "\n"; out << startLine << "Number of literals: " << nbLits << "\n"; -} // displaystat +} // displaystat -} // namespace d4 +} // namespace d4 diff --git a/src/problem/cnf/ProblemManagerCnf.hpp b/src/problem/cnf/ProblemManagerCnf.hpp index 30aaac5f..56c176f4 100644 --- a/src/problem/cnf/ProblemManagerCnf.hpp +++ b/src/problem/cnf/ProblemManagerCnf.hpp @@ -20,22 +20,26 @@ #include "../ProblemManager.hpp" #include "../ProblemTypes.hpp" #include "src/solvers/WrapperSolver.hpp" +#include "src/utils/IDIDFunc.hpp" namespace d4 { class ProblemManagerCnf : public ProblemManager { - private: +protected: std::vector> m_clauses; - - public: + std::vector> m_learnt; +public: ProblemManagerCnf(); ProblemManagerCnf(int nbVar, std::vector &weightLit, - std::vector &weightVar, std::vector &selected); + std::vector &weightVar, std::vector &selected,int freevars=0); ProblemManagerCnf(ProblemManager *problem); - ProblemManagerCnf(std::string &nameFile); ~ProblemManagerCnf(); + void normalize() override; + void normalizeInner() override; + void display(std::ostream &out) override; std::vector> &getClauses() { return m_clauses; } + std::vector> &getLearnt() { return m_learnt; } void setClauses(std::vector> &clauses) { m_clauses = clauses; } @@ -43,4 +47,4 @@ class ProblemManagerCnf : public ProblemManager { ProblemManager *getUnsatProblem() override; ProblemManager *getConditionedFormula(std::vector &units) override; }; -} // namespace d4 +} // namespace d4 diff --git a/src/problem/cnf/ProblemManagerGPMC.hpp b/src/problem/cnf/ProblemManagerGPMC.hpp new file mode 100644 index 00000000..2533efb4 --- /dev/null +++ b/src/problem/cnf/ProblemManagerGPMC.hpp @@ -0,0 +1,34 @@ +#pragma once +#include "ProblemManagerCnf.hpp" +#include "src/preprocs/cnf/PreprocGPMC.hpp" +#include "3rdParty/GPMC/core/Instance.h" + + +namespace d4{ +class ProblemManagerGPMC:public ProblemManagerCnf{ + +public: + ProblemManagerGPMC(GPMCInstance& instance,IDIDFunc proj_map){ + m_nbVar = instance.vars; + m_projMap = proj_map; + for(Var i = 1;i<=instance.npvars;i++){ + m_selected.push_back(i); + } + m_weightVar.resize((m_nbVar+1)+2,1.0); + m_weightVar.resize((m_nbVar+2)); + m_isUnsat = instance.unsat; + m_clauses.resize(instance.clauses.size()); + for(int i =0;i ncl(cl.size()); + for(int k = 0;k>& learnt) = 0; virtual bool solve(std::vector &setOfVar) = 0; virtual bool solve() = 0; + virtual void exportLearnt(std::vector>& clause) { + throw std::runtime_error("No solver support"); + + } virtual void uncheckedEnqueue(Lit l) = 0; virtual void restart() = 0; virtual void setAssumption(std::vector &assums) = 0; @@ -58,6 +62,9 @@ class WrapperSolver : public ActivityManager, public PolarityManager { // this function returns false if the propagation gives a conflict. virtual bool decideAndComputeUnit(Lit l, std::vector &units) = 0; + virtual bool decideAndComputeUnit(std::vector, std::vector &units){ + throw std::runtime_error("Unimplemented"); + } virtual void whichAreUnits(std::vector &component, std::vector &units) = 0; diff --git a/src/solvers/cnf/WrapperMinisat.cpp b/src/solvers/cnf/WrapperMinisat.cpp index 3d7b2a10..a75548c9 100644 --- a/src/solvers/cnf/WrapperMinisat.cpp +++ b/src/solvers/cnf/WrapperMinisat.cpp @@ -35,19 +35,34 @@ using minisat::toInt; @param[in] p, the problem we want to link with the SAT solver. */ + +void WrapperMinisat::addClause(std::vector &cl, bool learnt) { + std::vector ps(cl.size()); + for (int i = 0; i < cl.size(); i++) { + ps[i] = minisat::mkLit(cl[i].var(), cl[i].sign()); + } + minisat::CRef cr = s.ca.alloc(ps, learnt); + if (!learnt) + s.clauses.push(cr); + else + s.learnts.push(cr); + s.attachClause(cr); +} void WrapperMinisat::initSolver(ProblemManager &p) { try { ProblemManagerCnf &pcnf = dynamic_cast(p); // say to the solver we have pcnf.getNbVar() variables. - while ((unsigned)s.nVars() <= pcnf.getNbVar()) s.newVar(); + while ((unsigned)s.nVars() <= pcnf.getNbVar()) + s.newVar(); m_model.resize(pcnf.getNbVar() + 1, l_Undef); // load the clauses std::vector> &clauses = pcnf.getClauses(); for (auto &cl : clauses) { minisat::vec lits; - for (auto &l : cl) lits.push(minisat::mkLit(l.var(), l.sign())); + for (auto &l : cl) + lits.push(minisat::mkLit(l.var(), l.sign())); s.addClause(lits); } } catch (std::bad_cast &bc) { @@ -59,8 +74,43 @@ void WrapperMinisat::initSolver(ProblemManager &p) { m_needModel = false; setNeedModel(m_needModel); m_isInAssumption.resize(p.getNbVar() + 1, 0); -} // initSolver +} // initSolver + +void WrapperMinisat::initSolver(ProblemManager &p, + std::vector> &learnt) { + try { + ProblemManagerCnf &pcnf = dynamic_cast(p); + + // force glucose to be in incremental mode in order to restart just after + // the assumptions. + // s.setIncrementalMode(); + + // say to the solver we have pcnf.getNbVar() variables. + while ((unsigned)s.nVars() <= pcnf.getNbVar()) + s.newVar(); + m_model.resize(pcnf.getNbVar() + 1, l_Undef); + + // load the clauses + std::vector> &clauses = pcnf.getClauses(); + for (auto &cl : clauses) { + minisat::vec lits; + for (auto &l : cl) + lits.push(minisat::mkLit(l.var(), l.sign())); + s.addClause(lits); + } + for (auto cl : learnt) { + addClause(cl, true); + } + } catch (std::bad_cast &bc) { + std::cerr << "bad_cast caught: " << bc.what() << '\n'; + std::cerr << "A CNF formula was expeted\n"; + } + m_activeModel = false; + m_needModel = false; + setNeedModel(m_needModel); + m_isInAssumption.resize(p.getNbVar() + 1, 0); +} /** Call the SAT solver and return its result. @@ -69,15 +119,17 @@ void WrapperMinisat::initSolver(ProblemManager &p) { \return true if the problem is SAT, false otherwise. */ bool WrapperMinisat::solve(std::vector &setOfVar) { - if (m_activeModel && m_needModel) return true; + if (m_activeModel && m_needModel) + return true; m_setOfVar_m.setSize(0); - for (auto &v : setOfVar) m_setOfVar_m.push(v); + for (auto &v : setOfVar) + m_setOfVar_m.push(v); s.rebuildWithConnectedComponent(m_setOfVar_m); m_activeModel = s.solveWithAssumptions(); return m_activeModel; -} // solve +} // solve /** Call the SAT solver and return its result. @@ -87,7 +139,7 @@ bool WrapperMinisat::solve(std::vector &setOfVar) { bool WrapperMinisat::solve() { s.rebuildWithAllVar(); return s.solveWithAssumptions(); -} // solve +} // solve /** * @brief Enforce the unit propagation of all the assumption literals. @@ -96,7 +148,7 @@ bool WrapperMinisat::solve() { */ bool WrapperMinisat::propagateAssumption() { return s.propagateAssumption(); -} // propagateAssumption +} // propagateAssumption /** * @brief Strong assumption in the sense we push the literal on the stack. @@ -105,7 +157,7 @@ bool WrapperMinisat::propagateAssumption() { */ void WrapperMinisat::uncheckedEnqueue(Lit l) { s.uncheckedEnqueue(minisat::mkLit(l.var(), l.sign())); -} // uncheckedEnqueue +} // uncheckedEnqueue /** An accessor on the activity of a variable. @@ -116,7 +168,7 @@ void WrapperMinisat::uncheckedEnqueue(Lit l) { */ double WrapperMinisat::getActivity(Var v) { return s.activity[v]; -} // getActivity +} // getActivity /** * @brief Set the reverse polarity flag to the solver. @@ -125,7 +177,7 @@ double WrapperMinisat::getActivity(Var v) { */ void WrapperMinisat::setReversePolarity(bool value) { s.reversePolarity = value; -} // setReversePolarity +} // setReversePolarity /** * @brief Return the number of times the variable v occurs in a conflict. @@ -134,7 +186,7 @@ void WrapperMinisat::setReversePolarity(bool value) { */ double WrapperMinisat::getCountConflict(Var v) { return s.scoreActivity[v]; -} // getCountConflict +} // getCountConflict /** * @brief Set the count conflict in the solver. @@ -143,21 +195,19 @@ double WrapperMinisat::getCountConflict(Var v) { */ void WrapperMinisat::setCountConflict(Var v, double count) { s.scoreActivity[v] = count; -} // setCountConflict +} // setCountConflict /** Print out the trail on the standard output. */ -void WrapperMinisat::showTrail() { s.showTrail(); } // showTrail +void WrapperMinisat::showTrail() { s.showTrail(); } // showTrail /** An accessor on the polarity of a variable. @param[in] v, the variable we want the polarity. */ -bool WrapperMinisat::getPolarity(Var v) { - return s.polarity[v]; -} // getPolarity +bool WrapperMinisat::getPolarity(Var v) { return s.polarity[v]; } // getPolarity /** Collect the unit literal from the affectation of the literal l to the @@ -172,7 +222,8 @@ bool WrapperMinisat::getPolarity(Var v) { bool WrapperMinisat::decideAndComputeUnit(Lit l, std::vector &units) { minisat::Lit ml = minisat::mkLit(l.var(), l.sign()); if (varIsAssigned(l.var())) { - if (s.litAssigned(l.var()) != ml) return false; + if (s.litAssigned(l.var()) != ml) + return false; units.push_back(l); return true; } @@ -182,7 +233,7 @@ bool WrapperMinisat::decideAndComputeUnit(Lit l, std::vector &units) { s.uncheckedEnqueue(ml); minisat::CRef confl = s.propagate(); - if (confl != minisat::CRef_Undef) // unit literal + if (confl != minisat::CRef_Undef) // unit literal { int bt; minisat::vec learnt_clause; @@ -197,7 +248,36 @@ bool WrapperMinisat::decideAndComputeUnit(Lit l, std::vector &units) { units.push_back(Lit::makeLit(var(s.trail[j]), sign(s.trail[j]))); s.cancelUntil(s.decisionLevel() - 1); return true; -} // decideAndComputeUnit +} // decideAndComputeUnit +bool WrapperMinisat::decideAndComputeUnit(std::vector lits, + std::vector &units) { + std::vector mlits; + for (auto l : lits) { + mlits.push_back(minisat::mkLit(l.var(), l.sign())); + if (varIsAssigned(l.var())) { + if (s.litAssigned(l.var()) != mlits.back()) + return false; + units.push_back(l); + return true; + } + } + + int posTrail = (s.trail).size(); + s.newDecisionLevel(); + for (auto l : mlits) { + s.uncheckedEnqueue(l); + } + minisat::CRef confl = s.propagate(); + if (confl != minisat::CRef_Undef) // unit literal + { + s.cancelUntil(s.decisionLevel() - 1); + return false; + } + for (int j = posTrail; j < s.trail.size(); j++) + units.push_back(Lit::makeLit(var(s.trail[j]), sign(s.trail[j]))); + s.cancelUntil(s.decisionLevel() - 1); + return true; +} // decideAndComputeUnit /** Fill the vector units with the literal l that are units such that l.var() is @@ -209,11 +289,12 @@ bool WrapperMinisat::decideAndComputeUnit(Lit l, std::vector &units) { void WrapperMinisat::whichAreUnits(std::vector &component, std::vector &units) { for (auto &v : component) { - if (!s.isAssigned(v)) continue; + if (!s.isAssigned(v)) + continue; minisat::Lit l = s.litAssigned(v); units.push_back(Lit::makeLit(var(l), sign(l))); } -} // whichAreUnits +} // whichAreUnits /** * @brief Get the list of unit literals that are in the trail (we suppose that @@ -226,7 +307,7 @@ void WrapperMinisat::getUnits(std::vector &units) { minisat::Lit l = s.trail[i]; units.push_back(Lit::makeLit(var(l), sign(l))); } -} // getUnits +} // getUnits /** Check out if the given variable is assigned or not by the solver. @@ -237,12 +318,12 @@ void WrapperMinisat::getUnits(std::vector &units) { */ bool WrapperMinisat::varIsAssigned(Var v) { return s.isAssigned(v); -} // varIsAssigned +} // varIsAssigned /** Restart the solver. */ -void WrapperMinisat::restart() { s.cancelUntil(0); } // restart +void WrapperMinisat::restart() { s.cancelUntil(0); } // restart /** Transfer to the solver the fact we have a set of assumption variables we want @@ -255,8 +336,9 @@ void WrapperMinisat::setAssumption(std::vector &assums) { minisat::vec &assumptions = s.assumptions; assumptions.clear(); m_assumption.clear(); - for (auto &l : assums) pushAssumption(l); -} // setAssumption + for (auto &l : assums) + pushAssumption(l); +} // setAssumption /** \return the current assumption. @@ -265,7 +347,7 @@ void WrapperMinisat::setAssumption(std::vector &assums) { */ std::vector &WrapperMinisat::getAssumption() { return m_assumption; -} // getAssumption +} // getAssumption /** Print out the assumption. @@ -279,7 +361,7 @@ void WrapperMinisat::displayAssumption(std::ostream &out) { std::cout << (minisat::sign(l) ? "-" : "") << minisat::var(l) << " "; } std::cout << "\n"; -} // displayAssumption +} // displayAssumption /** Ask for the model. @@ -289,7 +371,7 @@ void WrapperMinisat::displayAssumption(std::ostream &out) { void WrapperMinisat::setNeedModel(bool b) { m_needModel = b; s.setNeedModel(b); -} // setNeedModel +} // setNeedModel /** * @brief Return the model computed by the solver. @@ -307,7 +389,7 @@ std::vector &WrapperMinisat::getModel() { } return m_model; -} // getModel +} // getModel /** * @brief Get the value given by the last computed model. @@ -317,7 +399,7 @@ std::vector &WrapperMinisat::getModel() { */ lbool WrapperMinisat::getModelVar(Var v) { return minisat::toInt(s.model[v]); -} // getModelVar +} // getModelVar /** Push a new assumption. @@ -344,7 +426,7 @@ void WrapperMinisat::pushAssumption(Lit l) { assert(cref == minisat::CRef_Undef); } } -} // pushAssumption +} // pushAssumption /** Remove the last assumption and cancelUntil. @@ -360,7 +442,14 @@ void WrapperMinisat::popAssumption(unsigned count) { m_assumption.resize(m_assumption.size() - count); (s.assumptions).shrink_(count); (s.cancelUntil)((s.assumptions).size()); -} // popAssumption +} // popAssumption inline unsigned WrapperMinisat::getNbConflict() { return s.conflicts; } -} // namespace d4 + +void WrapperMinisat::decay() { + for (int i = 0; i < s.activity.size(); i++) { + s.activity[i] = s.activity[i] * 0.5; + } +} + +} // namespace d4 diff --git a/src/solvers/cnf/WrapperMinisat.hpp b/src/solvers/cnf/WrapperMinisat.hpp index 6b2794c4..8754cbee 100644 --- a/src/solvers/cnf/WrapperMinisat.hpp +++ b/src/solvers/cnf/WrapperMinisat.hpp @@ -1,4 +1,4 @@ -/* +/*Mini * d4 * Copyright (C) 2020 Univ. Artois & CNRS * @@ -38,12 +38,17 @@ class WrapperMinisat : public WrapperSolver { public: void initSolver(ProblemManager &p) override; + void initSolver(ProblemManager &p,std::vector>& learnt) override; + virtual ~WrapperMinisat(){} + +void addClause(std::vector& cl,bool learnt); bool solve(std::vector &setOfVar) override; bool solve() override; void uncheckedEnqueue(Lit l) override; bool varIsAssigned(Var v) override; bool getPolarity(Var v) override; bool decideAndComputeUnit(Lit l, std::vector &units) override; + bool decideAndComputeUnit(std::vector, std::vector &units) override; void whichAreUnits(std::vector &component, std::vector &units) override; void restart() override; @@ -64,5 +69,6 @@ class WrapperMinisat : public WrapperSolver { void setCountConflict(Var v, double count) override; unsigned getNbConflict() override; void setReversePolarity(bool value) override; + virtual void decay(); }; } // namespace d4 diff --git a/src/specs/SpecManager.cpp b/src/specs/SpecManager.cpp index cb9583d9..8be0f80b 100644 --- a/src/specs/SpecManager.cpp +++ b/src/specs/SpecManager.cpp @@ -25,7 +25,7 @@ namespace d4 { /** Generate an occurrence manager regarding the options given as parameter. - @param[in] config, the configuration. + @param[in] vm, the arguments on the command line. @param[in] p, a problem manager. \return the occurrence manager that fits the command line. @@ -33,14 +33,18 @@ namespace d4 { SpecManager *SpecManager::makeSpecManager(Config &config, ProblemManager &p, std::ostream &out) { - out << "c [CONSTRUCTOR SPEC] Spec manager: " << config.occurrence_manager << " " << config.input_type << "\n"; + std::string inType = config.input_type; + std::string meth = config.occurrence_manager; - if (config.input_type == "cnf" || config.input_type == "dimacs") { - if (config.occurrence_manager == "dynamic") return new SpecManagerCnfDyn(p); + out << "c [CONSTRUCTOR SPEC] Spec manager: " << meth << " " << inType << "\n"; + + if (inType == "cnf" || inType == "dimacs") { + if (meth == "dynamic") + return new SpecManagerCnfDyn(p); return NULL; } throw(FactoryException("Cannot create a SpecManager", __FILE__, __LINE__)); -} // makeSpecManager +} // makeSpecManager -} // namespace d4 +} // namespace d4 diff --git a/src/specs/SpecManager.hpp b/src/specs/SpecManager.hpp index 34b3574a..8b2b6adb 100644 --- a/src/specs/SpecManager.hpp +++ b/src/specs/SpecManager.hpp @@ -16,27 +16,41 @@ * along with this program. If not, see . */ #pragma once - +#include "src/utils/Proj.hpp" +#include +#include +#include +#include #include -#include "src/config/Config.hpp" -#include "src/problem/ProblemManager.hpp" -#include "src/problem/ProblemTypes.hpp" - namespace d4 { +namespace po = boost::program_options; class SpecManager { - public: +protected: + unsigned m_nbVar; + unsigned m_nbProj; + +public: static SpecManager *makeSpecManager(Config &config, ProblemManager &p, std::ostream &out); + inline bool isSelected(Var v) { return v <= m_nbProj; } + inline bool isProj() { return m_nbProj != m_nbVar; } + inline int nbSelected() { return m_nbProj; } + virtual ~SpecManager() {} virtual bool litIsAssigned(Lit l) = 0; virtual bool litIsAssignedToTrue(Lit l) = 0; virtual bool varIsAssigned(Var v) = 0; - virtual int computeConnectedComponent( - std::vector> &varConnected, std::vector &setOfVar, - std::vector &freeVar) = 0; + virtual int + computeConnectedComponent(std::vector> &varConnected, + std::vector &setOfVar, + std::vector &freeVar) = 0; + virtual int computeConnectedComponent(std::vector &varConnected, + std::vector &setOfVar, + std::vector &freeVar) = 0; virtual void preUpdate(std::vector &lits) = 0; + virtual void preUpdate(std::vector &lits,std::vector& pure ) = 0; virtual void postUpdate(std::vector &lits) = 0; virtual void initialize(std::vector &setOfVar, std::vector &units) = 0; @@ -46,4 +60,4 @@ class SpecManager { virtual int getNbOccurrence(Lit l) = 0; virtual int getNbVariable() = 0; }; -} // namespace d4 +} // namespace d4 diff --git a/src/specs/cnf/SpecManagerCnf.cpp b/src/specs/cnf/SpecManagerCnf.cpp index 36b6ae7b..f3b8a174 100644 --- a/src/specs/cnf/SpecManagerCnf.cpp +++ b/src/specs/cnf/SpecManagerCnf.cpp @@ -18,20 +18,26 @@ #include "SpecManagerCnf.hpp" -#include // std::sort +#include // std::sort #include +#include #include "SpecManagerCnfDyn.hpp" #include "src/methods/nnf/Node.hpp" #include "src/problem/ProblemTypes.hpp" + + + + namespace d4 { /** Constructor. */ -SpecManagerCnf::SpecManagerCnf(ProblemManager &p) : m_nbVar(p.getNbVar()) { +SpecManagerCnf::SpecManagerCnf(ProblemManager &p) { // get the clauses. + m_nbVar = (p.getNbVar()); try { ProblemManagerCnf &pcnf = dynamic_cast(p); m_clauses = pcnf.getClauses(); @@ -45,9 +51,11 @@ SpecManagerCnf::SpecManagerCnf(ProblemManager &p) : m_nbVar(p.getNbVar()) { unsigned count = 0; std::vector> occurrence((m_nbVar + 1) << 1); for (unsigned i = 0; i < m_clauses.size(); i++) { - if (m_clauses[i].size() > 2) m_clausesNotBin.push_back(i); + if (m_clauses[i].size() > 2) + m_clausesNotBin.push_back(i); - for (auto &l : m_clauses[i]) occurrence[l.intern()].push_back(i); + for (auto &l : m_clauses[i]) + occurrence[l.intern()].push_back(i); count += m_clauses[i].size(); if (m_clauses[i].size() > m_maxSizeClause) @@ -93,9 +101,9 @@ SpecManagerCnf::SpecManagerCnf(ProblemManager &p) : m_nbVar(p.getNbVar()) { for (unsigned i = 0; i < m_clauses.size(); i++) { m_infoClauses[i].watcher = m_clauses[i][0]; } - m_infoCluster.resize(p.getNbVar() + nbClause + 1, {0, 0, -1}); -} // construtor + m_nbProj = p.getNbSelectedVar(); +} // construtor /** * @brief Destroy the Spec Manager Cnf:: Spec Manager Cnf object @@ -103,7 +111,7 @@ SpecManagerCnf::SpecManagerCnf(ProblemManager &p) : m_nbVar(p.getNbVar()) { */ SpecManagerCnf::~SpecManagerCnf() { delete[] m_dataOccurrenceMemory; -} // destructor +} // destructor /** Look all the formula in order to compute the connected component @@ -126,13 +134,14 @@ int SpecManagerCnf::computeConnectedComponent( } for (auto const &v : setOfVar) { - if (m_currentValue[v] != l_Undef) continue; + if (m_currentValue[v] != l_Undef) + continue; // visit the index clauses Var rootV = v; Lit l = Lit::makeLit(v, false); - for (unsigned i = 0; i < 2; i++) { // both literals. + for (unsigned i = 0; i < 2; i++) { // both literals. IteratorIdxClause listIndex = getVecIdxClause(l); for (int *ptr = listIndex.start; ptr != listIndex.end; ptr++) { @@ -152,7 +161,8 @@ int SpecManagerCnf::computeConnectedComponent( } // already in the same component. - if (rootV == rootW) continue; + if (rootV == rootW) + continue; // union. if (m_infoCluster[rootV].size < m_infoCluster[rootW].size) { @@ -175,7 +185,8 @@ int SpecManagerCnf::computeConnectedComponent( freeVar.resize(0); for (auto const &v : setOfVar) { - if (m_currentValue[v] != l_Undef) continue; + if (m_currentValue[v] != l_Undef) + continue; if (m_infoCluster[v].parent == v && m_infoCluster[v].size == 1) { freeVar.push_back(v); @@ -204,10 +215,109 @@ int SpecManagerCnf::computeConnectedComponent( // restore for the next run. resetUnMark(); - for (auto &v : rootSet) m_infoCluster[v].pos = -1; + for (auto &v : rootSet) + m_infoCluster[v].pos = -1; + + return varCo.size(); +} // computeConnectedComponent + // +int SpecManagerCnf::computeConnectedComponent(std::vector &varCo, + std::vector &setOfVar, + std::vector &freeVar) { + for (auto v : setOfVar) { + assert(v < m_infoCluster.size()); + m_infoCluster[v].parent = v; + m_infoCluster[v].size = 1; + } + + for (auto const &v : setOfVar) { + if (m_currentValue[v] != l_Undef) + continue; + + // visit the index clauses + Var rootV = v; + Lit l = Lit::makeLit(v, false); + + for (unsigned i = 0; i < 2; i++) { // both literals. + IteratorIdxClause listIndex = getVecIdxClause(l); + + for (int *ptr = listIndex.start; ptr != listIndex.end; ptr++) { + int idx = *ptr; + if (!m_markView[idx]) { + m_markView[idx] = true; + m_infoCluster[idx + m_nbVar + 1].parent = rootV; + m_infoCluster[rootV].size++; + m_mustUnMark.push_back(idx); + } else { + // search for the root. + Var rootW = m_infoCluster[idx + m_nbVar + 1].parent; + while (rootW != m_infoCluster[rootW].parent) { + m_infoCluster[rootW].parent = + m_infoCluster[m_infoCluster[rootW].parent].parent; + rootW = m_infoCluster[rootW].parent; + } + + // already in the same component. + if (rootV == rootW) + continue; + + // union. + if (m_infoCluster[rootV].size < m_infoCluster[rootW].size) { + m_infoCluster[rootW].size += m_infoCluster[rootV].size; + m_infoCluster[rootV].parent = m_infoCluster[rootW].parent; + rootV = rootW; + } else { + m_infoCluster[rootV].size += m_infoCluster[rootW].size; + m_infoCluster[rootW].parent = m_infoCluster[rootV].parent; + } + } + } + + l = ~l; + } + } + + // collect the component. + std::vector rootSet; + freeVar.resize(0); + + for (auto const &v : setOfVar) { + if (m_currentValue[v] != l_Undef) + continue; + + if (m_infoCluster[v].parent == v && m_infoCluster[v].size == 1) { + freeVar.push_back(v); + assert(getNbClause(v) == 0); + continue; + } + assert(getNbClause(v) != 0); + assert(m_currentValue[v] == l_Undef); + + // get the root. + unsigned rootV = m_infoCluster[v].parent; + while (rootV != m_infoCluster[rootV].parent) { + m_infoCluster[rootV].parent = + m_infoCluster[m_infoCluster[rootV].parent].parent; + rootV = m_infoCluster[rootV].parent; + } + + if (m_infoCluster[rootV].pos == -1) { + m_infoCluster[rootV].pos = varCo.size(); + varCo.push_back(ProjVars()); + rootSet.push_back(rootV); + } + + varCo[m_infoCluster[rootV].pos].vars.push_back(v); + varCo[m_infoCluster[rootV].pos].nbProj += isSelected(v); + } + + // restore for the next run. + resetUnMark(); + for (auto &v : rootSet) + m_infoCluster[v].pos = -1; return varCo.size(); -} // computeConnectedComponent +} /** Test if a given clause is actually satisfied under the current @@ -220,7 +330,7 @@ int SpecManagerCnf::computeConnectedComponent( bool SpecManagerCnf::isSatisfiedClause(unsigned idx) { assert(idx < m_clauses.size()); return m_infoClauses[idx].nbSat; -} // isSatisfiedClause +} // isSatisfiedClause /** Test if a given clause is actually satisfied under the current @@ -232,13 +342,16 @@ bool SpecManagerCnf::isSatisfiedClause(unsigned idx) { */ bool SpecManagerCnf::isSatisfiedClause(std::vector &c) { for (auto &l : c) { - if (!litIsAssigned(l)) continue; - if (l.sign() && m_currentValue[l.var()] == l_False) return true; - if (!l.sign() && m_currentValue[l.var()] == l_True) return true; + if (!litIsAssigned(l)) + continue; + if (l.sign() && m_currentValue[l.var()] == l_False) + return true; + if (!l.sign() && m_currentValue[l.var()] == l_True) + return true; } return false; -} // isSatisfiedClause +} // isSatisfiedClause /** Test at the same time if a given clause is actually satisfied under @@ -254,33 +367,38 @@ bool SpecManagerCnf::isSatisfiedClause(std::vector &c) { */ bool SpecManagerCnf::isNotSatisfiedClauseAndInComponent( int idx, std::vector &m_inCurrentComponent) { - if (m_infoClauses[idx].nbSat) return false; + if (m_infoClauses[idx].nbSat) + return false; assert(m_infoClauses[idx].watcher != lit_Undef); assert(!litIsAssigned(m_infoClauses[idx].watcher)); return m_inCurrentComponent[m_infoClauses[idx].watcher.var()]; -} // isSatisfiedClause +} // isSatisfiedClause void SpecManagerCnf::getCurrentClauses(std::vector &idxClauses, std::vector &component) { idxClauses.resize(0); - for (auto &v : component) m_inCurrentComponent[v] = true; + for (auto &v : component) + m_inCurrentComponent[v] = true; for (unsigned i = 0; i < m_clauses.size(); i++) { if (isNotSatisfiedClauseAndInComponent(i, m_inCurrentComponent)) idxClauses.push_back(i); } - for (auto &v : component) m_inCurrentComponent[v] = false; -} // getCurrentclauses + for (auto &v : component) + m_inCurrentComponent[v] = false; +} // getCurrentclauses void SpecManagerCnf::getCurrentClausesNotBin(std::vector &idxClauses, std::vector &component) { idxClauses.resize(0); - for (auto &v : component) m_inCurrentComponent[v] = true; + for (auto &v : component) + m_inCurrentComponent[v] = true; for (auto &i : m_clausesNotBin) { if (isNotSatisfiedClauseAndInComponent(i, m_inCurrentComponent)) idxClauses.push_back(i); } - for (auto &v : component) m_inCurrentComponent[v] = false; -} // getCurrentclauses + for (auto &v : component) + m_inCurrentComponent[v] = false; +} // getCurrentclauses void SpecManagerCnf::showFormula(std::ostream &out) { out << "p cnf " << getNbVariable() << " " << getNbClause() << "\n"; @@ -288,11 +406,12 @@ void SpecManagerCnf::showFormula(std::ostream &out) { showListLit(out, cl); out << "0\n"; } -} // showFormula +} // showFormula void SpecManagerCnf::showTrail(std::ostream &out) { for (int i = 0; i < getNbVariable(); i++) { - if (!varIsAssigned(i)) continue; + if (!varIsAssigned(i)) + continue; Lit l = Lit::makeLit(i, false); if (litIsAssignedToTrue(l)) out << l << " "; @@ -300,15 +419,17 @@ void SpecManagerCnf::showTrail(std::ostream &out) { out << ~l << " "; } out << "\n"; -} // showFormula +} // showFormula void SpecManagerCnf::showCurrentFormula(std::ostream &out) { out << "p cnf " << getNbVariable() << " " << getNbClause() << "\n"; for (unsigned i = 0; i < m_clauses.size(); i++) { - if (m_infoClauses[i].nbSat) continue; + if (m_infoClauses[i].nbSat) + continue; for (auto &l : m_clauses[i]) - if (!litIsAssigned(l)) out << l << " "; + if (!litIsAssigned(l)) + out << l << " "; out << "0\n"; } -} // showFormula -} // namespace d4 +} // showFormula +} // namespace d4 diff --git a/src/specs/cnf/SpecManagerCnf.hpp b/src/specs/cnf/SpecManagerCnf.hpp index c7168059..145b1a66 100644 --- a/src/specs/cnf/SpecManagerCnf.hpp +++ b/src/specs/cnf/SpecManagerCnf.hpp @@ -24,13 +24,13 @@ #include "src/problem/ProblemManager.hpp" #include "src/problem/cnf/ProblemManagerCnf.hpp" #include "src/utils/Enum.hpp" +#include "src/utils/Proj.hpp" namespace d4 { struct SpecClauseInfo { unsigned nbSat; unsigned nbUnsat; Lit watcher; - SpecClauseInfo() : nbSat(0), nbUnsat(0), watcher(lit_Undef) { ; } }; @@ -41,15 +41,16 @@ struct InfoCluster { }; class SpecManagerCnf : public SpecManager { - protected: +protected: std::vector> m_clauses; std::vector m_clausesNotBin; - unsigned m_nbVar, m_maxSizeClause; + unsigned m_maxSizeClause; std::vector m_currentValue; std::vector m_infoClauses; std::vector m_inCurrentComponent; std::vector m_occurrence; + std::vector cleaness; int *m_dataOccurrenceMemory; std::vector m_infoCluster; @@ -61,11 +62,12 @@ class SpecManagerCnf : public SpecManager { std::vector m_markView; inline void resetUnMark() { - for (auto &idx : m_mustUnMark) m_markView[idx] = false; + for (auto &idx : m_mustUnMark) + m_markView[idx] = false; m_mustUnMark.resize(0); - } // resetUnMark + } // resetUnMark - public: +public: SpecManagerCnf(ProblemManager &p); ~SpecManagerCnf(); @@ -73,9 +75,20 @@ class SpecManagerCnf : public SpecManager { std::vector &setOfVar, std::vector &freeVar) override; + int computeConnectedComponent(std::vector &varConnected, + std::vector &setOfVar, + std::vector &freeVar) override; + void showFormula(std::ostream &out) override; void showCurrentFormula(std::ostream &out) override; void showTrail(std::ostream &out) override; + void freeVars(std::vector &component, std::vector &free) { + for (auto v : component) { + if (getNbClause(v) == 0) { + free.push_back(v); + } + } + } int getInitSize(int i) { return m_clauses[i].size(); } int getCurrentSize(int i) { @@ -84,8 +97,9 @@ class SpecManagerCnf : public SpecManager { bool isSatisfiedClause(unsigned idx); bool isSatisfiedClause(std::vector &c); - bool isNotSatisfiedClauseAndInComponent( - int idx, std::vector &m_inCurrentComponent); + bool + isNotSatisfiedClauseAndInComponent(int idx, + std::vector &m_inCurrentComponent); void getCurrentClauses(std::vector &idxClauses, std::vector &component); @@ -119,16 +133,18 @@ class SpecManagerCnf : public SpecManager { virtual inline int getSumSizeClauses() { int sum = 0; - for (auto &cl : m_clauses) sum += cl.size(); + for (auto &cl : m_clauses) + sum += cl.size(); return sum; - } // getSumSizeClauses + } // getSumSizeClauses inline int getNbBinaryClause(Lit l) { int nbBin = m_occurrence[l.intern()].nbBin; for (unsigned i = 0; i < m_occurrence[l.intern()].nbNotBin; i++) - if (getSize(m_occurrence[l.intern()].notBin[i]) == 2) nbBin++; + if (getSize(m_occurrence[l.intern()].notBin[i]) == 2) + nbBin++; return nbBin; - } // getNbBinaryClause + } // getNbBinaryClause // about the clauses. inline int getNbUnsat(int idx) { return m_infoClauses[idx].nbUnsat; } @@ -141,7 +157,7 @@ class SpecManagerCnf : public SpecManager { return m_clauses[idx]; } - // about the assignment. + // about the asdssignment. inline bool varIsAssigned(Var v) override { return m_currentValue[v] != l_Undef; } @@ -174,14 +190,17 @@ class SpecManagerCnf : public SpecManager { inline IteratorIdxClause getVecIdxClause(Lit l, ModeStore mode) { assert(l.intern() < m_occurrence.size()); - if (mode == NT) return m_occurrence[l.intern()].getNotBinClauses(); - if (mode == ALL) return m_occurrence[l.intern()].getClauses(); + if (mode == NT) + return m_occurrence[l.intern()].getNotBinClauses(); + if (mode == ALL) + return m_occurrence[l.intern()].getClauses(); return m_occurrence[l.intern()].getBinClauses(); } inline void showOccurenceList(std::ostream &out) { for (unsigned i = 0; i < m_occurrence.size(); i++) { - if (!m_occurrence[i].nbBin && !m_occurrence[i].nbNotBin) continue; + if (!m_occurrence[i].nbBin && !m_occurrence[i].nbNotBin) + continue; out << ((i & 1) ? "-" : "") << (i >> 1) << " --> [ "; for (unsigned j = 0; j < m_occurrence[i].nbBin; j++) out << m_occurrence[i].bin[j] << " "; @@ -191,4 +210,4 @@ class SpecManagerCnf : public SpecManager { } } }; -} // namespace d4 +} // namespace d4 diff --git a/src/specs/cnf/SpecManagerCnfDyn.cpp b/src/specs/cnf/SpecManagerCnfDyn.cpp index 00ad4c66..77e14d1e 100644 --- a/src/specs/cnf/SpecManagerCnfDyn.cpp +++ b/src/specs/cnf/SpecManagerCnfDyn.cpp @@ -30,21 +30,22 @@ namespace d4 { @param[in] _nbVar, the number of variables in the problem */ SpecManagerCnfDyn::SpecManagerCnfDyn(ProblemManager &p) - : SpecManagerCnf(p) {} // SpecManagerCnfDyn + : SpecManagerCnf(p) {} // SpecManagerCnfDyn /** Update the occurrence list w.r.t. a new set of assigned variables. It's important that the order is conserved between the moment where - we assign and the moment we unassign. + we assign and tVsadshe moment we unassign. @param[in] lits, the new assigned variables */ + void SpecManagerCnfDyn::preUpdate(std::vector &lits) { m_reviewWatcher.resize(0); for (auto &l : lits) { + assert(!litIsAssigned(l)); m_currentValue[l.var()] = l.sign() ? l_False : l_True; - // not binary clauses. for (unsigned i = 0; i < m_occurrence[l.intern()].nbNotBin; i++) { int idxCl = m_occurrence[l.intern()].notBin[i]; @@ -59,7 +60,8 @@ void SpecManagerCnfDyn::preUpdate(std::vector &lits) { int idxCl = m_occurrence[(~l).intern()].notBin[i]; m_infoClauses[idxCl].nbUnsat++; - if (m_infoClauses[idxCl].watcher == ~l) m_reviewWatcher.push_back(idxCl); + if (m_infoClauses[idxCl].watcher == ~l) + m_reviewWatcher.push_back(idxCl); } // binary clauses. @@ -74,13 +76,85 @@ void SpecManagerCnfDyn::preUpdate(std::vector &lits) { for (unsigned i = 0; i < m_occurrence[(~l).intern()].nbBin; i++) { int idxCl = m_occurrence[(~l).intern()].bin[i]; m_infoClauses[idxCl].nbUnsat++; - if (m_infoClauses[idxCl].watcher == ~l) m_reviewWatcher.push_back(idxCl); + if (m_infoClauses[idxCl].watcher == ~l) + m_reviewWatcher.push_back(idxCl); + } + } + + // we search another non assigned literal if requiered + for (auto &idxCl : m_reviewWatcher) { + if (m_infoClauses[idxCl].nbSat) + continue; + + for (auto &l : m_clauses[idxCl]) { + if (m_currentValue[l.var()] == l_Undef) { + m_infoClauses[idxCl].watcher = l; + break; + } + } + } +} // preUpdate +void SpecManagerCnfDyn::preUpdate(std::vector &lits, + std::vector &pure) { + m_reviewWatcher.resize(0); + + for (auto &l : lits) { + m_currentValue[l.var()] = l.sign() ? l_False : l_True; + // not binary clauses. + for (unsigned i = 0; i < m_occurrence[l.intern()].nbNotBin; i++) { + int idxCl = m_occurrence[l.intern()].notBin[i]; + m_infoClauses[idxCl].nbSat++; + for (auto &ll : m_clauses[idxCl]) + if (m_currentValue[ll.var()] == l_Undef) { + m_occurrence[ll.intern()].removeNotBin(idxCl); + if (!isSelected(ll.var())&&!litIsAssigned(ll) &&m_occurrence[ll.intern()].nbNotBin == 0 && + m_occurrence[ll.intern()].nbBin == 0 && + m_occurrence[(~ll).intern()].nbBin + + m_occurrence[(~ll).intern()].nbNotBin > + 0) { + pure.push_back(~ll); + } + } + } + + for (unsigned i = 0; i < m_occurrence[(~l).intern()].nbNotBin; i++) { + int idxCl = m_occurrence[(~l).intern()].notBin[i]; + + m_infoClauses[idxCl].nbUnsat++; + if (m_infoClauses[idxCl].watcher == ~l) + m_reviewWatcher.push_back(idxCl); + } + + // binary clauses. + for (unsigned i = 0; i < m_occurrence[l.intern()].nbBin; i++) { + int idxCl = m_occurrence[l.intern()].bin[i]; + m_infoClauses[idxCl].nbSat++; + for (auto &ll : m_clauses[idxCl]) { + if (m_currentValue[ll.var()] == l_Undef) { + m_occurrence[ll.intern()].removeBin(idxCl); + if (!isSelected(ll.var())&&!litIsAssigned(ll)&&m_occurrence[ll.intern()].nbBin == 0 && + m_occurrence[ll.intern()].nbNotBin == 0 && + m_occurrence[(~ll).intern()].nbBin + + m_occurrence[(~ll).intern()].nbNotBin > + 0) { + pure.push_back(~ll); + } + } + } + } + + for (unsigned i = 0; i < m_occurrence[(~l).intern()].nbBin; i++) { + int idxCl = m_occurrence[(~l).intern()].bin[i]; + m_infoClauses[idxCl].nbUnsat++; + if (m_infoClauses[idxCl].watcher == ~l) + m_reviewWatcher.push_back(idxCl); } } // we search another non assigned literal if requiered for (auto &idxCl : m_reviewWatcher) { - if (m_infoClauses[idxCl].nbSat) continue; + if (m_infoClauses[idxCl].nbSat) + continue; for (auto &l : m_clauses[idxCl]) { if (m_currentValue[l.var()] == l_Undef) { @@ -89,7 +163,7 @@ void SpecManagerCnfDyn::preUpdate(std::vector &lits) { } } } -} // preUpdate +} // preUpdate /** Update the occurrence list w.r.t. a new set of unassigned variables. @@ -132,6 +206,6 @@ void SpecManagerCnfDyn::postUpdate(std::vector &lits) { m_currentValue[l.var()] = l_Undef; } -} // postUpdate +} // postUpdate -} // namespace d4 +} // namespace d4 diff --git a/src/specs/cnf/SpecManagerCnfDyn.hpp b/src/specs/cnf/SpecManagerCnfDyn.hpp index fedfb901..7398b14f 100644 --- a/src/specs/cnf/SpecManagerCnfDyn.hpp +++ b/src/specs/cnf/SpecManagerCnfDyn.hpp @@ -25,7 +25,7 @@ namespace d4 { class SpecManagerCnfDyn : public SpecManagerCnf { - private: + protected: std::vector m_reviewWatcher; void initClauses(std::vector> &clauses); @@ -33,6 +33,7 @@ class SpecManagerCnfDyn : public SpecManagerCnf { SpecManagerCnfDyn(ProblemManager &p); void preUpdate(std::vector &lits); + void preUpdate(std::vector &lits,std::vector& pure ) override; void postUpdate(std::vector &lits); // we cannot use this function here diff --git a/src/utils/IDIDFunc.hpp b/src/utils/IDIDFunc.hpp new file mode 100644 index 00000000..f4e4d178 --- /dev/null +++ b/src/utils/IDIDFunc.hpp @@ -0,0 +1,35 @@ +#include +#include +struct IDIDFunc { + std::vector data; + int max_val = 0, max_img = 0; + IDIDFunc(int max_val, int max_img) + : data(max_val, 0), max_val(max_val), max_img(max_img) {} + IDIDFunc() {} + const int &operator[](int v) const { + assert(v < max_val); + const int &i = data[v]; + assert(i < max_img); + return i; + } + int &operator[](int v) { + assert(v < max_val); + int &i = data[v]; + assert(i < max_img); + return i; + } + IDIDFunc reverse() { + IDIDFunc out(max_img, max_val); + for (int i = 0; i < max_val; i++) { + out.data[data[i]] = i; + } + return out; + } + template std::vector permute(std::vector values) { + std::vector out(max_img); + for (int i = 0; i < max_val; i++) { + out[i] = values[data[i]]; + } + return out; + } +}; diff --git a/src/utils/Proj.hpp b/src/utils/Proj.hpp new file mode 100644 index 00000000..8a2ad020 --- /dev/null +++ b/src/utils/Proj.hpp @@ -0,0 +1,15 @@ +#pragma once +#include "src/problem/ProblemTypes.hpp" +#include +namespace d4 { +struct ProjVars { + std::vector vars; + int nbProj = 0; + std::span iter_proj() { + return {vars.begin(), vars.begin() + nbProj}; + } + std::span iter_nproj() { + return {vars.begin() + nbProj, vars.end()}; + } +}; +} // namespace d4 diff --git a/src/utils/UnionFind.hpp b/src/utils/UnionFind.hpp new file mode 100644 index 00000000..9a33d0a9 --- /dev/null +++ b/src/utils/UnionFind.hpp @@ -0,0 +1,36 @@ +#pragma once +#include +#include +#include +struct UnionFind { + + int cnt; + std::vector parent; + std::vector size; + UnionFind(int s) :cnt(s), parent(s), size(s) { clear(); } + + int find_set(int v) { + if (v == parent[v]) + return v; + return parent[v] = find_set(parent[v]); + } + + void union_sets(int a, int b) { + a = find_set(a); + b = find_set(b); + if (a != b) { + cnt--; + if (size[a] < size[b]) + std::swap(a, b); + parent[b] = a; + size[a] += size[b]; + } + } + void clear() { + for (int i = 0; i < parent.size(); i++) { + parent[i] = i; + size[i] = 1; + } + cnt = parent.size(); + } +};