Rfc sat backend mergesat #6088

conp-solutions · 2021-05-06T20:16:28Z

This is a RFC patch to investigate whether moving the SAT backend to a more recent solver would be beneficial. This patch set is scappy. In case the integration of the new solver results in performance benefits, required changes could be worked into the used MergeSat solver, and this patch series could be cleaned up.

I am not aware how the performance of the SAT backend can be tested. Please advice. Thanks!

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

TGWDB · 2021-05-07T08:11:29Z

CMakeLists.txt

@@ -62,7 +62,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
    set(CMAKE_CXX_FLAGS_RELEASE "-O2")
    set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g")
    #   Enable lots of warnings
-    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Werror -Wno-deprecated-declarations -Wswitch-enum")
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wpedantic -Wno-deprecated-declarations -Wswitch-enum")


The policy of the current build is to error on warnings, this should probably be discussed independently of other PRs. If this is required for this PR to work, I would recommend explaining why the warnings cannot be avoided.

TGWDB · 2021-05-07T08:14:55Z

src/Makefile

+	@echo "Downloading MergeSat (replacing Minisat 2.2.1)"
 	@for i in $$(seq 1 3) ; do \
 	  $(DOWNLOADER) \
-	    http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz && \
+	    https://github.com/conp-solutions/mergesat/archive/refs/tags/v3.0.tar.gz && \
 	    exit 0 ; \
-		$(RM) minisat2_2.2.1.orig.tar.gz ; \
+		$(RM) v3.0.tar.gz ; \
 	  if [ $$i -lt 3 ] ; then echo "Re-trying in 10 seconds" 1>&2 ; sleep 10 ; fi ; \
 	done ; exit 1
-	@$(TAR) xfz minisat2_2.2.1.orig.tar.gz
+	@$(TAR) xfz v3.0.tar.gz # will create mergesat-3.0
 	@rm -Rf ../minisat-2.2.1
-	@mv minisat2-2.2.1 ../minisat-2.2.1
-	@(cd ../minisat-2.2.1; patch -p1 < ../scripts/minisat-2.2.1-patch)
-	@rm minisat2_2.2.1.orig.tar.gz
+	@mv mergesat-3.0 ../minisat-2.2.1
+	@rm v3.0.tar.gz


This appears to be editing and replacing the current MiniSAT build process. I would much prefer to see a new build path for MergeSat (like the ones for CaDiCaL or glucose) and then if this has much improved performance we can simply change the default. Also see recent PRs for documenting and updating alternative build systems (e.g. #6075 #6047).

Yes; absolutely.

TGWDB · 2021-05-07T08:15:14Z

src/config.inc

@@ -5,7 +5,7 @@ BUILD_ENV = AUTO
 ifeq ($(BUILD_ENV),MSVC)
  #CXXFLAGS += /Wall /WX
 else
-  CXXFLAGS += -Wall -pedantic -Werror -Wno-deprecated-declarations -Wswitch-enum
+  CXXFLAGS += -Wall -pedantic -Wno-deprecated-declarations -Wswitch-enum


Again, this should be separate.

TGWDB · 2021-05-07T08:15:43Z

src/solvers/Makefile

@@ -17,7 +17,7 @@ endif
 ifneq ($(MINISAT2),)
  MINISAT2_SRC=sat/satcheck_minisat2.cpp
  MINISAT2_INCLUDE=-I $(MINISAT2)
-  MINISAT2_LIB=$(MINISAT2)/minisat/simp/SimpSolver$(OBJEXT) $(MINISAT2)/minisat/core/Solver$(OBJEXT)
+  MINISAT2_LIB=$(MINISAT2)/minisat/simp/SimpSolver$(OBJEXT) $(MINISAT2)/minisat/core/Solver$(OBJEXT) $(MINISAT2)/minisat/utils/ccnr$(OBJEXT) $(MINISAT2)/minisat/utils/Options$(OBJEXT) $(MINISAT2)/minisat/utils/System$(OBJEXT)


Again, editing the MiniSAT and not providing a new option.

TGWDB · 2021-05-07T08:15:55Z

src/solvers/Makefile

+$(MINISAT2)/minisat/utils/ccnr$(OBJEXT): $(MINISAT2)/minisat/utils/ccnr.cc
+	$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@
+
+$(MINISAT2)/minisat/utils/Options$(OBJEXT): $(MINISAT2)/minisat/utils/Options.cc
+	$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@
+
+$(MINISAT2)/minisat/utils/System$(OBJEXT): $(MINISAT2)/minisat/utils/System.cc
+	$(CXX) $(CP_CXXFLAGS) /w /nologo /c /EHsc $< /Fo$@
+


Again, editing.

conp-solutions · 2021-05-07T19:51:34Z

Thanks for the comments. I fully understand that I should create a separate back-end. I can happily to so, in case the performance of the proposed SAT back-end exceeds the performance of the current one.

This PR is an RFC. In case we decide to move forward, I will address all the comments. I could adapt MergeSat so that dropping "-Werror" is not required any more (or provide a CBMC local patch as is done for other solvers).

Until then, I would love to understand whether there is an agreed way to measure the performance of a new back-end. Thanks!

To be able to build less quality code, allow compilation warnings. This is only meant as a helper step to allow test new SAT backends. Signed-off-by: Norbert Manthey <[email protected]>

MergeSat is a recent SAT solver that fits the MiniSat interface. This change uses MergeSat in place of Minisat2. For this test, no deep changes are performed. Besides replacing the package to be downloaded, the required build dependencies are adapted. 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]>

