Add support for CaDiCaL

CaDiCaL is Armin Biere's latest solver with a minimal IPASIR-compatible
interface. In some initial experiments it considerable outperforms Minisat.

Author: tautschnig

scripts/cadical-patch

@@ -0,0 +1,10 @@
+--- a/src/cadical.hpp	2018-03-10 14:22:11.000000000 +0000
++++ b/src/cadical.hpp	2018-03-31 16:18:32.000000000 +0100
+@@ -141,6 +141,6 @@
+   File * output ();             // get access to internal 'output' file
+ };
+ 
+-};
++}
+ 
+ #endif

src/Makefile

@@ -107,6 +107,15 @@ ipasir-build: ipasir-download
 	$(MAKE) -C ../ipasir/sat/picosat961 libipasirpicosat961.a
 	@(cd ../ipasir; ln -sf sat/picosat961/libipasirpicosat961.a libipasir.a)
 
+cadical_release = rel-06w
+cadical-download:
+	@echo "Downloading CaDiCaL $(cadical_release)"
+	@curl -L https://github.com/arminbiere/cadical/archive/$(cadical_release).tar.gz | tar xz
+	@rm -Rf ../cadical
+	@mv cadical-$(cadical_release) ../cadical
+	@(cd ../cadical; patch -p1 < ../scripts/cadical-patch)
+	@cd ../cadical && CXX=$(CXX) CXXFLAGS=-O3 ./configure --debug && make
+
 doc :
 	doxygen
 

src/common

@@ -156,7 +156,7 @@ else
 endif
 
 # select default solver to be minisat2 if no other is specified
-ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT)$(PRECOSAT),)
+ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT)$(PRECOSAT)$(CADICAL),)
   MINISAT2 = ../../minisat-2.2.1
 endif
 
@@ -196,6 +196,10 @@ ifneq ($(GLUCOSE),)
   CP_CXXFLAGS += -DHAVE_GLUCOSE
 endif
 
+ifneq ($(CADICAL),)
+  CP_CXXFLAGS += -DHAVE_CADICAL
+endif
+
 
 
 first_target: all

src/config.inc

@@ -25,6 +25,7 @@ endif
 #MINISAT2 = ../../minisat-2.2.1
 #IPASIR = ../../ipasir
 #GLUCOSE = ../../glucose-syrup
+#CADICAL = ../../cadical
 #SMVSAT =
 
 # Extra library for SAT solver. This should link to the archive file to be used
@@ -63,6 +64,10 @@ ifneq ($(GLUCOSE),)
   CP_CXXFLAGS += -DSATCHECK_GLUCOSE
 endif
 
+ifneq ($(CADICAL),)
+  CP_CXXFLAGS += -DSATCHECK_CADICAL
+endif
+
 ifneq ($(SMVSAT),)
   CP_CXXFLAGS += -DSATCHECK_SMVSAT
 endif

src/solvers/Makefile

@@ -84,6 +84,13 @@ ifneq ($(LIMMAT),)
   CP_CXXFLAGS += -DHAVE_LIMMAT
 endif
 
+ifneq ($(CADICAL),)
+  CADICAL_SRC=sat/satcheck_cadical.cpp
+  CADICAL_INCLUDE=-I $(CADICAL)/src
+  CADICAL_LIB=$(CADICAL)/build/libcadical$(LIBEXT)
+  CP_CXXFLAGS += -DHAVE_CADICAL
+endif
+
 SRC = $(BOOLEFORCE_SRC) \
       $(CHAFF_SRC) \
       $(CUDD_SRC) \
@@ -97,6 +104,7 @@ SRC = $(BOOLEFORCE_SRC) \
       $(SMVSAT_SRC) \
       $(SQUOLEM2_SRC) \
       $(LIMMAT_SRC) \
+      $(CADICAL_SRC) \
       cvc/cvc_conv.cpp \
       cvc/cvc_dec.cpp \
       flattening/arrays.cpp \
