Skip to content

Commit be41d4d

Browse files
committed
Document SAT API.
Add some basic explanation of how the SAT api we are working with is implemented.
1 parent dcb6b94 commit be41d4d

File tree

1 file changed

+39
-2
lines changed

1 file changed

+39
-2
lines changed

src/solvers/README.md

Lines changed: 39 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -198,7 +198,7 @@ Performs any post-processing, which is normally adding constraints that
198198
require some global knowledge of the formula, ex. for encoding arrays
199199
into uninterpreted functions.
200200

201-
Some key classes:
201+
**Some key classes:**
202202

203203
\ref propt is instance of whichever solver is currently being used. This
204204
inherits from `decision_proceduret` whose interface has a fuller explanation
@@ -228,7 +228,44 @@ To be documented.
228228

229229
\subsection sat-solving-api-section SAT solving API
230230

231-
To be documented.
231+
The basic SAT solver interface is in [cnf](\ref cnft). This inherits
232+
from the [propositional logic decision procedure wrapper](\ref propt).
233+
234+
The interface supports the following operations by default:
235+
1. Boolean operations on literals (like `and`, `or`, `xor`), etc.
236+
These take as input two [literals](\ref literalt) and return as
237+
output another [literal](\ref literalt), applying Tseitin's
238+
transformation on them. Tseitin's transformation converts a
239+
propositional formula `F` into an equisatisfiable CNF formula
240+
that is linear in the size of `F`. For more information look at:
241+
https://en.wikipedia.org/wiki/Tseytin_transformation
242+
2. Generating new [literals](\ref literalt) and adding their
243+
variables to the formula and returning the number of variables
244+
or clauses the solver is operating with (with `no_variables`).
245+
246+
This interface is then extended by the various solver interfaces
247+
which implement the interface by hooking into the solver
248+
related functions that implement the operations that they
249+
abstract. Solvers for which drivers exist include Minisat,
250+
Minisat2, Chaff, Picosat, Glucose, Cadical, Booleforce and Lingeling.
251+
252+
For example, the Minisat 2 interface (in `satcheck_minisat2.h`)
253+
implements a method `prop_solve()` that hooks into Minisat 2's
254+
interface by initialising the variable list Minisat 2 will use,
255+
and then invoking the actual solver on the formula and checking
256+
whether the solver could manage find a satisfying assignment or
257+
not.
258+
259+
For more details on how the particular drivers work, refer
260+
to them in their interface and implementation files, which follow
261+
the naming pattern `satcheck_x`, where `x` is the name of the
262+
solver.
263+
264+
We also support any solver that can hook into [ipasir](http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/IPASIR____IPASIR). This is a
265+
generic incremental SAT solver API. This is handled by the
266+
`satcheck_ipasir.h` interface abstracts over `ipasir` with our own
267+
generic interface. For a description of the `ipasir` interface
268+
take a look at the following file: [ipasir.h](https://github.com/biotomas/ipasir/blob/master/ipasir.h)
232269

233270
\section sat-smt-encoding SAT/SMT Encoding
234271

0 commit comments

Comments
 (0)