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.

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.

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 usewith-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 theinit field in order to eliminate a source of unsoundness.(ipasir-reinit ipasir) initializes a solver object, just likeipasir-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 bywith-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 callingipasir-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 ofipasir-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 withipasir-add-lit are permanent, the assumption is emptied each timeipasir-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 ofipasir-add-lit oripasir-assume , the solver can be queried withipasir-val to assess the values of literals under the satisfying assignment. Similarly, when it returns:unsat , then until the next call ofipasir-add-lit oripasir-assume the solver can be queried withipasir-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).</li> <li>@('(ipasir-val ipasir lit) determines the value of lit under the current satisfying assignment, returning 1 if true, 0 if false, ornil 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 ofipasir-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 toipasir-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 theipasir-set-limit callback has been called since the last initialization or call ofipasir-set-limit .

- Literals are represented as
(var << 1) | neg rather thanvar*(-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 thanipasir-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 .

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.

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

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.

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

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,

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

- 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-set$c
- Ipasir-failed$c
- Ipasir-assume$c
- Ipasir-add-lit$c
- Ipasir-val$c
- With-local-ipasir
- Create a local ipasir solver object, initialize it, and properly release it when done.
- Ipasir-solve$c
- Ipasir-reinit$c
- Ipasir-init$c
- Ipasir-finalize-clause$c
- Ipasir-some-history$c
- Ipasir-solved-assumption$c
- Ipasir-release$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.