Add support for MergeSat

MergeSat is a recent SAT solver that fits the MiniSat2 interface. Run
the check-ubuntu-20_04-cmake-gcc CI job with MergeSat to continuously
confirm that this configuration actually works.

To use MergeSat as a proper SAT backend, some extensions might be dropped.
Especially being able to print memory usage is not helpful for CBMC, but
requires pulling in a new dependency.

Signed-off-by: Norbert Manthey <[email protected]>

Author: conp-solutions

.github/workflows/pull-request-checks.yaml

@@ -222,7 +222,7 @@ jobs:
         run: |
           mkdir build
           cd build
-          cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++
+          cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl=mergesat
       - name: Check that doc task works
         run: |
           cd build

scripts/mergesat_CMakeLists.txt

@@ -0,0 +1,28 @@
+# CBMC only uses part of MergeSat.
+# This CMakeLists is designed to build just the parts that are needed.
+
+add_library(mergesat-condensed
+    minisat/core/Lookahead.cc
+    minisat/core/Solver.cc
+    minisat/simp/SimpSolver.cc
+    minisat/utils/ccnr.cc
+    minisat/utils/Options.cc
+    minisat/utils/System.cc
+)
+
+set_target_properties(
+    mergesat-condensed
+    PROPERTIES
+    CXX_STANDARD 11
+    CXX_STANDARD_REQUIRED true
+    XCODE_ATTRIBUTE_CODE_SIGN_IDENTITY "Developer ID Application: Daniel Kroening"
+)
+
+if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+    target_compile_options(mergesat-condensed PUBLIC /w)
+endif()
+
+target_include_directories(mergesat-condensed
+    PUBLIC
+    ${CMAKE_CURRENT_SOURCE_DIR}
+)

src/Makefile

@@ -139,6 +139,15 @@ minisat2-download:
 	@(cd ../minisat-2.2.1; patch -p1 < ../scripts/minisat-2.2.1-patch)
 	@rm minisat2_2.2.1.orig.tar.gz
 
+mergesat_version = 4.0-rc
+mergesat-download:
+	@echo "Downloading MergeSat $(mergesat_version)"
+	@$(DOWNLOADER) https://github.com/conp-solutions/mergesat/archive/$(mergesat_version).tar.gz
+	@$(TAR) xfz $(mergesat_version).tar.gz
+	@rm -Rf ../mergesat
+	@mv mergesat-$(mergesat_version) ../mergesat
+	@$(RM) $(mergesat_version).tar.gz
+
 cudd-download:
 	@echo "Downloading Cudd 3.0.0"
 	@$(DOWNLOADER) https://sourceforge.net/projects/cudd-mirror/files/cudd-3.0.0.tar.gz/download cudd-3.0.0.tar.gz

src/config.inc

@@ -30,12 +30,13 @@ endif
 #BOOLEFORCE = ../../booleforce-0.4
 #MINISAT = ../../MiniSat-p_v1.14
 #MINISAT2 = ../../minisat-2.2.1
+#MERGESAT = ../../mergesat-3.0
 #IPASIR = ../../ipasir
 #GLUCOSE = ../../glucose-syrup
 #CADICAL = ../../cadical
 
 # select default solver to be minisat2 if no other is specified
-ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(PICOSAT)$(CADICAL),)
+ifeq ($(BOOLEFORCE)$(CHAFF)$(GLUCOSE)$(IPASIR)$(LINGELING)$(MINISAT)$(MINISAT2)$(MERGESAT)$(PICOSAT)$(CADICAL),)
   MINISAT2 = ../../minisat-2.2.1
 endif
 
@@ -63,6 +64,10 @@ ifneq ($(MINISAT2),)
   CP_CXXFLAGS += -DSATCHECK_MINISAT2
 endif
 
