Add SAT solver Cadical

CMakeLists.txt

@@ -217,6 +217,7 @@ include_directories(
 	# SYSTEM ${PROJECT_BINARY_DIR}/third-party/or-tools
 	SYSTEM third-party/abseil-cpp
 	SYSTEM third-party/bliss
+	SYSTEM third-party/cadical
 	SYSTEM third-party/Catch
 	SYSTEM third-party/Eigen
 	SYSTEM third-party/FADBAD++

minimum/linear/CMakeLists.txt

@@ -3,6 +3,7 @@ library_with_tests("minimum_linear"
     "absl_str_format"
 	"absl::flat_hash_map"
 	"absl::flat_hash_set"
+	"cadical"
 	"cleaneling"
 	"glpk"
 	"glucose"

minimum/linear/cadical_solver.cpp

@@ -0,0 +1,83 @@
+#include <iterator>
+#include <string>
+
+#include <third-party/cadical/cadical/cadical.hpp>
+
+#include <minimum/core/check.h>
+#include <minimum/core/scope_guard.h>
+#include <minimum/core/string.h>
+#include <minimum/linear/easy-ip-internal.h>
+#include <minimum/linear/ip.h>
+#include <minimum/linear/ip_to_sat_solver.h>
+#include <minimum/linear/sat_solver.h>
+
+using minimum::core::check;
+
+namespace minimum {
+namespace linear {
+
+class CadicalInternalSatSolver : public SatSolver {
+   public:
+	CadicalInternalSatSolver(bool silent_mode);
+
+	virtual Var add_variable() override;
+	virtual Var add_helper_variable() override;
+	virtual void add_clause(const std::vector<Literal>& clause) override;
+	virtual bool solve(std::vector<int>* solution) override;
+	virtual bool solve(const std::vector<Literal>& assumptions,
+	                   std::vector<int>* solution) override;
+
+   private:
+	CaDiCaL::Solver solver;
+	std::vector<int> literals;
+};
+
+std::unique_ptr<SatSolver> cadical_solver(bool silent_mode) {
+	return std::make_unique<CadicalInternalSatSolver>(silent_mode);
+}
+
+CadicalInternalSatSolver::CadicalInternalSatSolver(bool silent_mode) {}
+
+SatSolver::Var CadicalInternalSatSolver::add_variable() {
+	literals.push_back(literals.size() + 1);
+	return literals.back() - 1;
+}
+
+SatSolver::Var CadicalInternalSatSolver::add_helper_variable() { return add_variable(); }
+
+void CadicalInternalSatSolver::add_clause(const std::vector<Literal>& clause) {
+	for (auto& literal : clause) {
+		if (literal.second) {
+			solver.add(literal.first + 1);
+		} else {
+			solver.add(-literal.first - 1);
+		}
+	}
+	solver.add(0);
+}
+
+bool CadicalInternalSatSolver::solve(std::vector<int>* solution) {
+	bool result = solver.solve() == 10;
+	if (result) {
+		solution->clear();
+		for (auto& lit : literals) {
+			auto value = solver.val(lit);
+			solution->push_back(value > 0 ? 1 : 0);
+		}
+	}
+	return result;
+}
+
+bool CadicalInternalSatSolver::solve(const std::vector<Literal>& assumptions,
+                                     std::vector<int>* solution) {
+	for (auto& literal : assumptions) {
+		if (literal.second) {
+			solver.assume(literal.first + 1);
+		} else {
+			solver.assume(-literal.first - 1);
+		}
+	}
+	return solve(solution);
+}
+}  // namespace linear
+}  // namespace minimum

minimum/linear/sat_solver.h

@@ -44,5 +44,6 @@ class SatSolver {
 std::unique_ptr<SatSolver> MINIMUM_LINEAR_API minisat_solver(bool silent_mode = false);
 std::unique_ptr<SatSolver> MINIMUM_LINEAR_API cleaneling_solver();
 std::unique_ptr<SatSolver> MINIMUM_LINEAR_API glucose_solver();
+std::unique_ptr<SatSolver> MINIMUM_LINEAR_API cadical_solver(bool silent_mode = false);
 }  // namespace linear
 }  // namespace minimum

minimum/linear/sat_test.cpp

@@ -181,6 +181,10 @@ TEST_CASE("minisatp") {
 
 TEST_CASE("glucose") { simple_test(glucose_solver); }
 
+TEST_CASE("cadical") {
+	simple_test([]() { return cadical_solver(true); });
+}
+
 TEST_CASE("simple_integer_programming_tests_minisat") {
 	IpToSatSolver solver(bind(minisat_solver, true));
 	solver.set_silent(true);
@@ -301,15 +305,17 @@ TEST_CASE("sat-constraints_coefs_larger_than_1") {
 	ip.add_constraint(4 * x - y - z >= 0);
 	REQUIRE(solve_minisat(&ip));
 
-	REQUIRE_NUM_SOLUTIONS(ip, []() { return minisat_solver(true); }, 5);
+	REQUIRE_NUM_SOLUTIONS(
+	    ip, []() { return minisat_solver(true); }, 5);
 }
 
 TEST_CASE("sat-constraints_coefs_zero") {
 	IP ip;
 	auto x = ip.add_boolean();
 	ip.add_constraint(0 * x >= 0);
 
-	REQUIRE_NUM_SOLUTIONS(ip, []() { return minisat_solver(true); }, 2);
+	REQUIRE_NUM_SOLUTIONS(
+	    ip, []() { return minisat_solver(true); }, 2);
 }
 
 TEST_CASE("sat-constraints_fractional_coeff-1") {
@@ -336,7 +342,8 @@ TEST_CASE("sat-constraints_coefs_less_than_minus_1") {
 	auto z = ip.add_boolean();
 	ip.add_constraint(8 * x - 2 * y - 2 * z >= 0);
 
-	REQUIRE_NUM_SOLUTIONS(ip, []() { return minisat_solver(true); }, 5);
+	REQUIRE_NUM_SOLUTIONS(
+	    ip, []() { return minisat_solver(true); }, 5);
 }
 
 TEST_CASE("sat-constraints_coefs_negative_multiple_times") {
@@ -346,7 +353,8 @@ TEST_CASE("sat-constraints_coefs_negative_multiple_times") {
 	auto z = ip.add_boolean();
 	ip.add_constraint(8 * x - y - y - z - z >= 0);
 
-	REQUIRE_NUM_SOLUTIONS(ip, []() { return minisat_solver(true); }, 5);
+	REQUIRE_NUM_SOLUTIONS(
+	    ip, []() { return minisat_solver(true); }, 5);
 }
 
 TEST_CASE("sat-negative-objective") {
@@ -376,7 +384,8 @@ TEST_CASE("sat-objective-next_solution") {
 	ip.add_objective(obj);
 	ip.add_constraint(x + y + z + w + u + v == 2);
 
-	REQUIRE_NUM_SOLUTIONS(ip, []() { return minisat_solver(true); }, 6);
+	REQUIRE_NUM_SOLUTIONS(
+	    ip, []() { return minisat_solver(true); }, 6);
 }
 
 TEST_CASE("add_min_consecutive_constraints-2-true") {
@@ -393,7 +402,8 @@ TEST_CASE("add_min_consecutive_constraints-2-true") {
 	// 1 1 0
 	// 0 1 1
 	// 1 0 1
-	REQUIRE_NUM_SOLUTIONS(ip, []() { return minisat_solver(true); }, 3);
+	REQUIRE_NUM_SOLUTIONS(
+	    ip, []() { return minisat_solver(true); }, 3);
 }
 
 TEST_CASE("add_min_max_consecutive_constraints-4") {

third-party/CMakeLists.txt

@@ -11,6 +11,7 @@ set(ABSL_STD_CXX_FLAG "" CACHE STRING "c++ std flag" FORCE)
 
 add_subdirectory(abseil-cpp)
 add_subdirectory(bliss)
+add_subdirectory(cadical)
 add_subdirectory(Catch)
 add_subdirectory(cleaneling)
 add_subdirectory(coin)

third-party/cadical/CMakeLists.txt

@@ -0,0 +1,25 @@
+add_definitions("-DNBUILD")
+if (MSVC)
+    add_definitions("-DNUNLOCKED")
+endif ()
+
+add_library(cadical
+cadical/analyze.cpp    cadical/decompose.cpp    cadical/minimize.cpp   cadical/signal.cpp
+cadical/arena.cpp      cadical/deduplicate.cpp  cadical/occs.cpp       cadical/solution.cpp
+cadical/assume.cpp     cadical/elim.cpp         cadical/options.cpp    cadical/solver.cpp
+cadical/averages.cpp   cadical/ema.cpp          cadical/parse.cpp      cadical/stats.cpp
+cadical/backtrack.cpp  cadical/extend.cpp       cadical/phases.cpp     cadical/subsume.cpp
+cadical/backward.cpp   cadical/external.cpp     cadical/probe.cpp      cadical/terminal.cpp
+cadical/bins.cpp       cadical/file.cpp         cadical/profile.cpp    cadical/ternary.cpp
+cadical/block.cpp      cadical/flags.cpp        cadical/proof.cpp      cadical/tracer.cpp
+cadical/ccadical.cpp   cadical/format.cpp       cadical/propagate.cpp  cadical/transred.cpp
+cadical/checker.cpp    cadical/gates.cpp        cadical/queue.cpp      cadical/util.cpp
+cadical/clause.cpp     cadical/instantiate.cpp  cadical/random.cpp     cadical/var.cpp
+cadical/collect.cpp    cadical/internal.cpp     cadical/reduce.cpp     cadical/version.cpp
+cadical/compact.cpp    cadical/ipasir.cpp       cadical/rephase.cpp    cadical/vivify.cpp
+cadical/condition.cpp  cadical/limit.cpp        cadical/report.cpp     cadical/walk.cpp
+cadical/config.cpp     cadical/logging.cpp      cadical/resources.cpp  cadical/watch.cpp
+cadical/contract.cpp   cadical/lookahead.cpp    cadical/restart.cpp
+cadical/cover.cpp      cadical/lucky.cpp        cadical/restore.cpp
+cadical/decide.cpp     cadical/message.cpp      cadical/score.cpp)
+

third-party/cadical/cadical/README.md

@@ -0,0 +1,12 @@
+This is the source code of the library `libcadical.a` with header
+`cadical.hpp`, the stand-alone solver `cadical` (in `cadical.cpp`) and the
+model based tester `mobical` (in `mobical.app`).
+
+The `configure` script and link to the `makefile` in the root directory
+can be used from within the `src` sub-directory too and then will just work
+as if used from the root directory.  For instance
+
+    ./configure && make test
+
+will configure and build in `../build` the default (optimizing)
+configuration and if successful then run the test suite.