cadical bind implementation

lib/cadical_bind.cpp

@@ -12,6 +12,21 @@ SUBool::CadicalBind::SolverInit()
 {
    mSolver = std::make_unique<CaDiCaL::Solver>();
    mResult = PartialValue::UNDEF;
+   mSolver->set("seed", sub_rand() % 2147483647);
+   mSolver->set("verbose", -1);
+   mSolver->set("quiet", 1);
+   if (mCollectLearnts)
+   {
+      if (!mLearner)
+      {
+         mLearner = std::make_unique<CBLearner>();
+      }
+      else
+      {
+         mLearner->Clear();
+      }
+      mSolver->connect_learner(mLearner.get());
+   }
    Adapt();
 }
 
@@ -117,3 +132,161 @@ SUBool::CadicalBind::SolveLitBuffer() const
    return bool_of_partial_value(mResult);
 }
 
+SUBool::PartialValue
+SUBool::CadicalBind::ValueOfVariable(unsigned var) const
+{
+   if (!bool_of_partial_value(mResult, false))
+   {
+      throw NoModelException(
+          "CadicalBind::ValueOfVariable", "No model available");
+   }
+   return of_cadical_value(mSolver->val(var));
+}
+
+SUBool::PartialValue
+SUBool::CadicalBind::ValueOfLiteral(const Literal &lit) const
+{
+   if (!bool_of_partial_value(mResult, false))
+   {
+      throw NoModelException(
+          "CadicalBind::ValueOfVariable", "No model available");
+   }
+   return of_cadical_value(mSolver->val(dimacs_literal(lit)));
+}
+
+SUBool::PartialAssignment
+SUBool::CadicalBind::Model() const
+{
+   if (!bool_of_partial_value(mResult, false))
+   {
+      throw NoModelException("CadicalBind::Model", "No model available");
+   }
+   PartialAssignment alpha(mSolver->vars());
+   for (int i = 1; i <= mSolver->vars(); ++i)
+   {
+      alpha[i] = ValueOfVariable(i);
+   }
+   return alpha;
+}
+
+SUBool::Clause
+SUBool::CadicalBind::ConflictClause() const
+{
+   if (mResult != PartialValue::FALSE)
+   {
+      throw NoModelException(
+          "CadicalBind::ConflictClause", "No conflict clause available");
+   }
+   std::vector<Literal> conflict_literals;
+   conflict_literals.reserve(mLitBuffer.size());
+   for (const auto cadical_lit : mLitBuffer)
+   {
+      if (mSolver->failed(cadical_lit))
+      {
+         conflict_literals.push_back(literal_from_dimacs(-cadical_lit));
+      }
+   }
+   return conflict_literals;
+}
+
+void
+SUBool::CadicalBind::Adapt(const SolverInterface::ADAPTATION adapt)
+{
+   mAdapt = adapt;
+   Adapt();
+}
+
+void
+SUBool::CadicalBind::Adapt()
+{
+#if 0
+   // TODO: Unclear how, should be possible to do it similar to Kissat, but the
+   //       options are slightly different in CaDiCaL.
+   switch (mAdapt)
+   {
+   case SolverInterface::ADAPTATION::LIKELY_SAT:
+      mSolver->set("target", TARGET_SAT);
+      break;
+   case SolverInterface::ADAPTATION::LIKELY_UNSAT:
+      mSolver->set("stable", STABLE_UNSAT);
+      break;
+   default:
+      break;
+   }
+#endif
+}
+
+size_t
+SUBool::CadicalBind::LearntsSize() const
+{
+   if (!mLearner || !mCollectLearnts)
+   {
+      return 0;
+   }
+   return mLearner->LearntsSize();
+}
+
+std::vector<SUBool::Clause>
+SUBool::CadicalBind::Learnts() const
+{
+   if (!mLearner || !mCollectLearnts)
+   {
+      return {};
+   }
+   return mLearner->Learnts();
+}
+
+std::vector<SUBool::Clause>
+SUBool::CadicalBind::ExtractLearnts()
+{
+   if (!mLearner || !mCollectLearnts)
+   {
+      return {};
+   }
+   return mLearner->ExtractLearnts();
+}
+
+bool
+SUBool::CBLearner::learning(int size [[maybe_unused]])
+{
+   return true;
+}
+
+void
+SUBool::CBLearner::learn(int lit)
+{
+   if (lit == 0)
+   {
+      mLearnts.emplace_back(std::move(mBuffer));
+      mBuffer.clear();
+      return;
+   }
+   mBuffer.push_back(literal_from_dimacs(lit));
+}
+
+void
+SUBool::CBLearner::Clear()
+{
+   mLearnts.clear();
+   mBuffer.clear();
+}
+
+size_t
+SUBool::CBLearner::LearntsSize() const
+{
+   return mLearnts.size();
+}
+
+std::vector<SUBool::Clause>
+SUBool::CBLearner::Learnts() const
+{
+   return mLearnts;
+}
+
+std::vector<SUBool::Clause>
+SUBool::CBLearner::ExtractLearnts()
+{
+   auto learnts = std::move(mLearnts);
+   Clear();
+   return learnts;
+}

