Ipasir
ACL2 bindings for the ipasir incremental SAT solving interface
IPASIR is a simple C interface to incremental SAT solvers. (It
stands for Reentrant Incremental Sat solver API, in reverse.) This interface is
supported by a few different solvers because it is used in the SAT
competition's incremental track. The ipasir distribution, containing the
interface and some sample solvers, can be found at this GitHub repository. The
ACL2 ipasir library is an attempt to semi-soundly allow ACL2 programs to
interface with such SAT solver libraries.
Getting Started
First, if you just want to reason about an incremental solver without
actually running it, you can include "ipasir-logic.lisp", which sets up the
abstract stobj representing the solver and its logical story, but doesn't
install the under-the-hood backend and therefore doesn't require any trust
tags. Additionally, "ipasir-tools.lisp" builds on that to create some useful
shortcuts, also without any trust tags.
To load the backend, include "ipasir-backend.lisp". This book first loads
the shared library specified by the environment variable
IPASIR_SHARED_LIBRARY, which should contain the path to a SAT solver shared
library. It then overrides the executable definitions of the ipasir interface
functions so that they instead call the appropriate functions from the shared
library.
There are several SAT solver libraries that implement the IPASIR interface;
to obtain one, see building-an-ipasir-solver-library.
Using ipasir functions
Note: If you are familiar with ipasir, you'll notice that the ACL2 wrappers
work slightly differently than the underlying ipasir implementation. The
differences are listed below under "Departures from the C Interface."
The following interfacing
functions are provided:
- (ipasir-init ipasir state) initializes the solver object so that other
functions can then be used. This is already done for you if you use
with-local-ipasir. It requires that the state of the solver is
:undef and it puts the solver in state :input. It takes and returns
state because (in the logical story) it reads the oracle into the init
field in order to eliminate a source of unsoundness.
- (ipasir-reinit ipasir) initializes a solver object, just like
ipasir-init, except that it has an additional guard, (consp
ipasir.history), which ensures that it can only be called on a solver that
has previously been initialized and subsequently released.
- (ipasir-release ipasir) frees the solver object when you are done with
it. This is also taken care of by with-local-ipasir. It requires that
the solver state not be :undef and it puts it in state :undef.
- (ipasir-add-lit ipasir lit) is the mechanism by which new clauses may
be added to the formula. A clause is added by calling this function once for
each literal in the clause, then calling ipasir-finalize-clause, which
adds the clause to the formula. (Literals are represented as natural numbers
where the LSB indicates negation and the rest is the variable number; see litp.) Requires that the solver not be in state :undef, and puts the
solver in state :input.
- (ipasir-finalize-clause ipasir) adds the clause built up by calls of
ipasir-add-lit to the formula, and empties the clause buffer. Requires
that the solver not be in state :undef, and puts the solver in state
:input.
- (ipasir-assume ipasir lit) adds a literal to the current assumption
cube. Whereas clauses added with ipasir-add-lit are permanent, the assumption
is emptied each time ipasir-solve is called. Requires that the solver not
be in state :undef, and puts the solver in state :input.
- (ipasir-input ipasir) requires that the solver not be in state
:undef and puts the solver in state :input. In reality, this is a
logical fiction that is convenient for functions that normally add some
literals, clauses, or assumptions but may sometimes not do anything.
- (ipasir-solve ipasir) determines the satisfiability of the formula
under the assumption. It returns (mv status ipasir), where status is one
of :unsat, :sat, or :failed. When it returns :sat, then
until the next call of ipasir-add-lit or ipasir-assume, the solver can be
queried with ipasir-val to assess the values of literals under the
satisfying assignment. Similarly, when it returns :unsat, then until the
next call of ipasir-add-lit or ipasir-assume the solver can be queried
with ipasir-failed to determine whether a given assumption literal was in
the unsatisfiable core subset of the assumption. Requires that the solver not
be in state :undef, and puts the solver in state :sat, :unsat,
or (when failed) :input.
- (ipasir-val ipasir lit) determines the value of lit under the current
satisfying assignment, returning 1 if true, 0 if false, or nil
if not determined. Requires that the solver be in state :sat and leaves
it in that state.
- (ipasir-failed ipasir lit) determines whether lit, which must be a
member of the assumptions from the previous call of ipasir-solve, was in
the unsatisfiable core, which is a subset of that assumption under which the
formula is unsat. Requires that the solver be in state :unsat and leaves
it in that state.
- (ipasir-set-limit ipasir count-or-nil) limits the effort spent by the
solver. Logically, all this does is cons something onto the history and reset
the callback count to 0. Under the hood, it sets a callback function for the
solver to call every so often. If count-or-nil is a positive number, then each
call of solve may only call the callback that many times before it fails.
Setting it to nil or 0 removes the limit. If 0, the callbacks are still
performed and counted, but will not cause termination. The frequency with
which the callback is called varies by solver.
- (ipasir-get-status ipasir) simply returns the current status :undef,
:input, :sat, or :unsat. Mostly used in guards to allow executable guards for
most of the ipasir functions.
- (ipasir-some-history ipasir) (ipasir-empty-new-clause ipasir)
(ipasir-get-assumption ipasir) (ipasir-solved-assumption ipasir) are
functions similar in spirit to ipasir-get-status in that they are intended
to only be used to define executable guards for the ipasir stobj.
- (ipasir-callback-count ipasir) queries how many times the
ipasir-set-limit callback has been called since the last initialization or
call of ipasir-set-limit.
Departures from the C Interface
- Literals are represented as (var << 1) | neg rather than
var*(-1^^neg), for compatibility with other ACL2 libraries such as satlink and ACL2::aignet.
- ipasir-solve returns a symbol as its status rather than an integer
code.
- ipasir-finalize-clause is used to complete a clause and add it to the
formula, rather than ipasir-add-lit with literal 0.
- ipasir-val returns a bit or NIL rather than a
literal to indicate the value of the literal in the counterexample.
- ipasir-set-limit is used to set resource limitations, replacing the
callback mechanism of ipasir_set_terminate.
- The ACL2 interface does not yet support the API ipasir_set_learn.
Logical story
There are several problems to solve when trying to soundly model an
interface with an external library in ACL2. First, we need a logical
description of the behavior of the external library that is specific enough to
be useful, but not so specific that unexpected behaviors produce soundness
bugs. Second, we need to restrict user access to functions that break the
abstraction that allows us to model the external behavior logically. Third, we
need to think about possible nondeterminism and how we can rule it out or
soundly account for it.
Logical description of behavior
The logical definitions for the ipasir abstract stobj's interface functions
are described in terms of a product data structure, ipasir$a.
The fields of the ipasir$a contain information such as the full
clausal formula and the current assumption, solver status, and current
satisfying assignment or unsat core. The behavior of the interface functions
above is modeled by updating and retrieving information from these fields.
However, the ipasir-solve function is special because it is a constrained
function: we don't know for any given solver state whether it will solve the
SAT problem or fail due to resource limitations. We constrain it so that when
it returns :unsat it implies the formula is unsatisfiable under the
assumption, and assume certain other behaviors, e.g., it doesn't change the
formula and it updates the assumption, solution, and status fields
appropriately.
Preventing Abstraction Breakage
The concrete stobj used to introduce the abstract stobj (prior to loading
the under-the-hood C interface) is a single-field stobj whose one field is
the (logical) solver object. The under-the-hood code smashes definitions built
upon this stobj's accessor/updater. So if a user were to use this concrete
stobj, after calling any of these smashed definitions he/she would find that
the stobj accessor (e.g.) returns some foreign pointer object. This would be a
logical problem, so we disallow execution of the accessor and updater for the
concrete stobj.
Handling Nondeterminism
A possible soundness problem with any external tool is that the logical
model may pretend something is a function which actually isn't. Calling an
external SAT solver on the same problem multiple times could yield different
results even if the solver is correct; e.g., it could produce different
satisfying assignments.
One way this could occur is by calling ipasir-solve on the same solver
object twice, without changing the formula and with the same assumptions. We
deal with this possibility in the logical story by having every function that
updates the solver also extend a history field in the solver model, so that you
can't ever get back to the same solver object on which you already called
ipasir-solve.
This takes care of multiple calls on the same solver object. But we could
also construct two different solvers and run exactly the same series of
functions on them, and possibly yield different results due to nondeterminism
in the external library. To solve this, ipasir-init sets the init
field of the solver model to the result of reading the ACL2 state's oracle.
The abstract stobj interface provides no way to access this field so we can't
know what its value is for any particular instance of the solver, and there's
no way to provably get the same value from the oracle twice, so this ensures
there's no way to make two solvers in such a way that they can logically be
proven to be equal.
This solution is a bit onerous because it means that any function that ever
uses an ipasir solver has to take and return state. This can be worked around
using with-local-state if necessary, at the cost of possible unsoundness
due to nondeterminism in the external library. Additionally,
ipasir-reinit can be used to reinitialize a previously released solver
without involving state.
Subtopics
- Ipasir$a
- Datatype for the logical model of an ipasir incremental SAT solver.
- Building-an-ipasir-solver-library
- How to obtain an ipasir backend implementation.
- Ipasir-formula
- Tools for constructing the ipasir formula.
- Ipasir-bump-activity-vars$a
- Logical function for bumping var activity (unmodeled side-effect)
- Ipasir-set$a
- Ipasir-bump-activity-vars$c
- Ipasir-get$a
- Ipasir-set-limit$c
- Ipasir-failed$c
- Ipasir-assume$c
- Ipasir-add-lit$c
- Ipasir-val$c
- Ipasir-set$c
- With-local-ipasir
- Create a local ipasir solver object, initialize it, and
properly release it when done.
- Ipasir-solve$c
- Ipasir-init$c
- Ipasir-finalize-clause$c
- Ipasir-some-history$c
- Ipasir-solved-assumption$c
- Ipasir-release$c
- Ipasir-reinit$c
- Ipasir-input$c
- Ipasir-get$c
- Ipasir-get-status$c
- Ipasir-get-curr-stats$c
- Ipasir-get-assumption$c
- Ipasir-empty-new-clause$c
- Ipasir-callback-count$c
- Ipasir-val
- Retrieve the value of the given literal under the current satisfying assignment.
- Ipasir-solve
- Attempt to solve the formula under the current assumption.
- Ipasir-set-limit
- Set a limit on the effort spent on each solve attempt.
- Ipasir-reinit
- Reinitializes a previously released ipasir solver to a useful state.
- Ipasir-failed
- Check whether a literal is in the current unsatisfiable assumption core.
- Ipasir-callback-count
- Return the number of times the ipasir-set-limit counter was incremented.
- Ipasir-release
- Frees the ipasir solver object.
- Ipasir-input
- Coerce the solver into the :input state.
- Ipasir-init
- Initializes the ipasir solver to a useful state.
- Ipasir-finalize-clause
- Add the accumulated clause to the formula.
- Ipasir-assume
- Add a literal to the current assumption cube.
- Ipasir-add-lit
- Add a new literal to the clause being accumulated.
