Add support for MergeSat #6439

tautschnig · 2021-11-04T10:27:37Z

Adds support for MergeSat.

Each commit message has a non-empty body, explaining why the change was made.
n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a 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.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

codecov · 2021-11-04T11:39:39Z

Codecov Report

All modified and coverable lines are covered by tests ✅

Comparison is base (52688d7) 79.09% compared to head (eb291f9) 79.09%.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #6439   +/-   ##
========================================
  Coverage    79.09%   79.09%           
========================================
  Files         1701     1701           
  Lines       196625   196625           
========================================
  Hits        155527   155527           
  Misses       41098    41098

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

kroening · 2021-11-04T13:10:57Z

I believe this is the only solver that uses the minisat identifiers (that isn't minisat). I may be worth adding some comments to make that apparent.

tautschnig · 2021-11-04T13:14:36Z

I believe this is the only solver that uses the minisat identifiers (that isn't minisat). I may be worth adding some comments to make that apparent.

Yes, good call! Where would you see the most natural place to find such comments (as a developer)?

martin-cs

In principle I don't see a problem.

src/solvers/sat/satcheck_minisat2.cpp

scripts/mergesat.patch

nmanthey · 2021-11-05T06:59:34Z

Thanks for picking this up. Let me know if there is anything on the SAT side to look at (except your PR)

src/solvers/Makefile

src/solvers/sat/satcheck.h

src/solvers/sat/satcheck_minisat2.cpp

tautschnig · 2022-04-26T12:41:37Z

IIUC, this variable needs to be set before the solver object is created. Have you checked whether this setting is actually passed through to the solver?

It might be simpler to always start from the SimpSolver object, and set the "use_simplification" parameter right after constructing the object, to indicate whether you want to have simplification or not. Then, you can also set the member behind the option you use in setenv, as this is always available as well. That would be member 'grow_iterations'

Done with minimal modifications, which, however, requires C++17. So I've added commits from #6749 to make this work (there's a CI job using MergeSat now).

tautschnig · 2022-04-26T12:44:39Z

nit: version "3.0" is not true

Is that still mentioned anywhere?

tautschnig · 2022-04-26T12:45:00Z

nit: Is this configuration actually tested on Windows? I did not test this myself, and know for earlier versions that this compilation does not work without modifications to MergeSat.

I've added MergeSat to the check-vs-2019-cmake-build-and-test CI job. Let's see!

tautschnig · 2022-04-26T14:16:32Z

nit: Is this configuration actually tested on Windows? I did not test this myself, and know for earlier versions that this compilation does not work without modifications to MergeSat.

I've added MergeSat to the check-vs-2019-cmake-build-and-test CI job. Let's see!

Does not seem to work:

D:\a\cbmc\cbmc\build\mergesat-src\minisat\core\Lookahead.cc(20,10): fatal error C1083: Cannot open include file: 'core/Lookahead.h': No such file or directory [D:\a\cbmc\cbmc\build\mergesat-build\mergesat-condensed.vcxproj]
cl : command line warning D9025: overriding '/W3' with '/w' [D:\a\cbmc\cbmc\build\mergesat-build\mergesat-condensed.vcxproj]
cl : Command line warning D9025: overriding '/W3' with '/w' [D:\a\cbmc\cbmc\build\mergesat-build\mergesat-condensed.vcxproj]
  Solver.cc
D:\a\cbmc\cbmc\build\mergesat-src\minisat\core\Solver.cc(50,10): fatal error C1083: Cannot open include file: 'unistd.h': No such file or directory

I'll limit the experimenting to Linux-based platforms, but even then the uses from within refinement appear to be causing trouble. Needs looking at.

Tests: do not unnecessarily constrain what models solvers can produce [blocks: #6439]

tautschnig · 2022-05-11T09:53:51Z

Note to self: We'll likely want conp-solutions/mergesat#124 to be merged and Mergesat 4.0 to be released before trying to merge this one.

conp-solutions · 2022-05-14T12:04:24Z

src/solvers/sat/satcheck_minisat2.cpp

+    // 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();


This is not required anymore. There was an issue with how incremental solving was implemented. The latest update of MergeSat has that fixed. Hence, feel free to drop this hunk!

Thank you! I don't think we want to merge this PR before MergeSat 4.0 is released, so I suppose 4.0 will include this fix?

Likely yes. On the other hand, I am not sure when I will release 4.0, i.. whether I wait for the SAT competition results or not. Hence, feel free to not wait. The major thing that will change is the default configuration of the solver - and the competition will help to identify which one to pick.

TGWDB · 2023-11-14T22:18:16Z

The runtime for the new CI job looks unpleasantly long. Is this expected? It seems well outside the numbers on the job description.

tautschnig · 2023-11-14T22:23:42Z

The runtime for the new CI job looks unpleasantly long. Is this expected? It seems well outside the numbers on the job description.

We might take this as a first performance indicator (the tests taking 54 minutes as compared to 18 minutes that MiniSat takes). Perhaps the switch from 4.0-rc1 to 4.0-rc4 (of mergesat) wasn't a good idea?!

TGWDB · 2023-11-20T09:45:33Z

The runtime for the new CI job looks unpleasantly long. Is this expected? It seems well outside the numbers on the job description.

We might take this as a first performance indicator (the tests taking 54 minutes as compared to 18 minutes that MiniSat takes). Perhaps the switch from 4.0-rc1 to 4.0-rc4 (of mergesat) wasn't a good idea?!

Yes. Without further knowledge/detail as to why (and whether it's an edge case we can accept), merging this seems like a bad idea.

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]>

tautschnig force-pushed the mergesat branch 3 times, most recently from 8668397 to ee3fd8c Compare November 4, 2021 12:45

martin-cs mentioned this pull request Nov 4, 2021

Parallelize DIMACS formula printing #6431

Open

7 tasks

martin-cs approved these changes Nov 4, 2021

View reviewed changes

src/solvers/sat/satcheck_minisat2.cpp Outdated Show resolved Hide resolved

scripts/mergesat.patch Outdated Show resolved Hide resolved

kroening reviewed Nov 5, 2021

View reviewed changes

src/solvers/Makefile Show resolved Hide resolved

kroening reviewed Nov 5, 2021

View reviewed changes

src/solvers/sat/satcheck.h Show resolved Hide resolved

kroening reviewed Nov 5, 2021

View reviewed changes

src/solvers/sat/satcheck_minisat2.cpp Show resolved Hide resolved

tautschnig self-assigned this Nov 17, 2021

tautschnig force-pushed the mergesat branch 2 times, most recently from c1d9942 to 74411eb Compare April 26, 2022 12:40

tautschnig force-pushed the mergesat branch from 74411eb to 8ad9e4a Compare April 26, 2022 12:44

tautschnig force-pushed the mergesat branch from 8ad9e4a to 8713425 Compare April 26, 2022 14:15

tautschnig force-pushed the mergesat branch from 8713425 to fd4705d Compare May 10, 2022 22:31

tautschnig mentioned this pull request May 10, 2022

Tests: do not unnecessarily constrain what models solvers can produce [blocks: #6439] #6849

Merged

3 tasks

tautschnig added the dependent - do not merge label May 10, 2022

tautschnig changed the title ~~Add support for MergeSat~~ Add support for MergeSat [depends-on: #6749, #6848, #6849] May 10, 2022

tautschnig force-pushed the mergesat branch from fd4705d to 0f8c0b0 Compare May 10, 2022 22:39

tautschnig changed the title ~~Add support for MergeSat [depends-on: #6749, #6848, #6849]~~ Add support for MergeSat [depends-on: #6749, #6849] May 10, 2022

tautschnig changed the title ~~Add support for MergeSat [depends-on: #6749, #6849]~~ Add support for MergeSat [depends-on: #6749] May 10, 2022

tautschnig added a commit that referenced this pull request May 11, 2022

Merge pull request #6849 from tautschnig/cleanup/solver-indep-tests

5c974cc

Tests: do not unnecessarily constrain what models solvers can produce [blocks: #6439]

tautschnig mentioned this pull request May 11, 2022

Make SimpSolver::reset_constrain_clause public conp-solutions/mergesat#124

Merged

conp-solutions reviewed May 14, 2022

View reviewed changes

tautschnig mentioned this pull request Jul 22, 2022

Avoid redundant variables and clauses in the propositional encoding #7001

Draft

4 tasks

tautschnig force-pushed the mergesat branch 6 times, most recently from 58e83d6 to 2156312 Compare March 1, 2023 09:42

tautschnig force-pushed the mergesat branch from 2156312 to d297de1 Compare November 13, 2023 16:07

tautschnig changed the title ~~Add support for MergeSat [depends-on: #6749]~~ Add support for MergeSat Nov 13, 2023

tautschnig force-pushed the mergesat branch from d297de1 to 705959e Compare November 14, 2023 13:15

tautschnig removed the dependent - do not merge label Nov 14, 2023

tautschnig removed their assignment Nov 14, 2023

tautschnig marked this pull request as ready for review November 14, 2023 14:57

tautschnig requested review from a team, peterschrammel, thomasspriggs, NlightNFotis, TGWDB and esteffin as code owners November 14, 2023 14:57

tautschnig assigned TGWDB Nov 14, 2023

tautschnig self-assigned this Nov 14, 2023

tautschnig force-pushed the mergesat branch from 705959e to eb291f9 Compare November 23, 2023 10:50

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add support for MergeSat #6439

Add support for MergeSat #6439

tautschnig commented Nov 4, 2021 •

edited

Loading

codecov bot commented Nov 4, 2021 •

edited

Loading

kroening commented Nov 4, 2021

tautschnig commented Nov 4, 2021

martin-cs left a comment

nmanthey commented Nov 5, 2021

tautschnig commented Apr 26, 2022

tautschnig commented Apr 26, 2022

tautschnig commented Apr 26, 2022

tautschnig commented Apr 26, 2022

tautschnig commented May 11, 2022

conp-solutions May 14, 2022

tautschnig May 14, 2022

conp-solutions May 14, 2022

TGWDB commented Nov 14, 2023

tautschnig commented Nov 14, 2023

TGWDB commented Nov 20, 2023

Add support for MergeSat #6439

Are you sure you want to change the base?

Add support for MergeSat #6439

Conversation

tautschnig commented Nov 4, 2021 • edited Loading

codecov bot commented Nov 4, 2021 • edited Loading

Codecov Report

kroening commented Nov 4, 2021

tautschnig commented Nov 4, 2021

martin-cs left a comment

Choose a reason for hiding this comment

nmanthey commented Nov 5, 2021

tautschnig commented Apr 26, 2022

tautschnig commented Apr 26, 2022

tautschnig commented Apr 26, 2022

tautschnig commented Apr 26, 2022

tautschnig commented May 11, 2022

conp-solutions May 14, 2022

Choose a reason for hiding this comment

tautschnig May 14, 2022

Choose a reason for hiding this comment

conp-solutions May 14, 2022

Choose a reason for hiding this comment

TGWDB commented Nov 14, 2023

tautschnig commented Nov 14, 2023

TGWDB commented Nov 20, 2023

tautschnig commented Nov 4, 2021 •

edited

Loading

codecov bot commented Nov 4, 2021 •

edited

Loading