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

@@ -219,7 +219,7 @@ jobs:
         env:
           # This is needed in addition to -yq to prevent apt-get from asking for
           # user input
-          DEBIAN_FRONTEND: noninteractive
+          DEBIAN_FRONTEND: nonint eractive
         run: |
           sudo apt-get update
           sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen graphviz z3
@@ -275,6 +275,61 @@ jobs:
             exit 1
           fi
 
+  # This job takes approximately 29 to 42 minutes
+  check-ubuntu-24_04-cmake-gcc-mergesat:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Fetch dependencies
+        env:
+          # This is needed in addition to -yq to prevent apt-get from asking for
+          # user input
+          DEBIAN_FRONTEND: noninteractive
+        run: |
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen z3
+      - name: Confirm z3 solver is available and log the version installed
+        run: z3 --version
+      - name: Download cvc-5 from the releases page and make sure it can be deployed
+        run: |
+          wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip
+          unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5
+          rm cvc5-Linux-x86_64-static.zip
+          cvc5 --version
+      - name: Prepare ccache
+        uses: actions/cache@v4
+        with:
+          path: .ccache
+          key: ${{ runner.os }}-24.04-Release-mergesat-${{ github.ref }}-${{ github.sha }}-PR
+          restore-keys: |
+            ${{ runner.os }}-24.04-Release-mergesat-${{ github.ref }}
+            ${{ runner.os }}-24.04-Release-mergesat
+      - name: ccache environment
+        run: |
+          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
+          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Configure using CMake
+        run: cmake -S . -B build -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="mergesat;cadical"
+      - name: Check that doc task works
+        run: ninja -C build doc
+      - name: Zero ccache stats and limit in size
+        run: ccache -z --max-size=500M
+      - name: Build with Ninja
+        run: ninja -C build -j${{env.linux-vcpus}}
+      - name: Print ccache stats
+        run: ccache -s
+      - name: Checking completeness of help output
+        run: scripts/check_help.sh /usr/bin/g++ build/bin
+      - name: Check if package building works
+        run: |
+          cd build
+          ninja package
+          ls *.deb
+      - name: Run tests
+        run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}}
+
   # This job takes approximately 20 to 38 minutes
   check-ubuntu-22_04-make-clang:
     runs-on: ubuntu-22.04

scripts/mergesat_CMakeLists.txt

@@ -0,0 +1,29 @@
+# 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 17
+    CXX_STANDARD_REQUIRED true
+    CXX_EXTENSIONS OFF
+    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

@@ -166,6 +166,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 = docker-solvers
+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

@@ -33,12 +33,13 @@ endif
 #BOOLEFORCE = ../../booleforce-0.4
 #MINISAT = ../../MiniSat-p_v1.14
 #MINISAT2 = ../../minisat-2.2.1
+#MERGESAT = ../../mergesat-4.0-rc1
 #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
 

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}
@@ -81,7 +81,7 @@ foreach(SOLVER ${sat_impl})
             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("${SOLVER}" STREQUAL "system-minisat2")
@@ -98,6 +98,25 @@ foreach(SOLVER ${sat_impl})
         else()
             message(FATAL_ERROR "Unable to find header file for preinstalled minisat2")
         endif()
+      elseif("${SOLVER}" STREQUAL "mergesat")
+        message(STATUS "Building solvers with MergeSat")
+
+        download_project(PROJ mergesat
+            URL https://github.com/conp-solutions/mergesat/archive/docker-solvers.tar.gz
+            PATCH_COMMAND true
+            COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/mergesat_CMakeLists.txt CMakeLists.txt
+            URL_MD5 1cef063f3255e86beef91f3cdd2eefb7
+        )
+
+        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("${SOLVER}" 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)
@@ -75,6 +90,7 @@ SRC = $(BOOLEFORCE_SRC) \
       $(GLUCOSE_SRC) \
       $(LINGELING_SRC) \
       $(MINISAT2_SRC) \
+      $(MERGESAT_SRC) \
       $(IPASIR_SRC) \
       $(MINISAT_SRC) \
       $(PICOSAT_SRC) \
@@ -234,6 +250,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
@@ -249,6 +290,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)
@@ -267,7 +309,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
@@ -71,7 +76,7 @@ Author: Daniel Kroening, [email protected]
 #  include "satcheck_minisat.h"
 #endif
 
-#if defined SATCHECK_MINISAT2
+#if defined(SATCHECK_MINISAT2) || defined(SATCHECK_MERGESAT)
 #  include "satcheck_minisat2.h"
 #endif
 
@@ -110,7 +115,9 @@ 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}
 
 typedef satcheck_minisat_simplifiert satcheckt;
 typedef satcheck_minisat_no_simplifiert satcheck_no_simplifiert;

src/solvers/sat/satcheck_minisat2.cpp

@@ -13,21 +13,24 @@ Author: Daniel Kroening, [email protected]
 #  include <unistd.h>
 #endif
 
-#include <limits>
-
 #include <util/invariant.h>
 #include <util/threeval.h>
 
 #include <minisat/core/Solver.h>
 #include <minisat/simp/SimpSolver.h>
 
+#include <cstdlib>
+#include <limits>
+
 #ifndef l_False
 #  define l_False Minisat::l_False
 #  define l_True Minisat::l_True
 #endif
 
-#ifndef HAVE_MINISAT2
-#error "Expected HAVE_MINISAT2"
+// 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)
@@ -95,7 +98,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)
   {
@@ -119,12 +126,20 @@ void satcheck_minisat2_baset<T>::clear_interrupt()
 
 std::string satcheck_minisat_no_simplifiert::solver_text() const
 {
+#ifdef HAVE_MERGESAT
+  return "MergeSat 4.0-rc without simplifier";
+#else
   return "MiniSAT 2.2.1 without simplifier";
+#endif
 }
 
 std::string satcheck_minisat_simplifiert::solver_text() const
 {
+#ifdef HAVE_MERGESAT
+  return "MergeSat 4.0-rc4 with simplifier";
+#else
   return "MiniSAT 2.2.1 with simplifier";
+#endif
 }
 
 template<typename T>
@@ -275,6 +290,15 @@ propt::resultt satcheck_minisat2_baset<T>::do_prop_solve(const bvt &assumptions)
 
 #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.
+    // See also https://github.com/conp-solutions/mergesat/pull/124
+    ((Minisat::Solver *)solver.get())->reset_constrain_clause();
+#endif
+
     if(solver_result == l_True)
     {
       log.status() << "SAT checker: instance is SATISFIABLE" << messaget::eom;
@@ -332,6 +356,15 @@ satcheck_minisat2_baset<T>::satcheck_minisat2_baset(
     solver(std::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>