|
|
|---|
|
|
|
|---|
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:
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.