diff --git a/CMakeLists.txt b/CMakeLists.txt index 4794008..b9944a5 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -217,6 +217,7 @@ include_directories( # SYSTEM ${PROJECT_BINARY_DIR}/third-party/or-tools SYSTEM third-party/abseil-cpp SYSTEM third-party/bliss + SYSTEM third-party/cadical SYSTEM third-party/Catch SYSTEM third-party/Eigen SYSTEM third-party/FADBAD++ diff --git a/minimum/linear/CMakeLists.txt b/minimum/linear/CMakeLists.txt index 63f0f6c..de764b2 100644 --- a/minimum/linear/CMakeLists.txt +++ b/minimum/linear/CMakeLists.txt @@ -3,6 +3,7 @@ library_with_tests("minimum_linear" "absl_str_format" "absl::flat_hash_map" "absl::flat_hash_set" + "cadical" "cleaneling" "glpk" "glucose" diff --git a/minimum/linear/cadical_solver.cpp b/minimum/linear/cadical_solver.cpp new file mode 100644 index 0000000..45fef76 --- /dev/null +++ b/minimum/linear/cadical_solver.cpp @@ -0,0 +1,83 @@ +#include +#include + +#include + +#include +#include +#include +#include +#include +#include +#include + +using minimum::core::check; + +namespace minimum { +namespace linear { + +class CadicalInternalSatSolver : public SatSolver { + public: + CadicalInternalSatSolver(bool silent_mode); + + virtual Var add_variable() override; + virtual Var add_helper_variable() override; + virtual void add_clause(const std::vector& clause) override; + virtual bool solve(std::vector* solution) override; + virtual bool solve(const std::vector& assumptions, + std::vector* solution) override; + + private: + CaDiCaL::Solver solver; + std::vector literals; +}; + +std::unique_ptr cadical_solver(bool silent_mode) { + return std::make_unique(silent_mode); +} + +CadicalInternalSatSolver::CadicalInternalSatSolver(bool silent_mode) {} + +SatSolver::Var CadicalInternalSatSolver::add_variable() { + literals.push_back(literals.size() + 1); + return literals.back() - 1; +} + +SatSolver::Var CadicalInternalSatSolver::add_helper_variable() { return add_variable(); } + +void CadicalInternalSatSolver::add_clause(const std::vector& clause) { + for (auto& literal : clause) { + if (literal.second) { + solver.add(literal.first + 1); + } else { + solver.add(-literal.first - 1); + } + } + solver.add(0); +} + +bool CadicalInternalSatSolver::solve(std::vector* solution) { + bool result = solver.solve() == 10; + if (result) { + solution->clear(); + for (auto& lit : literals) { + auto value = solver.val(lit); + solution->push_back(value > 0 ? 1 : 0); + } + } + return result; +} + +bool CadicalInternalSatSolver::solve(const std::vector& assumptions, + std::vector* solution) { + for (auto& literal : assumptions) { + if (literal.second) { + solver.assume(literal.first + 1); + } else { + solver.assume(-literal.first - 1); + } + } + return solve(solution); +} +} // namespace linear +} // namespace minimum diff --git a/minimum/linear/sat_solver.h b/minimum/linear/sat_solver.h index 00419cb..9a147f8 100644 --- a/minimum/linear/sat_solver.h +++ b/minimum/linear/sat_solver.h @@ -44,5 +44,6 @@ class SatSolver { std::unique_ptr MINIMUM_LINEAR_API minisat_solver(bool silent_mode = false); std::unique_ptr MINIMUM_LINEAR_API cleaneling_solver(); std::unique_ptr MINIMUM_LINEAR_API glucose_solver(); +std::unique_ptr MINIMUM_LINEAR_API cadical_solver(bool silent_mode = false); } // namespace linear } // namespace minimum diff --git a/minimum/linear/sat_test.cpp b/minimum/linear/sat_test.cpp index cbe4d7f..b230a3a 100644 --- a/minimum/linear/sat_test.cpp +++ b/minimum/linear/sat_test.cpp @@ -181,6 +181,10 @@ TEST_CASE("minisatp") { TEST_CASE("glucose") { simple_test(glucose_solver); } +TEST_CASE("cadical") { + simple_test([]() { return cadical_solver(true); }); +} + TEST_CASE("simple_integer_programming_tests_minisat") { IpToSatSolver solver(bind(minisat_solver, true)); solver.set_silent(true); @@ -301,7 +305,8 @@ TEST_CASE("sat-constraints_coefs_larger_than_1") { ip.add_constraint(4 * x - y - z >= 0); REQUIRE(solve_minisat(&ip)); - REQUIRE_NUM_SOLUTIONS(ip, []() { return minisat_solver(true); }, 5); + REQUIRE_NUM_SOLUTIONS( + ip, []() { return minisat_solver(true); }, 5); } TEST_CASE("sat-constraints_coefs_zero") { @@ -309,7 +314,8 @@ TEST_CASE("sat-constraints_coefs_zero") { auto x = ip.add_boolean(); ip.add_constraint(0 * x >= 0); - REQUIRE_NUM_SOLUTIONS(ip, []() { return minisat_solver(true); }, 2); + REQUIRE_NUM_SOLUTIONS( + ip, []() { return minisat_solver(true); }, 2); } TEST_CASE("sat-constraints_fractional_coeff-1") { @@ -336,7 +342,8 @@ TEST_CASE("sat-constraints_coefs_less_than_minus_1") { auto z = ip.add_boolean(); ip.add_constraint(8 * x - 2 * y - 2 * z >= 0); - REQUIRE_NUM_SOLUTIONS(ip, []() { return minisat_solver(true); }, 5); + REQUIRE_NUM_SOLUTIONS( + ip, []() { return minisat_solver(true); }, 5); } TEST_CASE("sat-constraints_coefs_negative_multiple_times") { @@ -346,7 +353,8 @@ TEST_CASE("sat-constraints_coefs_negative_multiple_times") { auto z = ip.add_boolean(); ip.add_constraint(8 * x - y - y - z - z >= 0); - REQUIRE_NUM_SOLUTIONS(ip, []() { return minisat_solver(true); }, 5); + REQUIRE_NUM_SOLUTIONS( + ip, []() { return minisat_solver(true); }, 5); } TEST_CASE("sat-negative-objective") { @@ -376,7 +384,8 @@ TEST_CASE("sat-objective-next_solution") { ip.add_objective(obj); ip.add_constraint(x + y + z + w + u + v == 2); - REQUIRE_NUM_SOLUTIONS(ip, []() { return minisat_solver(true); }, 6); + REQUIRE_NUM_SOLUTIONS( + ip, []() { return minisat_solver(true); }, 6); } TEST_CASE("add_min_consecutive_constraints-2-true") { @@ -393,7 +402,8 @@ TEST_CASE("add_min_consecutive_constraints-2-true") { // 1 1 0 // 0 1 1 // 1 0 1 - REQUIRE_NUM_SOLUTIONS(ip, []() { return minisat_solver(true); }, 3); + REQUIRE_NUM_SOLUTIONS( + ip, []() { return minisat_solver(true); }, 3); } TEST_CASE("add_min_max_consecutive_constraints-4") { diff --git a/third-party/CMakeLists.txt b/third-party/CMakeLists.txt index d09d6f9..c1c74d9 100644 --- a/third-party/CMakeLists.txt +++ b/third-party/CMakeLists.txt @@ -11,6 +11,7 @@ set(ABSL_STD_CXX_FLAG "" CACHE STRING "c++ std flag" FORCE) add_subdirectory(abseil-cpp) add_subdirectory(bliss) +add_subdirectory(cadical) add_subdirectory(Catch) add_subdirectory(cleaneling) add_subdirectory(coin) diff --git a/third-party/cadical/CMakeLists.txt b/third-party/cadical/CMakeLists.txt new file mode 100644 index 0000000..4fdd3e5 --- /dev/null +++ b/third-party/cadical/CMakeLists.txt @@ -0,0 +1,25 @@ +add_definitions("-DNBUILD") +if (MSVC) + add_definitions("-DNUNLOCKED") +endif () + +add_library(cadical +cadical/analyze.cpp cadical/decompose.cpp cadical/minimize.cpp cadical/signal.cpp +cadical/arena.cpp cadical/deduplicate.cpp cadical/occs.cpp cadical/solution.cpp +cadical/assume.cpp cadical/elim.cpp cadical/options.cpp cadical/solver.cpp +cadical/averages.cpp cadical/ema.cpp cadical/parse.cpp cadical/stats.cpp +cadical/backtrack.cpp cadical/extend.cpp cadical/phases.cpp cadical/subsume.cpp +cadical/backward.cpp cadical/external.cpp cadical/probe.cpp cadical/terminal.cpp +cadical/bins.cpp cadical/file.cpp cadical/profile.cpp cadical/ternary.cpp +cadical/block.cpp cadical/flags.cpp cadical/proof.cpp cadical/tracer.cpp +cadical/ccadical.cpp cadical/format.cpp cadical/propagate.cpp cadical/transred.cpp +cadical/checker.cpp cadical/gates.cpp cadical/queue.cpp cadical/util.cpp +cadical/clause.cpp cadical/instantiate.cpp cadical/random.cpp cadical/var.cpp +cadical/collect.cpp cadical/internal.cpp cadical/reduce.cpp cadical/version.cpp +cadical/compact.cpp cadical/ipasir.cpp cadical/rephase.cpp cadical/vivify.cpp +cadical/condition.cpp cadical/limit.cpp cadical/report.cpp cadical/walk.cpp +cadical/config.cpp cadical/logging.cpp cadical/resources.cpp cadical/watch.cpp +cadical/contract.cpp cadical/lookahead.cpp cadical/restart.cpp +cadical/cover.cpp cadical/lucky.cpp cadical/restore.cpp +cadical/decide.cpp cadical/message.cpp cadical/score.cpp) + diff --git a/third-party/cadical/cadical/README.md b/third-party/cadical/cadical/README.md new file mode 100644 index 0000000..f17395f --- /dev/null +++ b/third-party/cadical/cadical/README.md @@ -0,0 +1,12 @@ +This is the source code of the library `libcadical.a` with header +`cadical.hpp`, the stand-alone solver `cadical` (in `cadical.cpp`) and the +model based tester `mobical` (in `mobical.app`). + +The `configure` script and link to the `makefile` in the root directory +can be used from within the `src` sub-directory too and then will just work +as if used from the root directory. For instance + + ./configure && make test + +will configure and build in `../build` the default (optimizing) +configuration and if successful then run the test suite. diff --git a/third-party/cadical/cadical/analyze.cpp b/third-party/cadical/cadical/analyze.cpp new file mode 100644 index 0000000..ae15680 --- /dev/null +++ b/third-party/cadical/cadical/analyze.cpp @@ -0,0 +1,785 @@ +#include "internal.hpp" + +namespace CaDiCaL { + +/*------------------------------------------------------------------------*/ + +// Code for conflict analysis, i.e., to generate the first UIP clause. The +// main function is 'analyze' below. It further uses 'minimize' to minimize +// the first UIP clause, which is in 'minimize.cpp'. An important side +// effect of conflict analysis is to update the decision queue by bumping +// variables. Similarly analyzed clauses are bumped to mark them as active. + +/*------------------------------------------------------------------------*/ + +void Internal::learn_empty_clause () { + assert (!unsat); + LOG ("learned empty clause"); + external->check_learned_empty_clause (); + if (proof) proof->add_derived_empty_clause (); + unsat = true; +} + +void Internal::learn_unit_clause (int lit) { + LOG ("learned unit clause %d", lit); + external->check_learned_unit_clause (lit); + if (proof) proof->add_derived_unit_clause (lit); + mark_fixed (lit); +} + +/*------------------------------------------------------------------------*/ + +// Move bumped variables to the front of the (VMTF) decision queue. The +// 'bumped' time stamp is updated accordingly. It is used to determine +// whether the 'queue.assigned' pointer has to be moved in 'unassign'. + +void Internal::bump_queue (int lit) { + assert (opts.bump); + const int idx = vidx (lit); + if (!links[idx].next) return; + queue.dequeue (links, idx); + queue.enqueue (links, idx); + assert (stats.bumped != INT64_MAX); + btab[idx] = ++stats.bumped; + LOG ("moved to front variable %d and bumped to %" PRId64 "", idx, btab[idx]); + if (!vals[idx]) update_queue_unassigned (idx); +} + +/*------------------------------------------------------------------------*/ + +// It would be better to use 'isinf' but there are some historical issues +// with this function. On some platforms it is a macro and even for C++ it +// changed the scope (in pre 5.0 gcc) from '::isinf' to 'std::isinf'. I do +// not want to worry about these strange incompatibilities and thus use the +// same trick as in older solvers (since the MiniSAT team invented EVSIDS) +// and simply put a hard limit here. It is less elegant but easy to port. + +static inline bool evsids_limit_hit (double score) { + assert (sizeof (score) == 8); // assume IEEE 754 64-bit double + return score > 1e150; // MAX_DOUBLE is around 1.8e308 +} + +/*------------------------------------------------------------------------*/ + +// Classical exponential VSIDS as pioneered by MiniSAT. + +void Internal::rescale_variable_scores () { + stats.rescored++; + double divider = score_inc; + for (auto idx : vars) { + const double tmp = stab[idx]; + if (tmp > divider) divider = tmp; + } + PHASE ("rescore", stats.rescored, + "rescoring %d variable scores by 1/%g", max_var, divider); + assert (divider > 0); + double factor = 1.0 / divider; + for (auto idx : vars) + stab[idx] *= factor; + score_inc *= factor; + PHASE ("rescore", stats.rescored, + "new score increment %g after %" PRId64 " conflicts", + score_inc, stats.conflicts); +} + +void Internal::bump_variable_score (int lit) { + assert (opts.bump); + int idx = vidx (lit); + double old_score = score (idx); + assert (!evsids_limit_hit (old_score)); + double new_score = old_score + score_inc; + if (evsids_limit_hit (new_score)) { + LOG ("bumping %g score of %d hits EVSIDS score limit", old_score, idx); + rescale_variable_scores (); + old_score = score (idx); + assert (!evsids_limit_hit (old_score)); + new_score = old_score + score_inc; + } + assert (!evsids_limit_hit (new_score)); + LOG ("new %g score of %d", new_score, idx); + score (idx) = new_score; + if (scores.contains (idx)) scores.update (idx); +} + +// Important variables recently used in conflict analysis are 'bumped', + +void Internal::bump_variable (int lit) { + if (use_scores ()) bump_variable_score (lit); + else bump_queue (lit); +} + +// After every conflict the variable score increment is increased by a +// factor (if we are currently using scores). + +void Internal::bump_variable_score_inc () { + assert (use_scores ()); + assert (!evsids_limit_hit (score_inc)); + double f = 1e3/opts.scorefactor; + double new_score_inc = score_inc * f; + if (evsids_limit_hit (new_score_inc)) { + LOG ("bumping %g increment by %g hits EVSIDS score limit", score_inc, f); + rescale_variable_scores (); + new_score_inc = score_inc * f; + } + assert (!evsids_limit_hit (new_score_inc)); + LOG ("bumped score increment from %g to %g with factor %g", + score_inc, new_score_inc, f); + score_inc = new_score_inc; +} + +/*------------------------------------------------------------------------*/ + +struct analyze_bumped_rank { + Internal * internal; + analyze_bumped_rank (Internal * i) : internal (i) { } + uint64_t operator () (const int & a) const { + return internal->bumped (a); + } +}; + +struct analyze_bumped_smaller { + Internal * internal; + analyze_bumped_smaller (Internal * i) : internal (i) { } + bool operator () (const int & a, const int & b) const { + const auto s = analyze_bumped_rank (internal) (a); + const auto t = analyze_bumped_rank (internal) (b); + return s < t; + } +}; + +/*------------------------------------------------------------------------*/ + +void Internal::bump_variables () { + + assert (opts.bump); + + START (bump); + + if (opts.bumpreason) bump_also_all_reason_literals (); + + if (!use_scores ()) { + + // Variables are bumped in the order they are in the current decision + // queue. This maintains relative order between bumped variables in + // the queue and seems to work best. We also experimented with + // focusing on variables of the last decision level, but results were + // mixed. + + MSORT (opts.radixsortlim, + analyzed.begin (), analyzed.end (), + analyze_bumped_rank (this), analyze_bumped_smaller (this)); + } + + for (const auto & lit : analyzed) + bump_variable (lit); + + if (use_scores ()) bump_variable_score_inc (); + + STOP (bump); +} + +/*------------------------------------------------------------------------*/ + +// We use the glue time stamp table 'gtab' for fast glue computation. + +int Internal::recompute_glue (Clause * c) { + int res = 0; + const int64_t stamp = ++stats.recomputed; + for (const auto & lit : *c) { + int level = var (lit).level; + assert (gtab[level] <= stamp); + if (gtab[level] == stamp) continue; + gtab[level] = stamp; + res++; + } + return res; +} + +// Clauses resolved since the last reduction are marked as 'used', their +// glue is recomputed and they are promoted if the glue shrinks. Note that +// promotion from 'tier3' to 'tier2' will set 'used' to '2'. + +inline void Internal::bump_clause (Clause * c) { + LOG (c, "bumping"); + unsigned used = c->used; + c->used = 1; + if (c->keep) return; + if (c->hyper) return; + if (!c->redundant) return; + int new_glue = recompute_glue (c); + if (new_glue < c->glue) promote_clause (c, new_glue); + else if (used && c->glue <= opts.reducetier2glue) c->used = 2; +} + +/*------------------------------------------------------------------------*/ + +// During conflict analysis literals not seen yet either become part of the +// first unique implication point (UIP) clause (if on lower decision level), +// are dropped (if fixed), or are resolved away (if on the current decision +// level and different from the first UIP). At the same time we update the +// number of seen literals on a decision level. This helps conflict clause +// minimization. The number of seen levels is the glucose level (also +// called 'glue', or 'LBD'). + +inline void +Internal::analyze_literal (int lit, int & open) { + assert (lit); + Flags & f = flags (lit); + if (f.seen) return; + Var & v = var (lit); + if (!v.level) return; + assert (val (lit) < 0); + assert (v.level <= level); + if (v.level < level) clause.push_back (lit); + Level & l = control[v.level]; + if (!l.seen.count++) { + LOG ("found new level %d contributing to conflict", v.level); + levels.push_back (v.level); + } + if (v.trail < l.seen.trail) l.seen.trail = v.trail; + f.seen = true; + analyzed.push_back (lit); + LOG ("analyzed literal %d assigned at level %d", lit, v.level); + if (v.level == level) open++; +} + +inline void +Internal::analyze_reason (int lit, Clause * reason, int & open) { + assert (reason); + bump_clause (reason); + for (const auto & other : *reason) + if (other != lit) + analyze_literal (other, open); +} + +/*------------------------------------------------------------------------*/ + +// This is an idea which was implicit in MapleCOMSPS 2016 for 'limit = 1'. +// See also the paragraph on 'bumping reason side literals' in their SAT'16 +// paper [LiangGaneshPoupartCzarnecki-SAT'16]. Reason side bumping was +// performed exactly when 'LRB' based decision heuristics was used, which in +// the original version was enabled after 10000 conflicts until a time limit +// of 2500 seconds was reached (half of the competition time limit). The +// Maple / Glucose / MiniSAT evolution winning the SAT race in 2019 made +// the schedule of reason side bumping deterministic, i.e., avoiding a time +// limit, by switching between 'LRB' and 'VSIDS' in an interval of initially +// 30 million propagations, which then is increased geometrically by 10%. + +inline bool Internal::bump_also_reason_literal (int lit) { + assert (lit); + assert (val (lit) < 0); + Flags & f = flags (lit); + if (f.seen) return false; + const Var & v = var (lit); + if (!v.level) return false; + f.seen = true; + analyzed.push_back (lit); + LOG ("bumping also reason literal %d assigned at level %d", lit, v.level); + return true; +} + +// We experimented with deeper reason bumping without much success though. + +inline void Internal::bump_also_reason_literals (int lit, int limit) { + assert (lit); + assert (limit > 0); + const Var & v = var (lit); + assert (val (lit)); + if (!v.level) return; + Clause * reason = v.reason; + if (!reason) return; + for (const auto & other : *reason) { + if (other == lit) continue; + if (!bump_also_reason_literal (other)) continue; + if (limit < 2) continue; + bump_also_reason_literals (-other, limit-1); + } +} + +inline void Internal::bump_also_all_reason_literals () { + assert (opts.bumpreason); + assert (opts.bumpreasondepth > 0); + LOG ("bumping reasons up to depth %d", opts.bumpreasondepth); + for (const auto & lit : clause) + bump_also_reason_literals (-lit, opts.bumpreasondepth); +} + +/*------------------------------------------------------------------------*/ + +void Internal::clear_analyzed_literals () { + LOG ("clearing %zd analyzed literals", analyzed.size ()); + for (const auto & lit : analyzed) { + Flags & f = flags (lit); + assert (f.seen); + f.seen = false; + assert (!f.keep); + assert (!f.poison); + assert (!f.removable); + } + analyzed.clear (); +} + +void Internal::clear_analyzed_levels () { + LOG ("clearing %zd analyzed levels", levels.size ()); + for (const auto & l : levels) + if (l < (int) control.size ()) + control[l].reset (); + levels.clear (); +} + +/*------------------------------------------------------------------------*/ + +// Smaller level and trail. Comparing literals on their level is necessary +// for chronological backtracking, since trail order might in this case not +// respect level order. + +struct analyze_trail_negative_rank { + Internal * internal; + analyze_trail_negative_rank (Internal * s) : internal (s) { } + uint64_t operator () (int a) { + Var & v = internal->var (a); + uint64_t res = v.level; + res <<= 32; + res |= v.trail; + return ~res; + } +}; + +struct analyze_trail_larger { + Internal * internal; + analyze_trail_larger (Internal * s) : internal (s) { } + bool operator () (const int & a, const int & b) const { + return + analyze_trail_negative_rank (internal) (a) < + analyze_trail_negative_rank (internal) (b); + } +}; + +/*------------------------------------------------------------------------*/ + +// Generate new driving clause and compute jump level. + +Clause * Internal::new_driving_clause (const int glue, int & jump) { + + const size_t size = clause.size (); + Clause * res; + + if (!size) { + + jump = 0; + res = 0; + + } else if (size == 1) { + + iterating = true; + jump = 0; + res = 0; + + } else { + + assert (clause.size () > 1); + + // We have to get the last assigned literals into the watch position. + // Sorting all literals with respect to reverse assignment order is + // overkill but seems to get slightly faster run-time. For 'minimize' + // we sort the literals too heuristically along the trail order (so in + // the opposite order) with the hope to hit the recursion limit less + // frequently. Thus sorting effort is doubled here. + // + MSORT (opts.radixsortlim, + clause.begin (), clause.end (), + analyze_trail_negative_rank (this), analyze_trail_larger (this)); + + jump = var (clause[1]).level; + res = new_learned_redundant_clause (glue); + res->used = 1 + (glue <= opts.reducetier2glue); + } + + LOG ("jump level %d", jump); + + return res; +} + +/*------------------------------------------------------------------------*/ + +// If chronological backtracking is enabled we need to find the actual +// conflict level and then potentially can also reuse the conflict clause +// as driving clause instead of deriving a redundant new driving clause +// (forcing 'forced') if the number 'count' of literals in conflict assigned +// at the conflict level is exactly one. + +inline int Internal::find_conflict_level (int & forced) { + + assert (conflict); + assert (opts.chrono); + + int res = 0, count = 0; + + forced = 0; + + for (const auto & lit : *conflict) { + const int tmp = var (lit).level; + if (tmp > res) { + res = tmp; + forced = lit; + count = 1; + } else if (tmp == res) { + count++; + if (res == level && count > 1) + break; + } + } + + LOG ("%d literals on actual conflict level %d", count, res); + + const int size = conflict->size; + int * lits = conflict->literals; + + // Move the two highest level literals to the front. + // + for (int i = 0; i < 2; i++) { + + const int lit = lits[i]; + + int highest_position = i; + int highest_literal = lit; + int highest_level = var (highest_literal).level; + + for (int j = i + 1; j < size; j++) { + const int other = lits[j]; + const int tmp = var (other).level; + if (highest_level >= tmp) continue; + highest_literal = other; + highest_position = j; + highest_level = tmp; + if (highest_level == res) break; +#if 0 + if (i && highest_level == res - 1) break; +#endif + } + + // No unwatched higher assignment level literal. + // + if (highest_position == i) continue; + + if (highest_position > 1) + { + LOG (conflict, "unwatch %d in", lit); + remove_watch (watches (lit), conflict); + } + + lits[highest_position] = lit; + lits[i] = highest_literal; + + if (highest_position > 1) + watch_literal (highest_literal, lits[!i], conflict); + } + + // Only if the number of highest level literals in the conflict is one + // then we can reuse the conflict clause as driving clause for 'forced'. + // + if (count != 1) forced = 0; + + return res; +} + +/*------------------------------------------------------------------------*/ + +inline int Internal::determine_actual_backtrack_level (int jump) { + + int res; + + assert (level > jump); + + if (!opts.chrono) { + res = jump; + LOG ("chronological backtracking disabled using jump level %d", res); + } else if (opts.chronoalways) { + stats.chrono++; + res = level - 1; + LOG ("forced chronological backtracking to level %d", res); + } else if (jump >= level - 1) { + res = jump; + LOG ("jump level identical to chronological backtrack level %d", res); + } else if ((size_t) jump < assumptions.size ()) { + res = jump; + LOG ("using jump level %d since it is lower than assumption level %zd", + res, assumptions.size ()); + } else if (level - jump > opts.chronolevelim) { + stats.chrono++; + res = level - 1; + LOG ("back-jumping over %d > %d levels prohibited" + "thus backtracking chronologically to level %d", + level - jump, opts.chronolevelim, res); + } else if (opts.chronoreusetrail) { + + int best_idx = 0, best_pos = 0; + + if (use_scores ()) { + for (size_t i = control[jump + 1].trail; i < trail.size (); i++) { + const int idx = abs (trail[i]); + if (best_idx && !score_smaller (this) (best_idx, idx)) continue; + best_idx = idx; + best_pos = i; + } + LOG ("best variable score %g", score (best_idx)); + } else { + for (size_t i = control[jump + 1].trail; i < trail.size (); i++) { + const int idx = abs (trail[i]); + if (best_idx && bumped (best_idx) >= bumped (idx)) continue; + best_idx = idx; + best_pos = i; + } + LOG ("best variable bumped %" PRId64 "", bumped (best_idx)); + } + assert (best_idx); + LOG ("best variable %d at trail position %d", best_idx, best_pos); + + // Now find the frame and decision level in the control stack of that + // best variable index. Note that, as in 'reuse_trail', the frame + // 'control[i]' for decision level 'i' contains the trail before that + // decision level, i.e., the decision 'control[i].decision' sits at + // 'control[i].trail' in the trail and we thus have to check the level + // of the control frame one higher than at the result level. + // + res = jump; + while (res < level-1 && control[res+1].trail <= best_pos) + res++; + + if (res == jump) + LOG ("default non-chronological back-jumping to level %d", res); + else { + stats.chrono++; + LOG ("chronological backtracking to level %d to reuse trail", res); + } + + } else { + res = jump; + LOG ("non-chronological back-jumping to level %d", res); + } + + return res; +} + +/*------------------------------------------------------------------------*/ + +void Internal::eagerly_subsume_recently_learned_clauses (Clause * c) { + assert (opts.eagersubsume); + LOG (c, "trying eager subsumption with"); + mark (c); + int64_t lim = stats.eagertried + opts.eagersubsumelim; + const auto begin = clauses.begin (); + auto it = clauses.end (); +#ifdef LOGGING + int64_t before = stats.eagersub; +#endif + while (it != begin && stats.eagertried++ <= lim) { + Clause * d = *--it; + if (c == d) continue; + if (d->garbage) continue; + if (!d->redundant) continue; + int needed = c->size; + for (auto & lit : *d) { + if (marked (lit) <= 0) continue; + if (!--needed) break; + } + if (needed) continue; + LOG (d, "eager subsumed"); + stats.eagersub++; + stats.subsumed++; + mark_garbage (d); + } + unmark (c); +#ifdef LOGGING + uint64_t subsumed = stats.eagersub - before; + if (subsumed) LOG ("eagerly subsumed %d clauses", subsumed); +#endif +} + +/*------------------------------------------------------------------------*/ + +// This is the main conflict analysis routine. It assumes that a conflict +// was found. Then we derive the 1st UIP clause, optionally minimize it, +// add it as learned clause, and then uses the clause for conflict directed +// back-jumping and flipping the 1st UIP literal. In combination with +// chronological backtracking (see discussion above) the algorithm becomes +// slightly more involved. + +void Internal::analyze () { + + START (analyze); + + assert (conflict); + + // First update moving averages of trail height at conflict. + // + UPDATE_AVERAGE (averages.current.trail.fast, trail.size ()); + UPDATE_AVERAGE (averages.current.trail.slow, trail.size ()); + + /*----------------------------------------------------------------------*/ + + if (opts.chrono) { + + int forced; + + const int conflict_level = find_conflict_level (forced); + + // In principle we can perform conflict analysis as in non-chronological + // backtracking except if there is only one literal with the maximum + // assignment level in the clause. Then standard conflict analysis is + // unnecessary and we can use the conflict as a driving clause. In the + // pseudo code of the SAT'18 paper on chronological backtracking this + // corresponds to the situation handled in line 4-6 in Alg. 1, except + // that the pseudo code in the paper only backtracks while we eagerly + // assign the single literal on the highest decision level. + + if (forced) { + + assert (forced); + assert (conflict_level > 0); + LOG ("single highest level literal %d", forced); + + // The pseudo code in the SAT'18 paper actually backtracks to the + // 'second highest decision' level, while their code backtracks + // to 'conflict_level-1', which is more in the spirit of chronological + // backtracking anyhow and thus we also do the latter. + // + backtrack (conflict_level - 1); + + LOG ("forcing %d", forced); + search_assign_driving (forced, conflict); + + conflict = 0; + STOP (analyze); + return; + } + + // Backtracking to the conflict level is in the pseudo code in the + // SAT'18 chronological backtracking paper, but not in their actual + // implementation. In principle we do not need to backtrack here. + // However, as a side effect of backtracking to the conflict level we + // set 'level' to the conflict level which then allows us to reuse the + // old 'analyze' code as is. The alternative (which we also tried but + // then abandoned) is to use 'conflict_level' instead of 'level' in the + // analysis, which however requires to pass it to the 'analyze_reason' + // and 'analyze_literal' functions. + // + backtrack (conflict_level); + } + + // Actual conflict on root level, thus formula unsatisfiable. + // + if (!level) { + learn_empty_clause (); + if (external->learner) external->export_learned_empty_clause (); + STOP (analyze); + return; + } + + /*----------------------------------------------------------------------*/ + + // First derive the 1st UIP clause by going over literals assigned on the + // current decision level. Literals in the conflict are marked as 'seen' + // as well as all literals in reason clauses of already 'seen' literals on + // the current decision level. Thus the outer loop starts with the + // conflict clause as 'reason' and then uses the 'reason' of the next + // seen literal on the trail assigned on the current decision level. + // During this process maintain the number 'open' of seen literals on the + // current decision level with not yet processed 'reason'. As soon 'open' + // drops to one, we have found the first unique implication point. This + // is sound because the topological order in which literals are processed + // follows the assignment order and a more complex algorithm to find + // articulation points is not necessary. + // + Clause * reason = conflict; + LOG (reason, "analyzing conflict"); + + assert (clause.empty ()); + + int i = trail.size (); // Start at end-of-trail. + int open = 0; // Seen but not processed on this level. + int uip = 0; // The first UIP literal. + + for (;;) { + analyze_reason (uip, reason, open); + uip = 0; + while (!uip) { + assert (i > 0); + const int lit = trail[--i]; + if (!flags (lit).seen) continue; + if (var (lit).level == level) uip = lit; + } + if (!--open) break; + reason = var (uip).reason; + LOG (reason, "analyzing %d reason", uip); + } + LOG ("first UIP %d", uip); + clause.push_back (-uip); + + // Update glue and learned (1st UIP literals) statistics. + // + int size = (int) clause.size (); + const int glue = (int) levels.size () - 1; + LOG (clause, "1st UIP size %d and glue %d clause", size, glue); + UPDATE_AVERAGE (averages.current.glue.fast, glue); + UPDATE_AVERAGE (averages.current.glue.slow, glue); + stats.learned.literals += size; + stats.learned.clauses++; + assert (glue < size); + + // Update decision heuristics. + // + if (opts.bump) bump_variables (); + + // Minimize the 1st UIP clause as pioneered by Niklas Soerensson in + // MiniSAT and described in our joint SAT'09 paper. + // + if (size > 1) { + if (opts.minimize) minimize_clause (); + size = (int) clause.size (); + if (external->learner) external->export_learned_large_clause (clause); + } else if (external->learner) external->export_learned_unit_clause (-uip); + + // Update actual size statistics. + // + stats.units += (size == 1); + stats.binaries += (size == 2); + UPDATE_AVERAGE (averages.current.size, size); + + // Determine back-jump level, learn driving clause, backtrack and assign + // flipped 1st UIP literal. + // + int jump; + Clause * driving_clause = new_driving_clause (glue, jump); + UPDATE_AVERAGE (averages.current.jump, jump); + + int new_level = determine_actual_backtrack_level (jump);; + UPDATE_AVERAGE (averages.current.level, new_level); + backtrack (new_level); + + if (uip) search_assign_driving (-uip, driving_clause); + else learn_empty_clause (); + + if (stable) reluctant.tick (); // Reluctant has its own 'conflict' counter. + + // Clean up. + // + clear_analyzed_literals (); + clear_analyzed_levels (); + clause.clear (); + conflict = 0; + + STOP (analyze); + + if (driving_clause && opts.eagersubsume) + eagerly_subsume_recently_learned_clauses (driving_clause); +} + +// We wait reporting a learned unit until propagation of that unit is +// completed. Otherwise the 'i' report gives the number of remaining +// variables before propagating the unit (and hides the actual remaining +// variables after propagating it). + +void Internal::iterate () { iterating = false; report ('i'); } + +} diff --git a/third-party/cadical/cadical/arena.cpp b/third-party/cadical/cadical/arena.cpp new file mode 100644 index 0000000..61123ec --- /dev/null +++ b/third-party/cadical/cadical/arena.cpp @@ -0,0 +1,30 @@ +#include "internal.hpp" + +namespace CaDiCaL { + +Arena::Arena (Internal * i) { + memset (this, 0, sizeof *this); + internal = i; +} + +Arena::~Arena () { + delete [] from.start; + delete [] to.start; +} + +void Arena::prepare (size_t bytes) { + LOG ("preparing 'to' space of arena with %zd bytes", bytes); + assert (!to.start); + to.top = to.start = new char[bytes]; + to.end = to.start + bytes; +} + +void Arena::swap () { + delete [] from.start; + LOG ("delete 'from' space of arena with %zd bytes", + (size_t) (from.end - from.start)); + from = to; + to.start = to.top = to.end = 0; +} + +} diff --git a/third-party/cadical/cadical/arena.hpp b/third-party/cadical/cadical/arena.hpp new file mode 100644 index 0000000..1a41ade --- /dev/null +++ b/third-party/cadical/cadical/arena.hpp @@ -0,0 +1,103 @@ +#ifndef _arena_hpp_INCLUDED +#define _arena_hpp_INCLUDED + +namespace CaDiCaL { + +// This memory allocation arena provides fixed size pre-allocated memory for +// the moving garbage collector 'copy_non_garbage_clauses' in 'collect.cpp' +// to hold clauses which should survive garbage collection. + +// The advantage of using a pre-allocated arena is that the allocation order +// of the clauses can be adapted in such a way that clauses watched by the +// same literal are allocated consecutively. This improves locality during +// propagation and thus is more cache friendly. A similar technique is +// implemented in MiniSAT and Glucose and gives substantial speed-up in +// propagations per second even though it might even almost double peek +// memory usage. Note that in MiniSAT this arena is actually required for +// MiniSAT to be able to use 32 bit clauses references instead of 64 bit +// pointers. This would restrict the maximum number of clauses and thus is +// a restriction we do not want to use anymore. + +// New learned clauses are allocated in CaDiCaL outside of this arena and +// moved to the arena during garbage collection. The additional 'to' space +// required for such a moving garbage collector is only allocated for those +// clauses surviving garbage collection, which usually needs much less +// memory than all clauses. The net effect is that in our implementation +// the moving garbage collector using this arena only needs roughly 50% more +// memory than allocating the clauses directly. Both implementations can be +// compared by varying the 'opts.arenatype' option (which also controls the +// allocation order of clauses during moving them). + +// The standard sequence of using the arena is as follows: +// +// Arena arena; +// ... +// arena.prepare (bytes); +// q1 = arena.copy (p1, bytes1); +// ... +// qn = arena.copy (pn, bytesn); +// assert (bytes1 + ... + bytesn <= bytes); +// arena.swap (); +// ... +// if (!arena.contains (q)) delete q; +// ... +// arena.prepare (bytes); +// q1 = arena.copy (p1, bytes1); +// ... +// qn = arena.copy (pn, bytesn); +// assert (bytes1 + ... + bytesn <= bytes); +// arena.swap (); +// ... +// +// One has to be really careful with 'qi' references to arena memory. + +struct Internal; + +class Arena { + + Internal * internal; + + struct { char * start, * top, * end; } from, to; + +public: + + Arena (Internal *); + ~Arena (); + + // Prepare 'to' space to hold that amount of memory. Precondition is that + // the 'to' space is empty. The following sequence of 'copy' operations + // can use as much memory in sum as pre-allocated here. + // + void prepare (size_t bytes); + + // Does the memory pointed to by 'p' belong to this arena? More precisely + // to the 'from' space, since that is the only one remaining after 'swap'. + // + bool contains (void * p) const { + char * c = (char *) p; + return from.start <= c && c < from.top; + } + + // Allocate that amount of memory in 'to' space. This assumes the 'to' + // space has been prepared to hold enough memory with 'prepare'. Then + // copy the memory pointed to by 'p' of size 'bytes'. Note that it does + // not matter whether 'p' is in 'from' or allocated outside of the arena. + // + char * copy (const char * p, size_t bytes) { + char * res = to.top; + to.top += bytes; + assert (to.top <= to.end); + memcpy (res, p, bytes); + return res; + } + + // Completely delete 'from' space and then replace 'from' by 'to' (by + // pointer swapping). Everything previously allocated (in 'from') and not + // explicitly copied to 'to' with 'copy' becomes invalid. + // + void swap (); +}; + +} + +#endif diff --git a/third-party/cadical/cadical/assume.cpp b/third-party/cadical/cadical/assume.cpp new file mode 100644 index 0000000..15079cb --- /dev/null +++ b/third-party/cadical/cadical/assume.cpp @@ -0,0 +1,172 @@ +#include "internal.hpp" + +namespace CaDiCaL { + +// Failed literal handling as pioneered by MiniSAT. This first function +// adds an assumption literal onto the assumption stack. + +void Internal::assume (int lit) { + Flags & f = flags (lit); + const unsigned char bit = bign (lit); + if (f.assumed & bit) { + LOG ("ignoring already assumed %d", lit); + return; + } + LOG ("assume %d", lit); + f.assumed |= bit; + assumptions.push_back (lit); + freeze (lit); +} + +// Find all failing assumptions starting from the one on the assumption +// stack with the lowest decision level. This goes back to MiniSAT and is +// called 'analyze_final' there. We always return '20' to simplify the code +// in the main search loop in 'Internal::search', which also terminates it. + +void Internal::failing () { + + START (analyze); + + LOG ("analyzing failing assumptions"); + + assert (analyzed.empty ()); + assert (clause.empty ()); + + int first = 0; + + // Try to find two clashing assumptions. + // + for (auto & lit : assumptions) { + if (!assumed (-lit)) continue; + first = lit; + break; + } + + if (first) { + + clause.push_back (first); + clause.push_back (-first); + + Flags & f = flags (first); + + unsigned bit = bign (first); + assert (!(f.failed & bit)); + f.failed |= bit; + bit = bign (-first); + f.failed |= bit; + + } else { + + // Find an assumption falsified at smallest decision level. + // + for (auto & lit : assumptions) { + const signed char tmp = val (lit); + if (tmp >= 0) continue; + if (!first || var (first).level > var (lit).level) + first = lit; + } + assert (first); + LOG ("starting with assumption %d falsified on decision level %d", + first, var (first).level); + + if (!var (first).level) { + + LOG ("failed assumption %d", first); + clause.push_back (-first); + + Flags & f = flags (first); + const unsigned bit = bign (first); + assert (!(f.failed & bit)); + f.failed |= bit; + + } else { + + // The 'analyzed' stack serves as working stack for a BFS through the + // implication graph until decisions, which are all assumptions, or units + // are reached. This is simpler than corresponding code in 'analyze'. + + { + LOG ("failed assumption %d", first); + Flags & f = flags (first); + const unsigned bit = bign (first); + assert (!(f.failed & bit)); + f.failed |= bit; + f.seen = true; + } + + analyzed.push_back (first); + clause.push_back (-first); + + size_t next = 0; + + while (next < analyzed.size ()) { + const int lit = analyzed[next++]; +#ifndef NDEBUG + if (first == lit) assert (val (lit) < 0); + else assert (val (lit) > 0); +#endif + Var & v = var (lit); + if (!v.level) continue; + + if (v.reason) { + assert (v.level); + LOG (v.reason, "analyze reason"); + for (const auto & other : *v.reason) { + Flags & f = flags (other); + if (f.seen) continue; + f.seen = true; + assert (val (other) < 0); + analyzed.push_back (-other); + } + } else { + assert (assumed (lit)); + LOG ("failed assumption %d", lit); + clause.push_back (-lit); + Flags & f = flags (lit); + const unsigned bit = bign (lit); + assert (!(f.failed & bit)); + f.failed |= bit; + } + } + clear_analyzed_literals (); + + // TODO, we can not do clause minimization here, right? + } + } + + VERBOSE (1, "found %zd failed assumptions %.0f%%", + clause.size (), percent (clause.size (), assumptions.size ())); + + // We do not actually need to learn this clause, since the conflict is + // forced already by some other clauses. There is also no bumping + // of variables nor clauses necessary. But we still want to check + // correctness of the claim that the determined subset of failing + // assumptions are a high-level core or equivalently their negations form + // a unit-implied clause. + // + external->check_learned_clause (); + if (proof) { + proof->add_derived_clause (clause); + proof->delete_clause (clause); + } + clause.clear (); + + STOP (analyze); +} + +// Add the start of each incremental phase (leaving the state +// 'UNSATISFIABLE' actually) we reset all assumptions. + +void Internal::reset_assumptions () { + for (const auto & lit : assumptions) { + Flags & f = flags (lit); + const unsigned char bit = bign (lit); + f.assumed &= ~bit; + f.failed &= ~bit; + melt (lit); + } + LOG ("cleared %zd assumptions", assumptions.size ()); + assumptions.clear (); +} + +} diff --git a/third-party/cadical/cadical/averages.cpp b/third-party/cadical/cadical/averages.cpp new file mode 100644 index 0000000..9376e6e --- /dev/null +++ b/third-party/cadical/cadical/averages.cpp @@ -0,0 +1,30 @@ +#include "internal.hpp" + +namespace CaDiCaL { + +void Internal::init_averages () { + + LOG ("initializing averages"); + + INIT_EMA (averages.current.jump, opts.emajump); + INIT_EMA (averages.current.level, opts.emalevel); + INIT_EMA (averages.current.size, opts.emasize); + + INIT_EMA (averages.current.glue.fast, opts.emagluefast); + INIT_EMA (averages.current.glue.slow, opts.emaglueslow); + + INIT_EMA (averages.current.trail.fast, opts.ematrailfast); + INIT_EMA (averages.current.trail.slow, opts.ematrailslow); + + assert (!averages.swapped); +} + +void Internal::swap_averages () { + LOG ("saving current averages"); + swap (averages.current, averages.saved); + if (!averages.swapped) init_averages (); + else LOG ("swapping in previously saved averages"); + averages.swapped++; +} + +} diff --git a/third-party/cadical/cadical/averages.hpp b/third-party/cadical/cadical/averages.hpp new file mode 100644 index 0000000..1d4451c --- /dev/null +++ b/third-party/cadical/cadical/averages.hpp @@ -0,0 +1,36 @@ +#ifndef _averages_hpp_INCLUDED +#define _averages_hpp_INCLUDED + +#include "ema.hpp" // alphabetically after 'averages.hpp' + +namespace CaDiCaL { + +struct Averages { + + int64_t swapped; + + struct { + + struct { + EMA fast; // average fast (small window) moving glucose level + EMA slow; // average slow (large window) moving glucose level + } glue; + + struct { + EMA fast; // average fast (small window) moving trail level + EMA slow; // average slow (large window) moving trail level + } trail; + + EMA size; // average learned clause size + EMA jump; // average (potential non-chronological) back-jump level + EMA level; // average back track level after conflict + + } current, saved; + + Averages () : swapped (0) { } + +}; + +} + +#endif diff --git a/third-party/cadical/cadical/backtrack.cpp b/third-party/cadical/cadical/backtrack.cpp new file mode 100644 index 0000000..f95e946 --- /dev/null +++ b/third-party/cadical/cadical/backtrack.cpp @@ -0,0 +1,125 @@ +#include "internal.hpp" + +namespace CaDiCaL { + +// The global assignment stack can only be (partially) reset through +// 'backtrack' which is the only function using 'unassign' (inlined and thus +// local to this file). It turns out that 'unassign' does not need a +// specialization for 'probe' nor 'vivify' and thus it is shared. + +inline void Internal::unassign (int lit) { + assert (val (lit) > 0); + const int idx = vidx (lit); + vals[idx] = 0; + vals[-idx] = 0; + LOG ("unassign %d @ %d", lit, var (idx).level); + + // In the standard EVSIDS variable decision heuristic of MiniSAT, we need + // to push variables which become unassigned back to the heap. + // + if (!scores.contains (idx)) scores.push_back (idx); + + // For VMTF we need to update the 'queue.unassigned' pointer in case this + // variable sits after the variable to which 'queue.unassigned' currently + // points. See our SAT'15 paper for more details on this aspect. + // + if (queue.bumped < btab[idx]) update_queue_unassigned (idx); +} + +/*------------------------------------------------------------------------*/ + +// Update the current target maximum assignment and also the very best +// assignment. Whether a trail produces a conflict is determined during +// propagation. Thus that all functions in the 'search' loop after +// propagation can assume that 'no_conflict_until' is valid. If a conflict +// is found then the trail before the last decision is used (see the end of +// 'propagate'). During backtracking we can then save this largest +// propagation conflict free assignment. It is saved as both 'target' +// assignment for picking decisions in 'stable' mode and if it is the +// largest ever such assignment also as 'best' assignment. This 'best' +// assignment can then be used in future stable decisions after the next +// 'rephase_best' overwrites saved phases with it. + +void Internal::update_target_and_best () { + + bool reset = (rephased && stats.conflicts > last.rephase.conflicts); + + if (reset) { + target_assigned = 0; + if (rephased == 'B') best_assigned = 0; // update it again + } + + if (no_conflict_until > target_assigned) { + copy_phases (phases.target); + target_assigned = no_conflict_until; + LOG ("new target trail level %d", target_assigned); + } + + if (no_conflict_until > best_assigned) { + copy_phases (phases.best); + best_assigned = no_conflict_until; + LOG ("new best trail level %d", best_assigned); + } + + if (reset) { + report (rephased); + rephased = 0; + } +} + +/*------------------------------------------------------------------------*/ + +void Internal::backtrack (int new_level) { + + assert (new_level <= level); + if (new_level == level) return; + + stats.backtracks++; + update_target_and_best (); + + const size_t assigned = control[new_level+1].trail; + + LOG ("backtracking to decision level %d with decision %d and trail %zd", + new_level, control[new_level].decision, assigned); + + const size_t end_of_trail = trail.size (); + size_t i = assigned, j = i; + + int reassigned = 0, unassigned = 0; + + while (i < end_of_trail) { + int lit = trail[i++]; + Var & v = var (lit); + if (v.level > new_level) { + unassign (lit); + unassigned++; + } else { + // This is the essence of the SAT'18 paper on chronological + // backtracking. It is possible to just keep out-of-order assigned + // literals on the trail without breaking the solver (after some + // modifications to 'analyze' - see 'opts.chrono' guarded code there). + assert (opts.chrono); +#ifdef LOGGING + if (!v.level) LOG ("reassign %d @ 0 unit clause %d", lit, lit); + else LOG (v.reason, "reassign %d @ %d", lit, v.level); +#endif + trail[j] = lit; + v.trail = j++; + reassigned++; + } + } + trail.resize (j); + LOG ("unassigned %d literals %.0f%%", + unassigned, percent (unassigned, unassigned + reassigned)); + LOG ("reassigned %d literals %.0f%%", + reassigned, percent (reassigned, unassigned + reassigned)); + + if (propagated > assigned) propagated = assigned; + if (propagated2 > assigned) propagated2 = assigned; + if (no_conflict_until > assigned) no_conflict_until = assigned; + + control.resize (new_level + 1); + level = new_level; +} + +} diff --git a/third-party/cadical/cadical/backward.cpp b/third-party/cadical/cadical/backward.cpp new file mode 100644 index 0000000..851de45 --- /dev/null +++ b/third-party/cadical/cadical/backward.cpp @@ -0,0 +1,148 @@ +#include "internal.hpp" + +namespace CaDiCaL { + +/*------------------------------------------------------------------------*/ + +// Provide eager backward subsumption for resolved clauses. + +// The eliminator maintains a queue of clauses that are new and have to be +// checked to subsume or strengthen other (longer or same size) clauses. + +void Eliminator::enqueue (Clause * c) { + if (!internal->opts.elimbackward) return; + if (c->enqueued) return; + LOG (c, "backward enqueue"); + backward.push (c); + c->enqueued = true; +} + +Clause * Eliminator::dequeue () { + if (backward.empty ()) return 0; + Clause * res = backward.front (); + backward.pop (); + assert (res->enqueued); + res->enqueued = false; + LOG (res, "backward dequeue"); + return res; +} + +Eliminator::~Eliminator () { + while (dequeue ()) + ; +} + +/*------------------------------------------------------------------------*/ + +void Internal::elim_backward_clause (Eliminator & eliminator, Clause *c) { + assert (opts.elimbackward); + assert (!c->redundant); + if (c->garbage) return; + LOG (c, "attempting backward subsumption and strengthening with"); + size_t len = UINT_MAX; + unsigned size = 0; + int best = 0; + bool satisfied = false; + for (const auto & lit : *c) { + const signed char tmp = val (lit); + if (tmp > 0) { satisfied = true; break; } + if (tmp < 0) continue; + size_t l = occs (lit).size (); + LOG ("literal %d occurs %zd times", lit, l); + if (l < len) best = lit, len = l; + mark (lit); + size++; + } + if (satisfied) { + LOG ("clause actually already satisfied"); + elim_update_removed_clause (eliminator, c); + mark_garbage (c); + } else if (len > (size_t) opts.elimocclim) { + LOG ("skipping backward subsumption due to too many occurrences"); + } else { + assert (len); + LOG ("literal %d has smallest number of occurrences %zd", best, len); + LOG ("marked %d literals in clause of size %d", size, c->size); + for (auto & d : occs (best)) { + if (d == c) continue; + if (d->garbage) continue; + if ((unsigned) d->size < size) continue; + int negated = 0; + unsigned found = 0; + for (const auto & lit : *d) { + signed char tmp = val (lit); + if (tmp > 0) { satisfied = true; break; } + if (tmp < 0) continue; + tmp = marked (lit); + if (!tmp) continue; + if (tmp < 0) { + if (negated) { size = UINT_MAX; break; } + else negated = lit; + } + if (++found == size) break; + } + if (satisfied) { + LOG (d, "found satisfied clause"); + elim_update_removed_clause (eliminator, d); + mark_garbage (d); + } else if (found == size) { + if (!negated) { + LOG (d, "found subsumed clause"); + elim_update_removed_clause (eliminator, d); + mark_garbage (d); + stats.subsumed++; + stats.elimbwsub++; + } else { + int unit = 0; + for (const auto & lit : * d) { + const signed char tmp = val (lit); + if (tmp < 0) continue; + if (tmp > 0) { satisfied = true; break; } + if (lit == negated) continue; + if (unit) { unit = INT_MIN; break; } + else unit = lit; + } + assert (unit); + if (satisfied) { + mark_garbage (d); + elim_update_removed_clause (eliminator, d); + } else if (unit && unit != INT_MIN) { + assert (unit); + LOG (d, "unit %d through hyper unary resolution with", unit); + assign_unit (unit); + elim_propagate (eliminator, unit); + break; + } else if (occs (negated).size () <= (size_t) opts.elimocclim) { + strengthen_clause (d, negated); + remove_occs (occs (negated), d); + elim_update_removed_lit (eliminator, negated); + stats.elimbwstr++; + assert (negated != best); + eliminator.enqueue (d); + } + } + } + } + } + unmark (c); +} + +/*------------------------------------------------------------------------*/ + +void Internal::elim_backward_clauses (Eliminator & eliminator) { + if (!opts.elimbackward) { + assert (eliminator.backward.empty ()); + return; + } + START (backward); + LOG ("attempting backward subsumption and strengthening with %zd clauses", + eliminator.backward.size ()); + Clause * c; + while (!unsat && (c = eliminator.dequeue ())) + elim_backward_clause (eliminator, c); + STOP (backward); +} + +/*------------------------------------------------------------------------*/ + +} diff --git a/third-party/cadical/cadical/bins.cpp b/third-party/cadical/cadical/bins.cpp new file mode 100644 index 0000000..8f108a3 --- /dev/null +++ b/third-party/cadical/cadical/bins.cpp @@ -0,0 +1,22 @@ +#include "internal.hpp" + +namespace CaDiCaL { + +/*------------------------------------------------------------------------*/ + +// Binary implication graph lists. + +void Internal::init_bins () { + assert (big.empty ()); + while (big.size () < 2*vsize) + big.push_back (Bins ()); + LOG ("initialized binary implication graph"); +} + +void Internal::reset_bins () { + assert (!big.empty ()); + erase_vector (big); + LOG ("reset binary implication graph"); +} + +} diff --git a/third-party/cadical/cadical/bins.hpp b/third-party/cadical/cadical/bins.hpp new file mode 100644 index 0000000..e55f0f5 --- /dev/null +++ b/third-party/cadical/cadical/bins.hpp @@ -0,0 +1,17 @@ +#ifndef _bins_hpp_INCLUDED +#define _bins_hpp_INCLUDED + +#include "util.hpp" // Alphabetically after 'bins'. + +namespace CaDiCaL { + +using namespace std; + +typedef vector Bins; + +inline void shrink_bins (Bins & bs) { shrink_vector (bs); } +inline void erase_bins (Bins & bs) { erase_vector (bs); } + +} + +#endif diff --git a/third-party/cadical/cadical/block.cpp b/third-party/cadical/cadical/block.cpp new file mode 100644 index 0000000..c4c0757 --- /dev/null +++ b/third-party/cadical/cadical/block.cpp @@ -0,0 +1,751 @@ +#include "internal.hpp" + +namespace CaDiCaL { + +/*------------------------------------------------------------------------*/ + +// This implements an inprocessing version of blocked clause elimination and +// is assumed to be triggered just before bounded variable elimination. It +// has a separate 'block' flag while variable elimination uses 'elim'. +// Thus it only tries to block clauses on a literal which was removed in an +// irredundant clause in negated form before and has not been tried to use +// as blocking literal since then. + +/*------------------------------------------------------------------------*/ + +inline bool block_more_occs_size::operator () (unsigned a, unsigned b) { + size_t s = internal->noccs (-internal->u2i (a)); + size_t t = internal->noccs (-internal->u2i (b)); + if (s > t) return true; + if (s < t) return false; + s = internal->noccs (internal->u2i (a)); + t = internal->noccs (internal->u2i (b)); + if (s > t) return true; + if (s < t) return false; + return a > b; +} + +/*------------------------------------------------------------------------*/ + +// Determine whether 'c' is blocked on 'lit', by first marking all its +// literals and then checking all resolvents with negative clauses (with +// '-lit') are tautological. We use a move-to-front scheme for both the +// occurrence list of negative clauses (with '-lit') and then for literals +// within each such clause. The clause move-to-front scheme has the goal to +// find non-tautological clauses faster in the future, while the literal +// move-to-front scheme has the goal to faster find the matching literal, +// which makes the resolvent tautological (again in the future). + +bool Internal::is_blocked_clause (Clause * c, int lit) { + + LOG (c, "trying to block on %d", lit); + + assert (c->size >= opts.blockminclslim); + assert (c->size <= opts.blockmaxclslim); + assert (active (lit)); + assert (!val (lit)); + assert (!c->garbage); + assert (!c->redundant); + assert (!level); + + mark (c); // First mark all literals in 'c'. + + Occs & os = occs (-lit); + LOG ("resolving against at most %zd clauses with %d", os.size (), -lit); + + bool res = true; // Result is true if all resolvents tautological. + + // Can not use 'auto' here since we update 'os' during traversal. + // + const auto end_of_os = os.end (); + auto i = os.begin (); + + Clause * prev_d = 0; // Previous non-tautological clause. + + for (; i != end_of_os; i++) + { + // Move the first clause with non-tautological resolvent to the front of + // the occurrence list to improve finding it faster later. + // + Clause * d = *i; + + assert (!d->garbage); + assert (!d->redundant); + assert (d->size <= opts.blockmaxclslim); + + *i = prev_d; // Move previous non-tautological clause + prev_d = d; // backwards but remember clause at this position. + + LOG (d, "resolving on %d against", lit); + stats.blockres++; + + int prev_other = 0; // Previous non-tautological literal. + + // No 'auto' since we update literals of 'd' during traversal. + // + const const_literal_iterator end_of_d = d->end (); + literal_iterator l; + + for (l = d->begin (); l != end_of_d; l++) + { + // Same move-to-front mechanism for literals within a clause. It + // moves the first negatively marked literal to the front to find it + // faster in the future. + // + const int other = *l; + *l = prev_other; + prev_other = other; + if (other == -lit) continue; + assert (other != lit); + assert (active (other)); + assert (!val (other)); + if (marked (other) < 0) { + LOG ("found tautological literal %d", other); + d->literals[0] = other; // Move to front of 'd'. + break; + } + } + + if (l == end_of_d) + { + LOG ("no tautological literal found"); + // + // Since we did not find a tautological literal we restore the old + // order of literals in the clause. + // + const const_literal_iterator begin_of_d = d->begin (); + while (l-- != begin_of_d) { + const int other = *l; + *l = prev_other; + prev_other = other; + } + res = false; // Now 'd' is a witness that 'c' is not blocked. + os[0] = d; // Move it to the front of the occurrence list. + break; + } + } + unmark (c); // ... all literals of the candidate clause. + + // If all resolvents are tautological and thus the clause is blocked we + // restore the old order of clauses in the occurrence list of '-lit'. + // + if (res) { + assert (i == end_of_os); + const auto boc = os.begin (); + while (i != boc) { + Clause * d = *--i; + *i = prev_d; + prev_d = d; + } + } + + return res; +} + +/*------------------------------------------------------------------------*/ + +void Internal::block_schedule (Blocker & blocker) +{ + // Set skip flags for all literals in too large clauses. + // + for (const auto & c : clauses) { + + if (c->garbage) continue; + if (c->redundant) continue; + if (c->size <= opts.blockmaxclslim) continue; + + for (const auto & lit : *c) + mark_skip (-lit); + } + + // Connect all literal occurrences in irredundant clauses. + // + for (const auto & c : clauses) { + + if (c->garbage) continue; + if (c->redundant) continue; + + for (const auto & lit : *c) { + assert (active (lit)); + assert (!val (lit)); + occs (lit).push_back (c); + } + } + + // We establish the invariant that 'noccs' gives the number of actual + // occurrences of 'lit' in non-garbage clauses, while 'occs' might still + // refer to garbage clauses, thus 'noccs (lit) <= occs (lit).size ()'. It + // is expensive to remove references to garbage clauses from 'occs' during + // blocked clause elimination, but decrementing 'noccs' is cheap. + + for (auto lit : lits) { + if (!active (lit)) continue; + assert (!val (lit)); + Occs & os = occs (lit); + noccs (lit) = os.size (); + } + + // Now we fill the schedule (priority queue) of candidate literals to be + // tried as blocking literals. It is probably slightly faster to do this + // in one go after all occurrences have been determined, instead of + // filling the priority queue during pushing occurrences. Filling the + // schedule can not be fused with the previous loop (easily) since we + // first have to initialize 'noccs' for both 'lit' and '-lit'. + + int skipped = 0; + + for (auto idx : vars) { + if (!active (idx)) continue; + if (frozen (idx)) { skipped += 2; continue; } + assert (!val (idx)); + for (int sign = -1; sign <= 1; sign += 2) { + const int lit = sign * idx; + if (marked_skip (lit)) { skipped++; continue; } + if (!marked_block (lit)) continue; + unmark_block (lit); + LOG ("scheduling %d with %" PRId64 " positive and %" PRId64 " negative occurrences", + lit, noccs (lit), noccs (-lit)); + blocker.schedule.push_back (vlit (lit)); + } + } + + PHASE ("block", stats.blockings, + "scheduled %zd candidate literals %.2f%% (%d skipped %.2f%%)", + blocker.schedule.size (), + percent (blocker.schedule.size (), 2.0*active ()), + skipped, percent (skipped, 2.0*active ())); +} + +/*------------------------------------------------------------------------*/ + +// A literal is pure if it only occurs positive. Then all clauses in which +// it occurs are blocked on it. This special case can be implemented faster +// than trying to block literals with at least one negative occurrence and +// is thus handled separately. It also allows to avoid pushing blocked +// clauses onto the extension stack. + +void Internal::block_pure_literal (Blocker & blocker, int lit) +{ + if (frozen (lit)) return; + assert (active (lit)); + + Occs & pos = occs (lit); + Occs & nos = occs (-lit); + + assert (!noccs (-lit)); +#ifndef NDEBUG + for (const auto & c : nos) assert (c->garbage); +#endif + stats.blockpurelits++; + LOG ("found pure literal %d", lit); + + int64_t pured = 0; + + for (const auto & c : pos) { + if (c->garbage) continue; + assert (!c->redundant); + LOG (c, "pure literal %d in", lit); + blocker.reschedule.push_back (c); + external->push_clause_on_extension_stack (c, lit); + stats.blockpured++; + mark_garbage (c); + pured++; + } + + erase_vector (pos); + erase_vector (nos); + + mark_pure (lit); + stats.blockpured++; + LOG ("blocking %" PRId64 " clauses on pure literal %d", pured, lit); +} + +/*------------------------------------------------------------------------*/ + +// If there is only one negative clause with '-lit' it is faster to mark it +// instead of marking all the positive clauses with 'lit' one after the +// other and then resolving against the negative clause. + +void +Internal::block_literal_with_one_negative_occ (Blocker & blocker, int lit) +{ + assert (active (lit)); + assert (!frozen (lit)); + assert (noccs (lit) > 0); + assert (noccs (-lit) == 1); + + Occs & nos = occs (-lit); + assert (nos.size () >= 1); + + Clause * d = 0; + for (const auto & c : nos) { + if (c->garbage) continue; + assert (!d); + d = c; +#ifndef NDEBUG + break; +#endif + } + assert (d); + nos.resize (1); + nos[0] = d; + + if (d && d->size > opts.blockmaxclslim) { + LOG (d, "skipped common antecedent"); + return; + } + + assert (!d->garbage); + assert (!d->redundant); + assert (d->size <= opts.blockmaxclslim); + + LOG (d, "common antecedent", lit); + mark (d); + + int64_t blocked = 0, skipped = 0; + + Occs & pos = occs (lit); + + // Again no 'auto' since 'pos' is update during traversal. + // + const auto eop = pos.end (); + auto j = pos.begin (), i = j; + + for (; i != eop; i++) + { + Clause * c = *j++ = *i; + + if (c->garbage) { j--; continue; } + if (c->size > opts.blockmaxclslim) { skipped++; continue; } + if (c->size < opts.blockminclslim) { skipped++; continue; } + + LOG (c, "trying to block on %d", lit); + + // We use the same literal move-to-front strategy as in + // 'is_blocked_clause'. See there for more explanations. + + int prev_other = 0; // Previous non-tautological literal. + + // No 'auto' since literals of 'c' are updated during traversal. + // + const const_literal_iterator end_of_c = c->end (); + literal_iterator l; + + for (l = c->begin (); l != end_of_c; l++) + { + const int other = *l; + *l = prev_other; + prev_other = other; + if (other == lit) continue; + assert (other != -lit); + assert (active (other)); + assert (!val (other)); + if (marked (other) < 0) { + LOG ("found tautological literal %d", other); + c->literals[0] = other; // Move to front of 'c'. + break; + } + } + + if (l == end_of_c) { + LOG ("no tautological literal found"); + + // Restore old literal order in the clause because. + + const const_literal_iterator begin_of_c = c->begin (); + while (l-- != begin_of_c) { + const int other = *l; + *l = prev_other; + prev_other = other; + } + + continue; // ... with next candidate 'c' in 'pos'. + } + + blocked++; + LOG (c, "blocked"); + external->push_clause_on_extension_stack (c, lit); + blocker.reschedule.push_back (c); + mark_garbage (c); + j--; + } + if (j == pos.begin ()) erase_vector (pos); + else pos.resize (j - pos.begin ()); + + stats.blocked += blocked; + LOG ("blocked %" PRId64 " clauses on %d (skipped %" PRId64 ")", blocked, lit, skipped); + + unmark (d); +} + +/*------------------------------------------------------------------------*/ + +// Determine the set of candidate clauses with 'lit', which are checked to +// be blocked by 'lit'. Filter out too large and small clauses and which do +// not have any negated other literal in any of the clauses with '-lit'. + +size_t Internal::block_candidates (Blocker & blocker, int lit) { + + assert (blocker.candidates.empty ()); + + Occs & pos = occs (lit); // Positive occurrences of 'lit'. + Occs & nos = occs (-lit); + + assert ((size_t) noccs (lit) <= pos.size ()); + assert ((size_t) noccs (-lit) == nos.size ()); // Already flushed. + + // Mark all literals in clauses with '-lit'. Note that 'mark2' uses + // separate bits for 'lit' and '-lit'. + // + for (const auto & c : nos) mark2 (c); + + const auto eop = pos.end (); + auto j = pos.begin (), i = j; + + for (; i != eop; i++) + { + Clause * c = *j++ = *i; + if (c->garbage) { j--; continue; } + assert (!c->redundant); + if (c->size > opts.blockmaxclslim) continue; + if (c->size < opts.blockminclslim) continue; + const const_literal_iterator eoc = c->end (); + const_literal_iterator l; + for (l = c->begin (); l != eoc; l++) { + const int other = *l; + if (other == lit) continue; + assert (other != -lit); + assert (active (other)); + assert (!val (other)); + if (marked2 (-other)) break; + } + if (l != eoc) blocker.candidates.push_back (c); + } + if (j == pos.begin ()) erase_vector (pos); + else pos.resize (j - pos.begin ()); + + assert (pos.size () == (size_t) noccs (lit)); // Now also flushed. + + for (const auto & c : nos) unmark (c); + + return blocker.candidates.size (); +} + +/*------------------------------------------------------------------------*/ + +// Try to find a clause with '-lit' which does not have any literal in +// clauses with 'lit'. If such a clause exists no candidate clause can be +// blocked on 'lit' since all candidates would produce a non-tautological +// resolvent with that clause. + +Clause * Internal::block_impossible (Blocker & blocker, int lit) +{ + assert (noccs (-lit) > 1); + assert (blocker.candidates.size () > 1); + + for (const auto & c : blocker.candidates) mark2 (c); + + Occs & nos = occs (-lit); + Clause * res = 0; + + for (const auto & c : nos) { + assert (!c->garbage); + assert (!c->redundant); + assert (c->size <= opts.blockmaxclslim); + const const_literal_iterator eoc = c->end (); + const_literal_iterator l; + for (l = c->begin (); l != eoc; l++) { + const int other = *l; + if (other == -lit) continue; + assert (other != lit); + assert (active (other)); + assert (!val (other)); + if (marked2 (-other)) break; + } + if (l == eoc) res = c; + } + + for (const auto & c : blocker.candidates) unmark (c); + + if (res) { + LOG (res, "common non-tautological resolvent producing"); + blocker.candidates.clear (); + } + + return res; +} + +/*------------------------------------------------------------------------*/ + +// In the general case we have at least two negative occurrences. + +void Internal::block_literal_with_at_least_two_negative_occs ( + Blocker & blocker, + int lit) +{ + assert (active (lit)); + assert (!frozen (lit)); + assert (noccs (lit) > 0); + assert (noccs (-lit) > 1); + + Occs & nos = occs (-lit); + assert ((size_t) noccs (-lit) <= nos.size ()); + + int max_size = 0; + + // Flush all garbage clauses in occurrence list 'nos' of '-lit' and + // determine the maximum size of negative clauses (with '-lit'). + // + const auto eon = nos.end (); + auto j = nos.begin (), i = j; + for (; i != eon; i++) + { + Clause * c = *j++ = *i; + if (c->garbage) j--; + else if (c->size > max_size) max_size = c->size; + } + if (j == nos.begin ()) erase_vector (nos); + else nos.resize (j - nos.begin ()); + + assert (nos.size () == (size_t) noccs (-lit)); + assert (nos.size () > 1); + + // If the maximum size of a negative clause (with '-lit') exceeds the + // maximum clause size limit ignore this candidate literal. + // + if (max_size > opts.blockmaxclslim) { + LOG ("maximum size %d of clauses with %d exceeds clause size limit %d", + max_size, -lit, opts.blockmaxclslim); + return; + } + + LOG ("maximum size %d of clauses with %d", max_size, -lit); + + // We filter candidate clauses with positive occurrence of 'lit' in + // 'blocker.candidates' and return if no candidate clause remains. + // Candidates should be small enough and should have at least one literal + // which occurs negated in one of the clauses with '-lit'. + // + size_t candidates = block_candidates (blocker, lit); + if (!candidates) { + LOG ("no candidate clauses found"); + return; + } + + LOG ("found %zd candidate clauses", candidates); + + // We further search for a clause with '-lit' that has no literal + // negated in any of the candidate clauses (except 'lit'). If such a + // clause exists, we know that none of the candidates is blocked. + // + if (candidates > 1 && block_impossible (blocker, lit)) { + LOG ("impossible to block any candidate clause on %d", lit); + assert (blocker.candidates.empty ()); + return; + } + + LOG ("trying to block %zd clauses out of %" PRId64 " with literal %d", + candidates, noccs (lit), lit); + + int64_t blocked = 0; + + // Go over all remaining candidates and try to block them on 'lit'. + // + for (const auto & c : blocker.candidates) { + assert (!c->garbage); + assert (!c->redundant); + if (!is_blocked_clause (c, lit)) continue; + blocked++; + LOG (c, "blocked"); + external->push_clause_on_extension_stack (c, lit); + blocker.reschedule.push_back (c); + mark_garbage (c); + } + + LOG ("blocked %" PRId64 " clauses on %d out of %zd candidates in %zd occurrences", + blocked, lit, blocker.candidates.size (), occs (lit).size ()); + + blocker.candidates.clear (); + stats.blocked += blocked; + if (blocked) flush_occs (lit); +} + +/*------------------------------------------------------------------------*/ + +// Reschedule literals in a clause (except 'lit') which was blocked. + +void +Internal::block_reschedule_clause (Blocker & blocker, int lit, Clause * c) +{ +#ifdef NDEBUG + (void) lit; +#endif + assert (c->garbage); + + for (const auto & other : *c) { + + int64_t & n = noccs (other); + assert (n > 0); + n--; + + LOG ("updating %d with %" PRId64 " positive and %" PRId64 " negative occurrences", + other, noccs (other), noccs (-other)); + + if (blocker.schedule.contains (vlit (-other))) + blocker.schedule.update (vlit (-other)); + else if (active (other) && + !frozen (other) && + !marked_skip (-other)) { + LOG ("rescheduling to block clauses on %d", -other); + blocker.schedule.push_back (vlit (-other)); + } + + if (blocker.schedule.contains (vlit (other))) { + assert (other != lit); + blocker.schedule.update (vlit (other)); + } + } +} + +// Reschedule all literals in clauses blocked by 'lit' (except 'lit'). + +void Internal::block_reschedule (Blocker & blocker, int lit) +{ + while (!blocker.reschedule.empty ()) { + Clause * c = blocker.reschedule.back (); + blocker.reschedule.pop_back (); + block_reschedule_clause (blocker, lit, c); + } +} + +/*------------------------------------------------------------------------*/ + +void Internal::block_literal (Blocker & blocker, int lit) +{ + assert (!marked_skip (lit)); + + if (!active (lit)) return; // Pure literal '-lit'. + if (frozen (lit)) return; + + assert (!val (lit)); + + // If the maximum number of a negative clauses (with '-lit') exceeds the + // occurrence limit ignore this candidate literal. + // + if (noccs (-lit) > opts.blockocclim) return; + + LOG ("blocking literal candidate %d " + "with %" PRId64 " positive and %" PRId64 " negative occurrences", + lit, noccs (lit), noccs (-lit)); + + stats.blockcands++; + + assert (blocker.reschedule.empty ()); + assert (blocker.candidates.empty ()); + + if (!noccs (-lit)) block_pure_literal (blocker, lit); + else if (!noccs (lit)) { + // Rare situation, where the clause length limit was hit for 'lit' and + // '-lit' is skipped and then it becomes pure. Can be ignored. We also + // so it once happing for a 'elimboundmin=-1' and zero positive and one + // negative occurrence. + } else if (noccs (-lit) == 1) + block_literal_with_one_negative_occ (blocker, lit); + else + block_literal_with_at_least_two_negative_occs (blocker, lit); + + // Done with blocked clause elimination on this literal and we do not + // have to try blocked clause elimination on it again until irredundant + // clauses with its negation are removed. + // + assert (!frozen (lit)); // just to be sure ... + unmark_block (lit); +} + +/*------------------------------------------------------------------------*/ + +bool Internal::block () { + + if (!opts.block) return false; + if (unsat) return false; + if (!stats.current.irredundant) return false; + if (terminated_asynchronously ()) return false; + + if (propagated < trail.size ()) { + LOG ("need to propagate %zd units first", trail.size () - propagated); + init_watches (); + connect_watches (); + if (!propagate ()) { + LOG ("propagating units results in empty clause"); + learn_empty_clause (); + assert (unsat); + } + clear_watches (); + reset_watches (); + if (unsat) return false; + } + + START_SIMPLIFIER (block, BLOCK); + + stats.blockings++; + + LOG ("block-%" PRId64 "", stats.blockings); + + assert (!level); + assert (!watching ()); + assert (!occurring ()); + + mark_satisfied_clauses_as_garbage (); + + init_occs (); // Occurrence lists for all literals. + init_noccs (); // Number of occurrences to avoid flushing garbage clauses. + + Blocker blocker (this); + block_schedule (blocker); + + int64_t blocked = stats.blocked; + int64_t resolutions = stats.blockres; + int64_t purelits = stats.blockpurelits; + int64_t pured = stats.blockpured; + + while (!terminated_asynchronously () && + !blocker.schedule.empty ()) { + int lit = u2i (blocker.schedule.front ()); + blocker.schedule.pop_front (); + block_literal (blocker, lit); + block_reschedule (blocker, lit); + } + + blocker.erase (); + reset_noccs (); + reset_occs (); + + resolutions = stats.blockres - resolutions; + blocked = stats.blocked - blocked; + + PHASE ("block", stats.blockings, + "blocked %" PRId64 " clauses in %" PRId64 " resolutions", + blocked, resolutions); + + pured = stats.blockpured - pured; + purelits = stats.blockpurelits - purelits; + + if (pured) + mark_redundant_clauses_with_eliminated_variables_as_garbage (); + + if (purelits) + PHASE ("block", stats.blockings, + "found %" PRId64 " pure literals in %" PRId64 " clauses", + purelits, pured); + else + PHASE ("block", stats.blockings, + "no pure literals found"); + + report ('b', !opts.reportall && !blocked); + + STOP_SIMPLIFIER (block, BLOCK); + + return blocked; +} + +} diff --git a/third-party/cadical/cadical/block.hpp b/third-party/cadical/cadical/block.hpp new file mode 100644 index 0000000..04ce12e --- /dev/null +++ b/third-party/cadical/cadical/block.hpp @@ -0,0 +1,37 @@ +#ifndef _block_hpp_INCLUDED +#define _block_hpp_INCLUDED + +#include "heap.hpp" // Alphabetically after 'block.hpp'. + +namespace CaDiCaL { + +struct Internal; + +struct block_more_occs_size { + Internal * internal; + block_more_occs_size (Internal * i) : internal (i) { } + bool operator () (unsigned a, unsigned b); +}; + +typedef heap BlockSchedule; + +class Blocker { + + friend struct Internal; + + vector candidates; + vector reschedule; + BlockSchedule schedule; + + Blocker (Internal * i) : schedule (block_more_occs_size (i)) { } + + void erase () { + erase_vector (candidates); + erase_vector (reschedule); + schedule.erase (); + } +}; + +} + +#endif diff --git a/third-party/cadical/cadical/cadical.cpp b/third-party/cadical/cadical/cadical.cpp new file mode 100644 index 0000000..d0dd42e --- /dev/null +++ b/third-party/cadical/cadical/cadical.cpp @@ -0,0 +1,1065 @@ +/*------------------------------------------------------------------------*/ + +// Do include 'internal.hpp' but try to minimize internal dependencies. + +#include "internal.hpp" +#include "signal.hpp" // Separate, only need for apps. + +/*------------------------------------------------------------------------*/ + +namespace CaDiCaL { + +// A wrapper app which makes up the CaDiCaL stand alone solver. It in +// essence only consists of the 'App::main' function. So this class +// contains code, which is not required if only the library interface in +// the class 'Solver' is used (defined in 'cadical.hpp'). It further uses +// static data structures in order to have a signal handler catch signals. +// +// It is thus neither thread-safe nor reentrant. If you want to use +// multiple instances of the solver use the 'Solver' interface directly +// which is thread-safe and reentrant among different solver instances. + +/*------------------------------------------------------------------------*/ + +// Jobs for running multiple solvers (sequentially and later in parallel). + +#ifdef _MSC_VER +namespace { +bool isatty(int) { + return false; +} +} +#endif + +struct Job +{ + int left; // Number of discrepancies. + int depth; // Splitting depth. + int64_t id; // Unique identifier. + string path; // Path from root node ('0'=left '1'=right). + + Job * parent; // Parent job. + Solver * solver; // This solver (might be zero). + + Job (Job * p, Solver * s) : parent (p), solver (s) { } + ~Job () { if (solver) delete solver; } + + // Compare jobs and prefer low discrepancy jobs (are smaller). + // + bool less (const Job & other) const { + if (solver && !other.solver) return true; + if (!solver && other.solver) return false; + if (solver) { + if (left > other.left) return true; + if (left < other.left) return false; + } + return id < other.id; + } +}; + +/*------------------------------------------------------------------------*/ + +class App : public Handler, public Terminator { + + Solver * root; // Global root solver. + Solver * winner; // Solver which found solution. + + vector jobs; // Our job working queue. + + bool multiple; // Set implicitly by '-p', '-D' etc. + + // Command line options. + // + // bool parallel; // '-p' + int max_depth; // '-D' + // int max_solvers; // '-S' + // int max_threads; // '-T' + int time_limit; // '-t ' + + // Strictness of (DIMACS) parsing: + // + // 0 = force parsing and completely ignore header + // 1 = relaxed header handling (default) + // 2 = strict header handling + // + // To use '0' use '-f' of '--force'. + // To use '2' use '--strict'. + // + int force_strict_parsing; + + bool force_writing; + static bool most_likely_existing_cnf_file (const char * path); + + // Shared global statistics over all solvers. + // + struct { + int64_t solvers; + int64_t decisions; + int64_t conflicts; + } stats; + + // Internal variables. + // + int max_var; // Set after parsing. + volatile bool timesup; // Asynchronous termination. + + // Printing. + // + void print_usage (bool all = false); + void print_witness (FILE *); + +#ifndef QUIET + void signal_message (const char * msg, int sig); +#endif + + // Option handling. + // + bool set (const char*); + bool set (const char*, int); + int get (const char*); + bool verbose () { return get ("verbose") && !get ("quiet"); } + + /*----------------------------------------------------------------------*/ + + void initialize_root () { + root = new Solver (); + Job * res = new Job (0, root); + jobs.push_back (res); + res->id = stats.solvers++; + res->depth = 0; + res->left = 0; + } + + bool split () { + if (!max_depth) return false; + Job * best = 0; + for (auto & job : jobs) + if (job->solver && (!best || job->less (*best))) + best = job; + if (!best) return false; + // TODO check memory limit ... + // TODO split ... + return false; + } + + /*----------------------------------------------------------------------*/ + + // The actual initialization. + // + void init (); + + // Terminator interface. + // + bool terminate () { return timesup; } + + // Handler interface. + // + void catch_signal (int sig); + void catch_alarm (); + +public: + + App (); + ~App (); + + // Parse the arguments and run the solver. + // + int main (int arg, char ** argv); +}; + +/*------------------------------------------------------------------------*/ + +void App::print_usage (bool all) { + printf ( +"usage: cadical [