constrain interface

LICENSE

@@ -2,6 +2,7 @@ MIT License
 
 Copyright (c) 2016-2021 Armin Biere, Johannes Kepler University Linz, Austria
 Copyright (c) 2020-2021 Mathias Fleury, Johannes Kepler University Linz, Austria
+Copyright (c) 2020-2021 Nils Froleyks, Johannes Kepler University Linz, Austria
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal

NEWS.md

@@ -0,0 +1,10 @@
+Version 1.5.0
+-------------
+
+- added constrain interface to optimize use with IC3
+
+Version 1.4.2
+-------------
+
+- replaced "`while () push_back ()`" with "`if () resize ()`" idiom
+  (thanks go to Alexander Smal for pointing this out)

VERSION

@@ -1 +1 @@
-1.4.1
+1.5.0

src/assume.cpp

@@ -31,135 +31,180 @@ void Internal::failing () {
   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) {
-
-    // TODO: if 'first' is on the root-level, then, as below, we probably
-    // want an empty core.
-
-    clause.push_back (first);
-    clause.push_back (-first);
-
-    Flags & f = flags (first);
+  if (!unsat_constraint) {
+    // Search for failing assumptions in the (internal) assumption stack.
 
-    unsigned bit = bign (first);
-    assert (!(f.failed & bit));
-    f.failed |= bit;
-    bit = bign (-first);
-    f.failed |= bit;
+    // There are in essence three cases: (1) An assumption is falsified on the
+    // root-level and then 'failed_unit' is set to that assumption, (2) two
+    // clashing assumptions are assumed and then 'failed_clashing' is set to
+    // the second assumed one, or otherwise (3) there is a failing assumption
+    // 'first_failed' with minimum (non-zero) decision level 'failed_level'.
 
-  } else {
+    int failed_unit = 0;
+    int failed_clashing = 0;
+    int first_failed = 0;
+    int failed_level = INT_MAX;
 
-    // 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;
+      if (val (lit) >= 0) continue;
+      const Var & v = var (lit);
+      if (!v.level) {
+        failed_unit = lit;
+        break;
+      }
+      if (failed_clashing) continue;
+      if (!v.reason) failed_clashing = lit;
+      else if (!first_failed || v.level < failed_level) {
+        first_failed = lit;
+        failed_level = v.level;
+      }
     }
 
-    assert (first);
-    LOG ("starting with assumption %d falsified on decision level %d",
-      first, var (first).level);
-
-    if (!var (first).level) {
-
-      // TODO: I think marking this should yield an empty core
-      // and not mark 'first' as failed (similarly above).
+    // Get the 'failed' assumption from one of the three cases.
+    int failed;
+    if (failed_unit)
+      failed = failed_unit;
+    else if (failed_clashing)
+      failed = failed_clashing;
+    else
+      failed = first_failed;
+    assert (failed);
+
+    // In any case mark literal 'failed' as failed assumption.
+    {
+      Flags & f = flags (failed);
+      const unsigned bit = bign (failed);
+      assert (!(f.failed & bit));
+      f.failed |= bit;
+    }
 
-      LOG ("failed assumption %d", first);
-      clause.push_back (-first);
+    // First case (1).
+    if (failed_unit) {
+      assert (failed == failed_unit);
+      LOG ("root-level falsified assumption %d", failed);
+      goto DONE;
+    }
 
-      Flags & f = flags (first);
-      const unsigned bit = bign (first);
+    // Second case (2).
+    if (failed_clashing) {
+      assert (failed == failed_clashing);
+      LOG ("clashing assumptions %d and %d", failed, -failed);
+      Flags & f = flags (-failed);
+      const unsigned bit = bign (-failed);
       assert (!(f.failed & bit));
       f.failed |= bit;
+      goto DONE;
+    }
 
-    } 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'.
+    // Fall through to third case (3).
+    LOG ("starting with assumption %d falsified on minimum decision level %d",
+        first_failed, failed_level);
+
+    assert (first_failed);
+    assert (failed_level > 0);
+
+    // 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_failed);
+      Flags & f = flags (first_failed);
+      assert (!f.seen);
+      f.seen = true;
+      assert (f.failed & bign (first_failed));
+      analyzed.push_back (-first_failed);
+      clause.push_back (-first_failed);
+    }
+  } else { // unsat_constraint
+    // The assumptions necessary to fail each literal in the constraint are
+    // collected.
+    for (auto lit : constraint) {
+      lit *= -1;
+      assert (lit != INT_MIN);
+      flags (lit).seen = true;
+      analyzed.push_back (lit);
+    }
+  }
 
