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.
This commit is contained in:
parent
1bd9efd057
commit
c34e073af6
|
@ -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
|
|
@ -107,6 +107,15 @@ ipasir-build: ipasir-download
|
||||||
$(MAKE) -C ../ipasir/sat/picosat961 libipasirpicosat961.a
|
$(MAKE) -C ../ipasir/sat/picosat961 libipasirpicosat961.a
|
||||||
@(cd ../ipasir; ln -sf sat/picosat961/libipasirpicosat961.a libipasir.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 :
|
doc :
|
||||||
doxygen
|
doxygen
|
||||||
|
|
||||||
|
|
|
@ -159,7 +159,7 @@ else
|
||||||
endif
|
endif
|
||||||
|
|
||||||
# select default solver to be minisat2 if no other is specified
|
# select default solver to be minisat2 if no other is specified
|
||||||
ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT),)
|
ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT)$(CADICAL),)
|
||||||
MINISAT2 = ../../minisat-2.2.1
|
MINISAT2 = ../../minisat-2.2.1
|
||||||
endif
|
endif
|
||||||
|
|
||||||
|
@ -195,6 +195,10 @@ ifneq ($(GLUCOSE),)
|
||||||
CP_CXXFLAGS += -DHAVE_GLUCOSE
|
CP_CXXFLAGS += -DHAVE_GLUCOSE
|
||||||
endif
|
endif
|
||||||
|
|
||||||
|
ifneq ($(CADICAL),)
|
||||||
|
CP_CXXFLAGS += -DHAVE_CADICAL
|
||||||
|
endif
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
first_target: all
|
first_target: all
|
||||||
|
|
|
@ -24,6 +24,7 @@ endif
|
||||||
#MINISAT2 = ../../minisat-2.2.1
|
#MINISAT2 = ../../minisat-2.2.1
|
||||||
#IPASIR = ../../ipasir
|
#IPASIR = ../../ipasir
|
||||||
#GLUCOSE = ../../glucose-syrup
|
#GLUCOSE = ../../glucose-syrup
|
||||||
|
#CADICAL = ../../cadical
|
||||||
|
|
||||||
# Extra library for SAT solver. This should link to the archive file to be used
|
# Extra library for SAT solver. This should link to the archive file to be used
|
||||||
# when linking against an IPASIR solver.
|
# when linking against an IPASIR solver.
|
||||||
|
@ -57,6 +58,10 @@ ifneq ($(GLUCOSE),)
|
||||||
CP_CXXFLAGS += -DSATCHECK_GLUCOSE
|
CP_CXXFLAGS += -DSATCHECK_GLUCOSE
|
||||||
endif
|
endif
|
||||||
|
|
||||||
|
ifneq ($(CADICAL),)
|
||||||
|
CP_CXXFLAGS += -DSATCHECK_CADICAL
|
||||||
|
endif
|
||||||
|
|
||||||
# Signing identity for MacOS Gatekeeper
|
# Signing identity for MacOS Gatekeeper
|
||||||
|
|
||||||
OSX_IDENTITY="Developer ID Application: Daniel Kroening"
|
OSX_IDENTITY="Developer ID Application: Daniel Kroening"
|
||||||
|
|
|
@ -67,6 +67,13 @@ ifneq ($(LINGELING),)
|
||||||
CP_CXXFLAGS += -DHAVE_LINGELING
|
CP_CXXFLAGS += -DHAVE_LINGELING
|
||||||
endif
|
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) \
|
SRC = $(BOOLEFORCE_SRC) \
|
||||||
$(CHAFF_SRC) \
|
$(CHAFF_SRC) \
|
||||||
$(CUDD_SRC) \
|
$(CUDD_SRC) \
|
||||||
|
@ -77,6 +84,7 @@ SRC = $(BOOLEFORCE_SRC) \
|
||||||
$(MINISAT_SRC) \
|
$(MINISAT_SRC) \
|
||||||
$(PICOSAT_SRC) \
|
$(PICOSAT_SRC) \
|
||||||
$(SQUOLEM2_SRC) \
|
$(SQUOLEM2_SRC) \
|
||||||
|
$(CADICAL_SRC) \
|
||||||
cvc/cvc_conv.cpp \
|
cvc/cvc_conv.cpp \
|
||||||
cvc/cvc_dec.cpp \
|
cvc/cvc_dec.cpp \
|
||||||
flattening/arrays.cpp \
|
flattening/arrays.cpp \
|
||||||
|
@ -194,7 +202,7 @@ INCLUDES += -I .. \
|
||||||
$(CHAFF_INCLUDE) $(BOOLEFORCE_INCLUDE) $(MINISAT_INCLUDE) $(MINISAT2_INCLUDE) \
|
$(CHAFF_INCLUDE) $(BOOLEFORCE_INCLUDE) $(MINISAT_INCLUDE) $(MINISAT2_INCLUDE) \
|
||||||
$(IPASIR_INCLUDE) \
|
$(IPASIR_INCLUDE) \
|
||||||
$(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \
|
$(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \
|
||||||
$(PICOSAT_INCLUDE) $(LINGELING_INCLUDE)
|
$(PICOSAT_INCLUDE) $(LINGELING_INCLUDE) $(CADICAL_INCLUDE)
|
||||||
|
|
||||||
CLEANFILES += solvers$(LIBEXT) \
|
CLEANFILES += solvers$(LIBEXT) \
|
||||||
smt2_solver$(EXEEXT) smt2/smt2_solver$(OBJEXT) smt2/smt2_solver$(DEPEXT)
|
smt2_solver$(EXEEXT) smt2/smt2_solver$(OBJEXT) smt2/smt2_solver$(DEPEXT)
|
||||||
|
@ -211,7 +219,7 @@ endif
|
||||||
|
|
||||||
SOLVER_LIB = $(CHAFF_LIB) $(BOOLEFORCE_LIB) $(MINISAT_LIB) \
|
SOLVER_LIB = $(CHAFF_LIB) $(BOOLEFORCE_LIB) $(MINISAT_LIB) \
|
||||||
$(MINISAT2_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \
|
$(MINISAT2_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \
|
||||||
$(PICOSAT_LIB) $(LINGELING_LIB) $(GLUCOSE_LIB)
|
$(PICOSAT_LIB) $(LINGELING_LIB) $(GLUCOSE_LIB) $(CADICAL_LIB)
|
||||||
|
|
||||||
###############################################################################
|
###############################################################################
|
||||||
|
|
||||||
|
|
|
@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
|
||||||
// #define SATCHECK_BOOLEFORCE
|
// #define SATCHECK_BOOLEFORCE
|
||||||
// #define SATCHECK_PICOSAT
|
// #define SATCHECK_PICOSAT
|
||||||
// #define SATCHECK_LINGELING
|
// #define SATCHECK_LINGELING
|
||||||
|
// #define SATCHECK_CADICAL
|
||||||
|
|
||||||
#if defined(HAVE_IPASIR) && !defined(SATCHECK_IPASIR)
|
#if defined(HAVE_IPASIR) && !defined(SATCHECK_IPASIR)
|
||||||
#define SATCHECK_IPASIR
|
#define SATCHECK_IPASIR
|
||||||
|
@ -54,6 +55,10 @@ Author: Daniel Kroening, kroening@kroening.com
|
||||||
#define SATCHECK_LINGELING
|
#define SATCHECK_LINGELING
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
|
#if defined(HAVE_CADICAL) && !defined(SATCHECK_CADICAL)
|
||||||
|
#define SATCHECK_CADICAL
|
||||||
|
#endif
|
||||||
|
|
||||||
#if defined SATCHECK_ZCHAFF
|
#if defined SATCHECK_ZCHAFF
|
||||||
|
|
||||||
#include "satcheck_zchaff.h"
|
#include "satcheck_zchaff.h"
|
||||||
|
@ -110,6 +115,13 @@ typedef satcheck_lingelingt satcheck_no_simplifiert;
|
||||||
typedef satcheck_glucose_simplifiert satcheckt;
|
typedef satcheck_glucose_simplifiert satcheckt;
|
||||||
typedef satcheck_glucose_no_simplifiert satcheck_no_simplifiert;
|
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
|
||||||
|
|
||||||
#endif // CPROVER_SOLVERS_SAT_SATCHECK_H
|
#endif // CPROVER_SOLVERS_SAT_SATCHECK_H
|
||||||
|
|
|
@ -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
|
|
@ -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() override;
|
||||||
|
virtual resultt prop_solve() override;
|
||||||
|
virtual tvt l_get(literalt a) const override;
|
||||||
|
|
||||||
|
virtual void lcnf(const bvt &bv) override;
|
||||||
|
virtual void set_assignment(literalt a, bool value) override;
|
||||||
|
|
||||||
|
virtual void set_assumptions(const bvt &_assumptions) override;
|
||||||
|
virtual bool has_set_assumptions() const override { return false; }
|
||||||
|
virtual bool has_is_in_conflict() const override { return false; }
|
||||||
|
virtual bool is_in_conflict(literalt a) const override;
|
||||||
|
|
||||||
|
protected:
|
||||||
|
// NOLINTNEXTLINE(readability/identifiers)
|
||||||
|
CaDiCaL::Solver * solver;
|
||||||
|
};
|
||||||
|
|
||||||
|
#endif // CPROVER_SOLVERS_SAT_SATCHECK_CADICAL_H
|
Loading…
Reference in New Issue