MergeSat is based on the MiniSat 2.2 interface. Hence, setPolarity needs a bool instead of an lbool. Signed-off-by: Norbert Manthey <[email protected]>

TGWDB · 2021-05-10T09:44:01Z

Thanks for the comments. I fully understand that I should create a separate back-end. I can happily to so, in case the performance of the proposed SAT back-end exceeds the performance of the current one.

This PR is an RFC. In case we decide to move forward, I will address all the comments. I could adapt MergeSat so that dropping "-Werror" is not required any more (or provide a CBMC local patch as is done for other solvers).

Great.

Until then, I would love to understand whether there is an agreed way to measure the performance of a new back-end. Thanks!

Recent performance work has explored some different benchmarks including: full runs on regression tests, runs over open source repositories (with cbmc validation checks), and clear test examples. An example of a PR with some performance data can be found here: #5964

martin-cs · 2021-05-10T16:43:44Z

@tautschnig has probably the best scripting for doing large scale performance evaluation. But I think this might be a little bit of a red herring.

There are already a number of back-ends that often have better performance than the default one. However MiniSAT remains the default because:

It's simple and requires little external dependency.
Its performance is remarkably consistent and scales predictably.

So, patches adding new solvers (SAT, SMT, others) are most welcome and should be merged eagerly. Changing the default is going to require a lot of benchmarking, including against the SMT solvers and a lot of time to see if there are performance regression in actual applications.

PS Is the IPASIR format still a going concern? That might be an easier route to integrate new solvers.

tautschnig · 2021-05-14T09:25:54Z

Here are results for two of the categories of SV-COMP, with Mergesat on the x axis of the scatter plots, and Minisat on the y axis. As can be seen, the results vary in both directions. On other categories the results are more consistent in that Mergesat is about 10% slower, but that slowdown does not affect overall scores. Hence, no clear-cut "solver X is uniformly better," which probably is the expected result anyway.

What is much better about Mergesat, of course, is that it is maintained :-)

TGWDB · 2021-05-26T12:37:16Z

@conp-solutions Just checking in to see where you are with this PR/RFC.

conp-solutions · 2021-05-26T13:00:16Z

Feel free to close this PR. I will likely follow up with a proper new SAT backend in the future, but cannot give a strict date (i should manage to iterate within the next month.

TGWDB · 2021-05-26T13:12:56Z

Closing as recommended by opening author. Look forward to the new SAT back end in the future.

conp-solutions requested review from chrisr-diffblue, kroening, peterschrammel, smowton, tautschnig and a team as code owners May 6, 2021 20:16

conp-solutions requested a review from martin-cs as a code owner May 6, 2021 20:37

TGWDB reviewed May 7, 2021

View reviewed changes

TGWDB requested changes May 7, 2021

View reviewed changes

conp-solutions added 3 commits May 7, 2021 21:51

build: drop Werror

2e6ca86

To be able to build less quality code, allow compilation warnings. This is only meant as a helper step to allow test new SAT backends. Signed-off-by: Norbert Manthey <[email protected]>

sat,solvers: adapt setPolarity for MergeSat

8d60dae

MergeSat is based on the MiniSat 2.2 interface. Hence, setPolarity needs a bool instead of an lbool. Signed-off-by: Norbert Manthey <[email protected]>

conp-solutions force-pushed the rfc-sat-backend-mergesat branch from e4b1bde to 8d60dae Compare May 7, 2021 19:52

tautschnig assigned tautschnig and conp-solutions May 11, 2021

tautschnig removed their assignment May 14, 2021

TGWDB closed this May 26, 2021

TGWDB mentioned this pull request Jun 9, 2021

Conps minisat [blocks: #3243] #3282

Closed

6 tasks

tautschnig mentioned this pull request Nov 4, 2021

Add support for MergeSat #6439

Open

4 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Rfc sat backend mergesat #6088

Rfc sat backend mergesat #6088

conp-solutions commented May 6, 2021

TGWDB May 7, 2021

TGWDB May 7, 2021

martin-cs May 10, 2021

TGWDB May 7, 2021

TGWDB May 7, 2021

TGWDB May 7, 2021

conp-solutions commented May 7, 2021

TGWDB commented May 10, 2021

martin-cs commented May 10, 2021

tautschnig commented May 14, 2021

TGWDB commented May 26, 2021

conp-solutions commented May 26, 2021 via email

TGWDB commented May 26, 2021

Rfc sat backend mergesat #6088

Rfc sat backend mergesat #6088

Conversation

conp-solutions commented May 6, 2021

TGWDB May 7, 2021

Choose a reason for hiding this comment

TGWDB May 7, 2021

Choose a reason for hiding this comment

martin-cs May 10, 2021

Choose a reason for hiding this comment

TGWDB May 7, 2021

Choose a reason for hiding this comment

TGWDB May 7, 2021

Choose a reason for hiding this comment

TGWDB May 7, 2021

Choose a reason for hiding this comment

conp-solutions commented May 7, 2021

TGWDB commented May 10, 2021

martin-cs commented May 10, 2021

tautschnig commented May 14, 2021

TGWDB commented May 26, 2021

conp-solutions commented May 26, 2021 via email

TGWDB commented May 26, 2021