lib/cadical_bind.h

@@ -16,6 +16,22 @@
 #include "solver_bind.h"
 namespace SUBool
 {
+   class CBLearner : public CaDiCaL::Learner
+   {
+      std::vector<Clause> mLearnts{};
+      std::vector<Literal> mBuffer{};
+
+    public:
+      virtual bool learning(int size) override;
+      virtual void learn(int lit) override;
+
+      void Clear();
+
+      size_t LearntsSize() const;
+      std::vector<Clause> Learnts() const;
+      std::vector<Clause> ExtractLearnts();
+   };
+
    class CadicalBind : public SolverInterface
    {
     private:
@@ -24,6 +40,7 @@ namespace SUBool
       std::unique_ptr<CaDiCaL::Solver> mSolver{};
       mutable std::vector<int> mLitBuffer{};
       mutable PartialValue mResult{PartialValue::UNDEF};
+      std::unique_ptr<CBLearner> mLearner{};
 
     public:
       CadicalBind(
@@ -75,7 +92,30 @@ namespace SUBool
    };
 
    using CadicalWrapper = SolverWrapperTemplate<CadicalBind>;
+
+   Literal of_cadical_lit(int lit);
+   constexpr PartialValue of_cadical_value(int val);
 } // namespace SUBool
 
+constexpr SUBool::PartialValue
+SUBool::of_cadical_value(int val)
+{
+   if (val > 0)
+   {
+      return PartialValue::TRUE;
+   }
+   else if (val < 0)
+   {
+      return PartialValue::FALSE;
+   }
+   return PartialValue::UNDEF;
+}
+
+inline bool
+SUBool::CadicalBind::IsIncremental() const
+{
+   return true;
+}
+
 #endif // HAS_CADICAL
 #endif // __CADICAL_BIND_H

lib/kissat_bind.cpp

@@ -22,12 +22,6 @@ SUBool::of_kissat_value(int val)
    return PartialValue::UNDEF;
 }
 
-SUBool::Literal
-SUBool::of_kissat_lit(int lit)
-{
-   return Literal(abs(lit), lit > 0);
-}
-
 void
 SUBool::KissatSolver::Adapt(const SolverInterface::ADAPTATION adapt)
 {

lib/kissat_bind.h

@@ -101,7 +101,6 @@ namespace SUBool
 
    using KissatBindSolver = KissatBind<KissatSolver>;
 
-   Literal of_kissat_lit(int lit);
    PartialValue of_kissat_value(int val);
 
    using KissatSolverWrapper = SolverWrapperTemplate<KissatBindSolver>;
@@ -251,8 +250,7 @@ SUBool::KissatBind<Solver>::ValueOfLiteral(const Literal &lit) const
       throw NoModelException(
           "KissatBind::ValueOfLiteral", "No model available");
    }
-   return of_kissat_value(kissat_value(
-       mSolver->solver, lit.mPositive ? lit.Variable() : -lit.Variable()));
+   return of_kissat_value(kissat_value(mSolver->solver, dimacs_literal(lit)));
 }
 
 template <class Solver>
@@ -285,7 +283,7 @@ SUBool::KissatBind<Solver>::ConflictClause() const
       for (unsigned i = 0; i < mSolver->solver->conflict.size; ++i)
       {
          conflict_literals.push_back(
-             of_kissat_lit(mSolver->solver->conflict.lits[i]));
+             of_dimacs_lit(mSolver->solver->conflict.lits[i]));
       }
    }
    return conflict_literals;

lib/literal.h

@@ -73,6 +73,7 @@ namespace SUBool
    constexpr unsigned positive_literal_index(unsigned var) noexcept;
    constexpr unsigned negative_literal_index(unsigned var) noexcept;
    constexpr int dimacs_literal(const Literal &lit) noexcept;
+   Literal literal_from_dimacs(int dimacs_lit) noexcept;
 
    std::vector<Literal> literals_of_assignment(const Assignment &alpha);
    std::vector<Literal> literals_of_assignment(const PartialAssignment &alpha);
@@ -159,6 +160,12 @@ SUBool::dimacs_literal(const Literal &lit) noexcept
                           : -static_cast<int>(lit.Variable()));
 }
 
+inline SUBool::Literal
+SUBool::literal_from_dimacs(int lit) noexcept
+{
+   return Literal(abs(lit), lit > 0);
+}
+
 constexpr unsigned
 SUBool::Literal::Index() const noexcept
 {