Fgl-solving
Proving SAT instances in FGL
Calls of SAT in FGL are controlled by configuration objects of the type
fgl-sat-config. (An exception is when the default attachment of the
stub function interp-st-sat-check is changed by the user; this topic
pertains to the usual situation where its attachment is
fgl-default-sat-check-impl.)
When FGL calls SAT automatically on the result of symbolically executing a
theorem, the fgl-sat-config object that is used is the result of calling
the attachable stub function fgl-toplevel-sat-check-config. The default
attachment produces a config object that calls an external SAT solver through
SATLINK, and delegates the configuration of SATLINK to another attachable
function, fgl-satlink-config. So the easiest way to change the SAT solver
used by FGL is to change this attachment as follows (see satlink::config):
(define my-fgl-satlink-config ()
:returns (config satlink::config-p)
(satlink::change-config satlink::*default-config* :cmdline "kissat "))
(defattach fgl::fgl-satlink-config my-fgl-satlink-config)
When FGL rewrite rules or top-level theorems call
SAT using fgl-sat-check, the configuration object is provided as an
argument to that function. FGL also checks vacuity of hypotheses by default,
and the default configuration for this uses another attachable stub function
fgl-toplevel-vacuity-check-config.
An fgl-sat-config object is either an fgl-satlink-monolithic-sat-config, an fgl-ipasir-config, or an fgl-exhaustive-test-config
object. When
it is a fgl-satlink-monolithic-sat-config, satisfiability is checked by
perhaps performing some
AIG transformations
and subsequently calling a
SATLINK
monolithic solver.
When it is an fgl-ipasir-config, satisfiability is
checked by calling an
IPASIR
incremental SAT shared library, which may allow the
current check to benefit from learned lemmas and heuristic information from
previous checks. Finally, when it is an fgl-exhaustive-test-config,
satisfiability is checked by exhaustive testing of the AIG using vector simulation, perhaps after
some AIG transformations. This requires that the AIG have 37 or fewer inputs,
corresponding to the number of entries in FGL's Boolean variable database (see
fgl-getting-bits-from-objects. However, if the random-iters field
of the config object is set, then this input constraint is removed, randomized
testing is used instead of exhaustive testing, and the check can never return
UNSAT.
All three such config object types are simple tagged products, and they have
two fields in common:
- ignore-pathcond says to ignore the path condition when checking satisfiability
- ignore-constraint says to ignore the constraint condition (see def-fgl-boolean-constraint when checking satisfiability.
The other fields of the fgl-satlink-monolithic-sat-config object are
as follows. The transform and transform-config-override fields also
pertain to fgl-exhaustive-test-config objects:
- satlink-config-override may either be a satlink::config object
or nil. If set, this object determines how to call SAT, e.g., what
command-line solver to use. If not, the SATLINK configuration object used is
the attachment of the stub function fgl-satlink-config.
- transform is a Boolean value; if T, then AIGNET transforms are
used to simplify the problem before calling the solver.
- transform-config-override is a list of AIGNET transform configuration
objects; see aignet::aignet-comb-transforms. If empty, the attachment
of the stub function fgl-aignet-transforms-config is used as the list of
transforms.
The other fields of the fgl-ipasir-config object are:
- ipasir-callback-limit may be nil or a natural number. If a number, it
provides a work limit for the incremental SAT checker, the precise meaning of
which depends on the solver but is generally a conflict or restart count.
- ipasir-recycle-callback-limit may be nil or a natural number. If a
number, it causes the solver object to be destroyed and recreated after the
given number of callbacks, which may be important for performance.
- ipasir-index is a natural number, default 0. This determines which
solver object is used. If a new ipasir index is used, then a new solver object
is created and initialized, and every subsequent use of that ipasir index
refers to that solver object (until perhaps the recycle-callback-limit causes
it to be reinitialized).
Subtopics
- Fgl-sat-check
- Checking satisfiability of intermediate terms during FGL interpretation.
- Fgl-exhaustive-test-config
- FGL SAT config object that says to use exhaustive vectorized simulation to check satisfiability.
- Fgl-prove
- Check that the given object is never NIL and report an error if not.
- Fgl-vacuity-check
- Check that the given object is satisfiable and report an error if not.
- Fgl-sat-check/print-counterexample
- Check satisfiability during FGL interpretation and print counterexamples.
