|
|
|---|
|
|
|
|---|
How to get a SAT solver that you can use with satlink.
To use Satlink you will need at least one SAT solver. Below are some solvers that are known to work well with Satlink. You may wish to install several of these. This lets you switch between solvers to figure out which solver is best for your particular problem, and perhaps to gain some additional confidence that a particular problem really is unsatisfiable (by checking it with many solvers.)
Special recommendations are for Glucose (no longer the most modern or highest-performing, but adequate and needed for certifying certain ACL2 community books) and Kissat (as of 2020, the best-performing free/open-source solver).
Based on our experiences using gl for proofs about hardware modules at Centaur, we usually try Glucose first. On Linux, version 3.0, 4.0, or 4.1 should work with Satlink without modification (though, some users have had difficulty with 4.0). (We have also successfully used earlier versions with Satlink, but occasionally needed to patch them in minor ways, e.g., to print counterexamples.)
Quick instructions:
(NOTE for Mac and FreeBSD/PCBSD users: If you are building Glucose 3.0 or
4.0, the build might fail. In that case, a solution may be first to make the
replacements shown below, where the the first in each pair (
In file
< // friend Lit mkLit(Var var, bool sign = false);
---
> friend Lit mkLit(Var var, bool sign = false);
< inline Lit mkLit (Var var, bool sign = false) { Lit p; p.x =
var + var + (int)sign; return p; }
---
> inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; }
In the file
< // double MiniSat::memUsedPeak(void) { return memUsed(); }
---
> double MiniSat::memUsedPeak(void) { return memUsed(); }
End of NOTE for Mac and FreeBSD/PCBSD users.)
Now create a shell script as follows, somewhere in your
#!/bin/sh /path/to/glucose-3.0/simp/glucose -model "$@"
As a quick test to make sure things are working, you can try to certify this book (where below, “[books]” refers to the community books directory):
cd [books]/centaur/satlink/solvers cert.pl test-glucose
You should now be able to use Satlink with configurations such as:
(satlink::make-config :cmdline "glucose")
Glucose can (optionally) produce UNSAT proofs that can be checked by a simpler program. Satlink includes a script that makes it easy to run the solver and then check any UNSAT answers. See unsat-checking for more information.
Penelope is a (mostly) open-source, parallel sat solver. The build process
is simple: run
cd [books]/centaur/satlink/solvers cert.pl test-penelope
Note that you will usually need to point Penelope at a configuration file
that tells it, e.g., how many cores to use. The Penelope distribution has a
(satlink::make-config :cmdline "penelope -config=/path/to/configuration.ini")
We are not aware of any UNSAT proof support for this solver.
An older version of Lingeling (Version ALA) is released under an open source (GPL3) license. For most of our problems, we found this version to be somewhat slower than Glucose 2.1. Of course, our experiences may not be representative.
Newer versions of Lingeling are available under a more restrictive license. These modern versions fared very well in the recent SAT competitions, so if the license does not pose a problem for you, it may well be worth trying.
For the open source version ALA, the build process is simple: download and
extract the tarball, run
cd [books]/centaur/satlink/solvers cert.pl test-lingeling cert.pl test-plingeling
Newer versions of Lingeling are allegedly able to produce unsat proofs, but we haven't figured out how to make it work.
Variants of Kissat won most of the major tracks at the 2022 SAT
competition. It can also be found on Github here. It is built using a
standard
The Riss3g solver is a (mostly) open-source variant of Glucose that did fairly well in recent competitions and seems to be sometimes faster than Glucose.
The build process was reasonably straightforward. After building, put the
resulting
cd [books]/centaur/satlink/solvers cert.pl test-riss3g cert.pl test-riss3gSimp
Like Glucose,
In principle, Satlink should work with any SAT solver that implements the DIMACS format. This format is used in the SAT competitions, so it is implemented by many solvers. Accordingly, you may wish to look at, e.g., the SAT Competition Results to get ideas about what SAT solvers are likely to perform well.
Getting a new solver to work with Satlink should be straightforward.
Typically you will need to install the solver, add it to your
<solver-command> <input-file>
Sometimes a solver may need extra command-line arguments. For instance,
Glucose needs a
To test out your new solver, Satlink includes a primitive check-config command that you can use to try your solver on a handful of
trivial problems. This is a very good way to make sure that at least the basic
i/o contract seems to be working. It should be easy to adapt one of the
If the