A simple representation for Boolean formulas in

SAT solvers are programs that can solve the Boolean satisfiability problem. Modern solvers implement clever algorithms in fast languages like C and C++, so they can quickly solve many large problems. Developing faster SAT solvers is an active area of research with frequent competitions.

SAT solvers are useful because many problems can be recast as SAT problems. For instance, the gl framework can translate many ACL2 proof goals, e.g., bounded arithmetic problems, into SAT problems. This allows for a large class of theorems to be solved quickly and automatically by the SAT solver. This is especially useful in ACL2::hardware-verification.

**Satlink** is an interfacing library that allows ACL2 to make use of
off-the-shelf SAT solvers like lingeling, glucose, and so on; see
sat-solver-options for download and build help. It provides:

- A (trivial) representation and semantics for Boolean formulas in conjunctive normal form; see cnf.
- A function, sat, that can invoke a SAT solver on a formula and interpret its output. This is done via tshell, so the integration is very smooth, e.g., you can interrupt the SAT solver.
- A logical-story that allows us to
, that when the SAT solver claims the formula is unsatisfiable, it's correct.**assume, using a**trust tag

We don't have to assume anything when the SAT solver claims that a formula is satisfiable, since we can just check the alleged satisfying assignment it produces.

The soundness threat may be reduced by checking the output of the SAT
solver. There has been recent progress in the SAT community toward
standardizing formats for UNSAT proofs, reducing the overhead of producing
these proofs, and developing fast tools to check these proofs. Satlink
includes, e.g., a

Satlink is a low-level library. It would be a bit weird to want to use it directly. Instead, it is typically used indirectly through other tools, such as the gl framework, or ACL2::aig-sat, or the aignet::aignet-cnf translation. These other approaches are likely to be more convenient than using Satlink directly.

If you want to include Satlink directly for some reason, the book to include is:

(include-book "centaur/satlink/top" :dir :system)

Once you load this book, you generally need to construct your input cnf formula in some way, and then call sat.

- Sat-solver-options
- How to get a SAT solver that you can use with satlink.
- Config-p
- Settings for which SAT solver to run, how to invoke it, what output to print, etc.
- Logical-story
- How we logically assume that the SAT solver's claims of unsat are correct.
- Dimacs
- DIMACS format is a standard interface to SAT solvers.
- Gather-benchmarks
- A satlink plugin for saving problems and storing them in
satlink-benchmarks directories. - Cnf
- Our representation (syntax and semantics) for conjunctive normal form formulas.
- Satlink-extra-hook
- An attachable hook for performing extra actions after successful calls of the SAT solver.
- Sat
- Top-level function for running a SAT solver.