-      {
-        LOG ("failed assumption %d", first);
-        Flags & f = flags (first);
-        const unsigned bit = bign (first);
+  {
+    size_t next = 0;
+
+    while (next < analyzed.size ()) {
+      const int lit = analyzed[next++];
+      assert (val (lit) > 0);
+      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;
-        f.seen = true;
       }
+    }
+    clear_analyzed_literals ();
+
+    // TODO: We can not do clause minimization here, right?
 
-      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;
+    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.
+    //
+    if (!unsat_constraint) {
+      external->check_learned_clause ();
+      if (proof) {
+        proof->add_derived_clause(clause);
+        proof->delete_clause(clause);
+      }
+    } else {
+      for (auto lit : constraint) {
+        clause.push_back(-lit);
+        external->check_learned_clause ();
+        if (proof) {
+          proof->add_derived_clause(clause);
+          proof->delete_clause(clause);
         }
+        clause.pop_back();
       }
-      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 ();
   }
-  clause.clear ();
+
+DONE:
 
   STOP (analyze);
 }
 
+bool Internal::failed (int lit) {
+  if (!marked_failed) {
+    failing ();
+    marked_failed = true;
+  }
+  Flags &f = flags (lit);
+  const unsigned bit = bign (lit);
+  return (f.failed & bit) != 0;
+}
+
 // Add the start of each incremental phase (leaving the state
 // 'UNSATISFIABLE' actually) we reset all assumptions.
 
@@ -173,6 +218,7 @@ void Internal::reset_assumptions () {
   }
   LOG ("cleared %zd assumptions", assumptions.size ());
   assumptions.clear ();
+  marked_failed = true;
 }
 
 }

src/bins.cpp

@@ -8,8 +8,8 @@ namespace CaDiCaL {
 
 void Internal::init_bins () {
   assert (big.empty ());
-  while (big.size () < 2*vsize)
-    big.push_back (Bins ());
+  if (big.size () < 2*vsize)
+    big.resize (2*vsize, Bins ());
   LOG ("initialized binary implication graph");
 }
 

src/cadical.hpp

@@ -133,13 +133,13 @@ namespace CaDiCaL {
 //               terminate (asynchronously)
 //      SOLVING  ------------------------->  UNKNOWN
 //
-// The important behaviour to remember is that adding or assuming a literal
-// (immediately) destroys the satisfying assignment in the 'SATISFIED' state
-// and vice versa resets all assumptions in the 'UNSATISFIED' state.  This
+// The important behaviour to remember is that adding, assuming or constraining
+// a literal (immediately) destroys the satisfying assignment in the 'SATISFIED'
+// state and vice versa resets all assumptions in the 'UNSATISFIED' state. This
 // is exactly the behaviour required by the IPASIR interface.
 //
 // Furthermore, the model can only be queried through 'val' in the
-// 'SATISFIED' state, while extracting failed assumptions with 'val' only in
+// 'SATISFIED' state, while extracting failed assumptions with 'failed' only in
 // the 'UNSATISFIED' state.  Solving can only be started in the 'UNKNOWN' or
 // 'CONFIGURING' state or after the previous call to 'solve' yielded an
 // 'UNKNOWN, 'SATISFIED' or 'UNSATISFIED' state.
@@ -286,6 +286,30 @@ class Solver {
 
   // ====== END IPASIR =====================================================
 
+  //------------------------------------------------------------------------
+  // Adds a literal to the constraint clause. Same functionality as 'add' but
+  // the clause only exists for the next call to solve (same lifetime as
+  // assumptions). Only one constraint may exists at a time. A new constraint
+  // replaces the old.
+  // The main application of this functonality is the model checking algorithm
+  // IC3. See our FMCAD'21 paper [FroleyksBiere-FMCAD'19] for more details.
+  //
+  // Add valid literal to the constraint clause or zero to terminate it.
+  //
+  //   require (VALID)                     // recall 'VALID = READY | ADDING'
+  //   if (lit) ensure (ADDING)            // and thus VALID but not READY
+  //   if (!lit) && !adding_clause ensure (UNKNOWN) // and thus READY
+  //
+  void constrain (int lit);
+
+  // Determine whether the constraint was used to proof the unsatisfiability.
+  // Note that the formula might still be unsatisfiable without the constraint.
+  //
+  //   require (UNSATISFIED)
+  //   ensure (UNSATISFIED)
+  //
+  bool constraint_failed ();
+
   //------------------------------------------------------------------------
   // This function determines a good splitting literal.  The result can be
   // zero if the formula is proven to be satisfiable or unsatisfiable.  This
@@ -305,7 +329,8 @@ class Solver {
 
   CubesWithStatus generate_cubes(int, int min_depth = 0);
 
-  void reset_assumptions();
+  void reset_assumptions ();
+  void reset_constraint ();
 
   // Return the current state of the solver as defined above.
   //
@@ -684,6 +709,11 @@ class Solver {
 
   //==== start of state ====================================================
 
+  // The solver is in the state ADDING if either the current clause or the
+  // constraint (or both) is not yet terminated.
+  bool adding_clause;
+  bool adding_constraint;
+
   State _state;            // API states as discussed above.
 
   /*----------------------------------------------------------------------*/