Add support for unsat cores

We implement basic support for computing unsat cores using our proof
producing capabilities.
We can obtain unsat core by logging resolution proof; the
compact version with resolution chains as logged by CDCL is sufficient.
We can then walk the resolution chains from root to the leaves, and
collect all the original clauses that participate in the proof. These
form unsat core at the clause level.
To lift the unsat core to the level of SMT-LIB assertion, we leverage
the fact that we propagate partitioning information from top-level
assertions to clauses.
We can, therefore collect the partition information from clausal unsat
core and then just take corresponding top-level assertions.

Author: blishko

src/api/MainSolver.cc

@@ -228,6 +228,20 @@ void MainSolver::printResolutionProofSMT2() const {
     return smt_solver->printResolutionProofSMT2(std::cout);
 }
 
+vec<PTRef> MainSolver::getUnsatCore() const {
+    using Partitions = ipartitions_t;
+    if (not config.produce_unsat_cores()) { throw OsmtApiException("Producing unsat cores is not enabled"); }
+    if (status != s_False) { throw OsmtApiException("Unsat core cannot be extracted if solver is not in UNSAT state"); }
+
+    vec<CRef> clauseRefs = smt_solver->getUnsatCoreClauses();
+    Partitions partitions;
+    for (CRef cref : clauseRefs) {
+        auto const & partition = pmanager.getClauseClassMask(cref);
+        opensmt::orbit(partitions, partitions, partition);
+    }
+    return pmanager.getPartitions(partitions);
+}
+
 lbool MainSolver::getTermValue(PTRef tr) const {
     if (logic.getSortRef(tr) != logic.getSort_bool()) { return l_Undef; }
     if (not term_mapper->hasLit(tr)) { return l_Undef; }

src/api/MainSolver.h

@@ -92,6 +92,8 @@ class MainSolver {
     // Returns model of the last query (must be in satisfiable state)
     std::unique_ptr<Model> getModel();
 
+    vec<PTRef> getUnsatCore() const;
+
     // Prints proof of the last query (must be in unsatisfiable state)
     void printResolutionProofSMT2() const;
 

src/options/SMTConfig.cc

@@ -445,6 +445,7 @@ const Info& SMTConfig::getInfo(const char* name) const {
 }
 
 const char* SMTConfig::o_produce_models = ":produce-models";
+const char* SMTConfig::o_produce_unsat_cores = ":produce-unsat-cores";
 const char* SMTConfig::o_verbosity      = ":verbosity";
 const char* SMTConfig::o_incremental    = ":incremental";
 const char* SMTConfig::o_produce_stats  = ":produce-stats";

src/options/SMTConfig.h

@@ -304,6 +304,7 @@ struct SMTConfig
   static const char* o_sat_split_randomize_lookahead;
   static const char* o_sat_split_randomize_lookahead_buf;
   static const char* o_produce_models;
+  static const char* o_produce_unsat_cores;
   static const char* o_sat_remove_symmetries;
   static const char* o_dryrun;
   static const char* o_do_substitutions;
@@ -511,6 +512,9 @@ struct SMTConfig
       return optionTable.has(o_produce_models) ?
               optionTable[o_produce_models]->getValue().numval :
               1; }
+  bool produce_unsat_cores() const {
+      return optionTable.has(o_produce_unsat_cores) && optionTable[o_produce_unsat_cores]->getValue().numval > 0;
+  }
   int          produceStats() const
      { return optionTable.has(o_produce_stats) ?
         optionTable[o_produce_stats]->getValue().numval == 1: false; }
@@ -579,8 +583,8 @@ struct SMTConfig
     { return optionTable.has(o_certify_inter) ?
         optionTable[o_certify_inter]->getValue().numval : 0; }
   bool produce_proof() const
-    { // produce_inter => produce_proof
-      if (produce_inter()) return true;
+    { // produce_inter or produce_unsat_core => produce_proof
+      if (produce_inter() or produce_unsat_cores()) return true;
       return optionTable.has(o_produce_proofs) ?
         optionTable[o_produce_proofs]->getValue().numval > 0 : false; }
   bool produce_inter() const

src/smtsolvers/CoreSMTSolver.cc

@@ -1897,3 +1897,28 @@ void CoreSMTSolver::fillBooleanVars(ModelBuilder &modelBuilder) {
         modelBuilder.addVarValue(atom, val);
     }
 }
+
+vec<CRef> CoreSMTSolver::getUnsatCoreClauses() const {
+    assert(resolutionProof);
+    vec<CRef> unsatCore;
+    auto const & derivations = resolutionProof->getProof();
+    std::vector<CRef> stack;
+    stack.push_back(CRef_Undef);
+    std::unordered_set<CRef> processed;
+    while (not stack.empty()) {
+        CRef current = stack.back();
+        stack.pop_back();
+        if (auto [_, inserted] = processed.insert(current); not inserted) { continue; }
+        auto it = derivations.find(current);
+        assert(it != derivations.end());
+        auto const & derivation = it->second;
+        if (derivation.type == clause_type::CLA_ORIG) {
+            unsatCore.push(current);
+            continue;
+        }
+        if (derivation.type == clause_type::CLA_LEARNT) {
+            for (CRef premise : derivation.chain_cla) { stack.push_back(premise); }
+        }
+    }
+    return unsatCore;
+}

src/smtsolvers/CoreSMTSolver.h

@@ -151,6 +151,7 @@ class CoreSMTSolver
     void fillBooleanVars(ModelBuilder & modelBuilder);
 
     ResolutionProof const & getResolutionProof() const { assert(resolutionProof); return *resolutionProof; }
+    vec<CRef> getUnsatCoreClauses() const;
 
     // Resource contraints:
     //

test/unit/CMakeLists.txt

@@ -148,6 +148,14 @@ target_sources(InterpolationTest
 target_link_libraries(InterpolationTest OpenSMT gtest gtest_main)
 gtest_add_tests(TARGET InterpolationTest)
 
+add_executable(UnsatCoreTest)
+target_sources(UnsatCoreTest
+    PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/test_UnsatCore.cc"
+    )
+
+target_link_libraries(UnsatCoreTest OpenSMT gtest gtest_main)
+gtest_add_tests(TARGET UnsatCoreTest)
+
 add_executable(ExplainTest)
 target_sources(ExplainTest
         PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/test_Explain.cc"

test/unit/test_UnsatCore.cc

@@ -0,0 +1,84 @@
+/*
+ *  Copyright (c) 2024, Martin Blicha <[email protected]>
+ *
+ *  SPDX-License-Identifier: MIT
+ */
+
+#include <gtest/gtest.h>
+#include <ArithLogic.h>
+#include <MainSolver.h>
+#include <SMTConfig.h>
+
+#include <memory>
+
+class UFUnsatCoreTest : public ::testing::Test {
+protected:
+    UFUnsatCoreTest(): logic{opensmt::Logic_t::QF_UF} {}
+    void SetUp() override {
+        ufsort = logic.declareUninterpretedSort("U");
+        x = logic.mkVar(ufsort, "x");
+        y = logic.mkVar(ufsort, "y");
+        f = logic.declareFun("f", ufsort, {ufsort});
+        g = logic.declareFun("g", ufsort, {ufsort, ufsort});
+        p = logic.declareFun("p", logic.getSort_bool(), {ufsort});
+        b1 = logic.mkBoolVar("b1");
+        b2 = logic.mkBoolVar("b2");
+        b3 = logic.mkBoolVar("b3");
+        b4 = logic.mkBoolVar("b4");
+        b5 = logic.mkBoolVar("b5");
+        nb1 = logic.mkNot(b1);
+        nb2 = logic.mkNot(b2);
+        nb3 = logic.mkNot(b3);
+        nb4 = logic.mkNot(b4);
+        nb5 = logic.mkNot(b5);
+    }
+    Logic logic;
+    SMTConfig config;
+    SRef ufsort;
+    PTRef x, y, b1, b2, b3, b4, b5;
+    PTRef nb1, nb2, nb3, nb4, nb5;
+    SymRef f, g, p;
+
+    MainSolver makeSolver() {
+        const char* msg = "ok";
+        config.setOption(SMTConfig::o_produce_unsat_cores, SMTOption(true), msg);
+        return {logic, config, "unsat_core"};
+    }
+};
+
+TEST_F(UFUnsatCoreTest, Bool_Simple) {
+    MainSolver solver = makeSolver();
+    solver.insertFormula(b1);
+    solver.insertFormula(b2);
+    solver.insertFormula(nb1);
+    auto res = solver.check();
+    ASSERT_EQ(res, s_False);
+    auto core = solver.getUnsatCore();
+    ASSERT_EQ(core.size(), 2);
+    EXPECT_TRUE(core[0] == b1 or core[1] == b1);
+    EXPECT_TRUE(core[0] == nb1 or core[1] == nb1);
+}
+
+TEST_F(UFUnsatCoreTest, Bool_ReuseProofChain) {
+    // We add three assertions
+    // a1 := (b1 or b2) and (b1 or ~b2)
+    // a2 := (~b1 or b3) and (~b1 or ~b3)
+    // a3 := b4
+    // The first two assertions form the unsat core.
+    MainSolver solver = makeSolver();
+    PTRef c1 = logic.mkOr(b1, b2);
+    PTRef c2 = logic.mkOr(b1, nb2);
+    PTRef c3 = logic.mkOr(nb1, b3);
+    PTRef c4 = logic.mkOr(nb1, nb3);
+    PTRef a1 = logic.mkAnd(c1,c2);
+    PTRef a2 = logic.mkAnd(c3,c4);
+    solver.insertFormula(a1);
+    solver.insertFormula(a2);
+    solver.insertFormula(b4);
+    auto res = solver.check();
+    ASSERT_EQ(res, s_False);
+    auto core = solver.getUnsatCore();
+    ASSERT_EQ(core.size(), 2);
+    EXPECT_TRUE(core[0] == a1 or core[1] == a1);
+    EXPECT_TRUE(core[0] == a2 or core[1] == a2);
+}