+ifneq ($(MERGESAT),)
+  CP_CXXFLAGS += -DSATCHECK_MERGESAT
+endif
+
 ifneq ($(GLUCOSE),)
   CP_CXXFLAGS += -DSATCHECK_GLUCOSE
 endif

src/solvers/CMakeLists.txt

@@ -9,7 +9,7 @@ set(chaff_source
 set(minisat_source
     ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_minisat.cpp
 )
-set(minisat2_source
+set(minisat2_mergesat_source
     ${CMAKE_CURRENT_SOURCE_DIR}/sat/satcheck_minisat2.cpp
 )
 set(glucose_source
@@ -44,7 +44,7 @@ file(GLOB_RECURSE sources "*.cpp" "*.h")
 list(REMOVE_ITEM sources
     ${chaff_source}
     ${minisat_source}
-    ${minisat2_source}
+    ${minisat2_mergesat_source}
     ${glucose_source}
     ${squolem2_source}
     ${cudd_source}
@@ -78,9 +78,28 @@ if("${sat_impl}" STREQUAL "minisat2")
         SATCHECK_MINISAT2 HAVE_MINISAT2 __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS
     )
 
-    target_sources(solvers PRIVATE ${minisat2_source})
+    target_sources(solvers PRIVATE ${minisat2_mergesat_source})
 
     target_link_libraries(solvers minisat2-condensed)
+elseif("${sat_impl}" STREQUAL "mergesat")
+    message(STATUS "Building solvers with MergeSat")
+
+    download_project(PROJ mergesat
+        URL https://github.com/conp-solutions/mergesat/archive/4.0-rc.tar.gz
+        PATCH_COMMAND true
+        COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/mergesat_CMakeLists.txt CMakeLists.txt
+        URL_MD5 069c0d4f69723847055c3491cff5940e
+    )
+
+    add_subdirectory(${mergesat_SOURCE_DIR} ${mergesat_BINARY_DIR})
+
+    target_compile_definitions(solvers PUBLIC
+        SATCHECK_MERGESAT HAVE_MERGESAT __STDC_FORMAT_MACROS __STDC_LIMIT_MACROS
+    )
+
+    target_sources(solvers PRIVATE ${minisat2_mergesat_source})
+
+    target_link_libraries(solvers mergesat-condensed)
 elseif("${sat_impl}" STREQUAL "glucose")
     message(STATUS "Building solvers with glucose")
 

src/solvers/Makefile

@@ -22,6 +22,21 @@ ifneq ($(MINISAT2),)
   CLEANFILES += $(MINISAT2_LIB) $(patsubst %$(OBJEXT), %$(DEPEXT), $(MINISAT2_LIB))
 endif
 
+ifneq ($(MERGESAT),)
+  # MergeSat is based on MiniSat2 and is invoked (with suitable defines/ifdefs)
+  # via satcheck_minisat2.{h,cpp}
+  MERGESAT_SRC=sat/satcheck_minisat2.cpp
+  MERGESAT_INCLUDE=-I $(MERGESAT)
+  MERGESAT_LIB=$(MERGESAT)/minisat/core/Lookahead$(OBJEXT) \
+               $(MERGESAT)/minisat/core/Solver$(OBJEXT) \
+	             $(MERGESAT)/minisat/simp/SimpSolver$(OBJEXT) \
+               $(MERGESAT)/minisat/utils/ccnr$(OBJEXT) \
+               $(MERGESAT)/minisat/utils/Options$(OBJEXT) \
+               $(MERGESAT)/minisat/utils/System$(OBJEXT)
+  CP_CXXFLAGS += -DHAVE_MERGESAT -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
+  CLEANFILES += $(MERGESAT_LIB) $(patsubst %$(OBJEXT), %$(DEPEXT), $(MERGESAT_LIB))
+endif
+
 ifneq ($(IPASIR),)
   IPASIR_SRC=sat/satcheck_ipasir.cpp
   IPASIR_INCLUDE=-I $(IPASIR)
@@ -74,6 +89,7 @@ SRC = $(BOOLEFORCE_SRC) \
       $(GLUCOSE_SRC) \
       $(LINGELING_SRC) \
       $(MINISAT2_SRC) \
+      $(MERGESAT_SRC) \
       $(IPASIR_SRC) \
       $(MINISAT_SRC) \
       $(PICOSAT_SRC) \
@@ -227,6 +243,31 @@ $(MINISAT2)/minisat/core/Solver$(OBJEXT): $(MINISAT2)/minisat/core/Solver.cc
 endif
 endif
 
+ifneq ($(MERGESAT),)
+ifeq ($(BUILD_ENV_),MSVC)
+sat/satcheck_minisat2$(OBJEXT): sat/satcheck_minisat2.cpp
+	$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@
+
+$(MERGESAT)/minisat/core/Lookahead$(OBJEXT): $(MERGESAT)/minisat/core/Lookahead.cc
+	$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@
+
+$(MERGESAT)/minisat/core/Solver$(OBJEXT): $(MERGESAT)/minisat/core/Solver.cc
+	$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@
+
+$(MERGESAT)/minisat/simp/SimpSolver$(OBJEXT): $(MERGESAT)/minisat/simp/SimpSolver.cc
+	$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@
+
+$(MERGESAT)/minisat/utils/ccnr$(OBJEXT): $(MERGESAT)/minisat/utils/ccnr.cc
+	$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@
+
+$(MERGESAT)/minisat/utils/Options$(OBJEXT): $(MERGESAT)/minisat/utils/Options.cc
+	$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@
+
+$(MERGESAT)/minisat/utils/System$(OBJEXT): $(MERGESAT)/minisat/utils/System.cc
+	$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@
+endif
+endif
+
 ifneq ($(GLUCOSE),)
 ifeq ($(BUILD_ENV_),MSVC)
 sat/satcheck_glucose$(OBJEXT): sat/satcheck_glucose.cpp
@@ -242,6 +283,7 @@ endif
 
 INCLUDES += -I .. \
   $(CHAFF_INCLUDE) $(BOOLEFORCE_INCLUDE) $(MINISAT_INCLUDE) $(MINISAT2_INCLUDE) \
+  $(MERGESAT_INCLUDE) \
   $(IPASIR_INCLUDE) \
   $(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \
 	$(PICOSAT_INCLUDE) $(LINGELING_INCLUDE) $(CADICAL_INCLUDE)
@@ -260,7 +302,7 @@ endif
 endif
 
 SOLVER_LIB = $(CHAFF_LIB) $(BOOLEFORCE_LIB) $(MINISAT_LIB) \
-        $(MINISAT2_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \
+        $(MINISAT2_LIB) $(MERGESAT_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \
         $(PICOSAT_LIB) $(LINGELING_LIB) $(GLUCOSE_LIB) $(CADICAL_LIB)
 
 SOLVER_OBJS = $(filter %$(OBJEXT), $(SOLVER_LIB))

src/solvers/sat/satcheck.h

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 // #define SATCHECK_ZCHAFF
 // #define SATCHECK_MINISAT1
 // #define SATCHECK_MINISAT2
+// #define SATCHECK_MERGESAT
 // #define SATCHECK_GLUCOSE
 // #define SATCHECK_BOOLEFORCE
 // #define SATCHECK_PICOSAT
@@ -39,6 +40,10 @@ Author: Daniel Kroening, [email protected]
 #define SATCHECK_MINISAT2
 #endif
 
+#if defined(HAVE_MERGESAT) && !defined(SATCHECK_MERGESAT)
+#  define SATCHECK_MERGESAT
+#endif
+
 #if defined(HAVE_GLUCOSE) && !defined(SATCHECK_GLUCOSE)
 #define SATCHECK_GLUCOSE
 #endif
@@ -80,9 +85,11 @@ typedef satcheck_booleforcet satcheck_no_simplifiert;
 typedef satcheck_minisat1t satcheckt;
 typedef satcheck_minisat1t satcheck_no_simplifiert;
 
-#elif defined SATCHECK_MINISAT2
+#elif defined SATCHECK_MINISAT2 || defined SATCHECK_MERGESAT
+// MergeSat is based on MiniSat2 and is invoked (with suitable defines/ifdefs)
+// via satcheck_minisat2.{h,cpp}
 
-#include "satcheck_minisat2.h"
+#  include "satcheck_minisat2.h"
 
 typedef satcheck_minisat_simplifiert satcheckt;
 typedef satcheck_minisat_no_simplifiert satcheck_no_simplifiert;

src/solvers/sat/satcheck_minisat2.cpp

@@ -13,17 +13,20 @@ Author: Daniel Kroening, [email protected]
 #  include <unistd.h>
 #endif
 
-#include <limits>
-
 #include <util/invariant.h>
 #include <util/make_unique.h>
 #include <util/threeval.h>
 
 #include <minisat/core/Solver.h>
 #include <minisat/simp/SimpSolver.h>
 
-#ifndef HAVE_MINISAT2
-#error "Expected HAVE_MINISAT2"
+#include <cstdlib>
+#include <limits>
+
+// MergeSat is based on MiniSat2; variations in their API are handled via
+// #ifdefs
+#if !defined(HAVE_MINISAT2) && !defined(HAVE_MERGESAT)
+#  error "Expected HAVE_MINISAT2 or HAVE_MERGESAT"
 #endif
 
 void convert(const bvt &bv, Minisat::vec<Minisat::Lit> &dest)
@@ -77,7 +80,11 @@ void satcheck_minisat2_baset<T>::set_polarity(literalt a, bool value)
   try
   {
     add_variables();
+#ifdef HAVE_MERGESAT
+    solver->setPolarity(a.var_no(), value);
+#else
     solver->setPolarity(a.var_no(), value ? l_True : l_False);
+#endif
   }
   catch(Minisat::OutOfMemoryException)
   {
@@ -101,12 +108,20 @@ void satcheck_minisat2_baset<T>::clear_interrupt()
 
 const std::string satcheck_minisat_no_simplifiert::solver_text()
 {
+#ifdef HAVE_MERGESAT
+  return "MergeSat 4.0-rc without simplifier";
+#else
   return "MiniSAT 2.2.1 without simplifier";
+#endif
 }
 
 const std::string satcheck_minisat_simplifiert::solver_text()
 {
+#ifdef HAVE_MERGESAT
+  return "MergeSat 4.0-rc with simplifier";
+#else
   return "MiniSAT 2.2.1 with simplifier";
+#endif
 }
 
 template<typename T>
@@ -257,6 +272,14 @@ propt::resultt satcheck_minisat2_baset<T>::do_prop_solve()
 
 #endif
 
+#ifdef HAVE_MERGESAT
+    // We do not actually use MergeSat's "constrain" clauses at the moment, but
+    // MergeSat internally still uses them to track UNSAT. To make sure we
+    // aren't stuck with "UNSAT" in incremental calls the status needs to be
+    // reset.
+    ((Minisat::Solver *)solver.get())->reset_constrain_clause();
+#endif
+
     if(solver_result == l_True)
     {
       log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom;
@@ -314,6 +337,15 @@ satcheck_minisat2_baset<T>::satcheck_minisat2_baset(
     solver(util_make_unique<T>()),
     time_limit_seconds(0)
 {
+#ifdef HAVE_MERGESAT
+  if constexpr(std::is_same<T, Minisat::SimpSolver>::value)
+  {
+    solver->grow_iterations = false;
+    // limit the amount of work spent in simplification; the optimal value needs
+    // to be found via benchmarking
+    solver->nr_max_simp_cls = 1000000;
+  }
+#endif
 }
 
 template <typename T>