@@ -215,7 +223,7 @@ INCLUDES += -I .. \
   $(CHAFF_INCLUDE) $(BOOLEFORCE_INCLUDE) $(MINISAT_INCLUDE) $(MINISAT2_INCLUDE) \
   $(IPASIR_INCLUDE) \
   $(SMVSAT_INCLUDE) $(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \
-	$(PRECOSAT_INCLUDE) $(PICOSAT_INCLUDE) $(LINGELING_INCLUDE)
+	$(PRECOSAT_INCLUDE) $(PICOSAT_INCLUDE) $(LINGELING_INCLUDE) $(CADICAL_INCLUDE)
 
 CLEANFILES = solvers$(LIBEXT) smt2_solver$(EXEEXT)
 
@@ -235,7 +243,7 @@ endif
 
 SOLVER_LIB = $(CHAFF_LIB) $(BOOLEFORCE_LIB) $(MINISAT_LIB) \
         $(MINISAT2_LIB) $(SMVSAT_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \
-	$(PRECOSAT_LIB) $(PICOSAT_LIB) $(LINGELING_LIB) $(GLUCOSE_LIB)
+	$(PRECOSAT_LIB) $(PICOSAT_LIB) $(LINGELING_LIB) $(GLUCOSE_LIB) $(CADICAL_LIB)
 
 ###############################################################################
 

src/solvers/sat/satcheck.h

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]
 // #define SATCHECK_PRECOSAT
 // #define SATCHECK_PICOSAT
 // #define SATCHECK_LINGELING
+// #define SATCHECK_CADICAL
 
 #if defined(HAVE_IPASIR) && !defined(SATCHECK_IPASIR)
 #define SATCHECK_IPASIR
@@ -59,6 +60,10 @@ Author: Daniel Kroening, [email protected]
 #define SATCHECK_LINGELING
 #endif
 
+#if defined(HAVE_CADICAL) && !defined(SATCHECK_CADICAL)
+#define SATCHECK_CADICAL
+#endif
+
 #if defined SATCHECK_ZCHAFF
 
 #include "satcheck_zchaff.h"
@@ -122,6 +127,13 @@ typedef satcheck_lingelingt satcheck_no_simplifiert;
 typedef satcheck_glucose_simplifiert satcheckt;
 typedef satcheck_glucose_no_simplifiert satcheck_no_simplifiert;
 
+#elif defined SATCHECK_CADICAL
+
+#include "satcheck_cadical.h"
+
+typedef satcheck_cadicalt satcheckt;
+typedef satcheck_cadicalt satcheck_no_simplifiert;
+
 #endif
 
 #endif // CPROVER_SOLVERS_SAT_SATCHECK_H

src/solvers/sat/satcheck_cadical.cpp

@@ -0,0 +1,129 @@
+/*******************************************************************\
+
+Module:
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#include "satcheck_cadical.h"
+
+#include <util/invariant.h>
+#include <util/threeval.h>
+
+#ifdef HAVE_CADICAL
+
+#include <cadical.hpp>
+
+tvt satcheck_cadicalt::l_get(literalt a) const
+{
+  if(a.is_constant())
+    return tvt(a.sign());
+
+  tvt result;
+
+  if(a.var_no() > static_cast<unsigned>(solver->max()))
+    return tvt(tvt::tv_enumt::TV_UNKNOWN);
+
+  const int val = solver->val(a.dimacs());
+  if(val>0)
+    result = tvt(true);
+  else if(val<0)
+    result = tvt(false);
+  else
+    return tvt(tvt::tv_enumt::TV_UNKNOWN);
+
+  return result;
+}
+
+const std::string satcheck_cadicalt::solver_text()
+{
+  return std::string("CaDiCaL ") + solver->version();
+}
+
+void satcheck_cadicalt::lcnf(const bvt &bv)
+{
+  for(const auto &lit : bv)
+  {
+    if(lit.is_true())
+      return;
+    else if(!lit.is_false())
+      INVARIANT(lit.var_no() < no_variables(), "reject out of bound variables");
+  }
+
+  for(const auto &lit : bv)
+  {
+    if(!lit.is_false())
+    {
+      // add literal with correct sign
+      solver->add(lit.dimacs());
+    }
+  }
+  solver->add(0); // terminate clause
+
+  clause_counter++;
+}
+
+propt::resultt satcheck_cadicalt::prop_solve()
+{
+  INVARIANT(status != statust::ERROR, "there cannot be an error");
+
+  messaget::status() << (no_variables() - 1) << " variables, " << clause_counter
+                     << " clauses" << eom;
+
+  if(status == statust::UNSAT)
+  {
+    messaget::status() << "SAT checker inconsistent: instance is UNSATISFIABLE"
+                       << eom;
+  }
+  else
+  {
+    switch(solver->solve())
+    {
+      case 10:
+        messaget::status() << "SAT checker: instance is SATISFIABLE" << eom;
+        status = statust::SAT;
+        return resultt::P_SATISFIABLE;
+      case 20:
+        messaget::status() << "SAT checker: instance is UNSATISFIABLE" << eom;
+        break;
+      default:
+        messaget::status() << "SAT checker: solving returned without solution"
+                           << eom;
+        throw "solving inside CaDiCaL SAT solver has been interrupted";
+    }
+  }
+
+  status = statust::UNSAT;
+  return resultt::P_UNSATISFIABLE;
+}
+
+void satcheck_cadicalt::set_assignment(literalt a, bool value)
+{
+  INVARIANT(!a.is_constant(), "cannot set an assignment for a constant");
+  INVARIANT(false, "method not supported");
+}
+
+satcheck_cadicalt::satcheck_cadicalt() :
+  solver(new CaDiCaL::Solver())
+{
+  solver->set("quiet", 1);
+}
+
+satcheck_cadicalt::~satcheck_cadicalt()
+{
+  delete solver;
+}
+
+void satcheck_cadicalt::set_assumptions(const bvt &bv)
+{
+  INVARIANT(false, "method not supported");
+}
+
+bool satcheck_cadicalt::is_in_conflict(literalt a) const
+{
+  INVARIANT(false, "method not supported");
+  return false;
+}
+
+#endif

src/solvers/sat/satcheck_cadical.h

@@ -0,0 +1,43 @@
+/*******************************************************************\
+
+Module:
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+
+#ifndef CPROVER_SOLVERS_SAT_SATCHECK_CADICAL_H
+#define CPROVER_SOLVERS_SAT_SATCHECK_CADICAL_H
+
+#include "cnf.h"
+
+namespace CaDiCaL // NOLINT(readability/namespace)
+{
+  class Solver; // NOLINT(readability/identifiers)
+}
+
+class satcheck_cadicalt:public cnf_solvert
+{
+public:
+  satcheck_cadicalt();
+  virtual ~satcheck_cadicalt();
+
+  virtual const std::string solver_text();
+  virtual resultt prop_solve();
+  virtual tvt l_get(literalt a) const;
+
+  virtual void lcnf(const bvt &bv);
+  virtual void set_assignment(literalt a, bool value);
+
+  virtual void set_assumptions(const bvt &_assumptions);
+  virtual bool has_set_assumptions() const { return false; }
+  virtual bool has_is_in_conflict() const { return false; }
+  virtual bool is_in_conflict(literalt a) const;
+
+protected:
+  // NOLINTNEXTLINE(readability/identifiers)
+  CaDiCaL::Solver * solver;
+};
+
+#endif // CPROVER_SOLVERS_SAT_SATCHECK_CADICAL_H