NAME
satnew, satadd1, sataddv, satrange1, satrangev, satsolve, satmore,
satval, satreset, satfree – boolean satisfiability (SAT) solver 
SYNOPSIS
#include <u.h> #include <libc.h> #include <sat.h>
struct SATParam {
struct SATSolve {
SATSolve* satnew(void); 
DESCRIPTION
Libsat is a solver for the boolean satisfiability problem, i.e.
given a boolean formula it will either find an assignment to the
variables that makes it true, or report that this is impossible.
The input formula must be in conjunctive normal form (CNF), i.e.
of the form
For example, consider
Once clauses have been added, satsolve will invoke the actual solver. It returns 1 if it found an assignment and 0 if there is no assignment (the formula is unsatisfiable). If an assignment has been found, further clauses can be added to constrain it further and satsolve rerun. Satmore performs this automatically, excluding the current values of the variables. It is equivalent to satsolve if no variables have assigned values. Once a solution has been found, satval returns the value of literal lit. It returns 1 for true, 0 for false and –1 for undetermined. If the formula is satisfiable, an undetermined variable is one where either value will satisfy the formula. If the formula is unsatisfiable, all variables are undetermined.
Satrange1 and satrangev function like their satadd brethren but
rather than adding a single clause they add multiple clauses corresponding
to the constraint that at least min and at most max literals from
the provided array be true. For example, the clause from above
corresponds to
Satreset resets all solver state, deleting all learned clauses and variable assignments. It retains all user provided clauses. Satfree deletes a solver structure and frees all associated storage.
There are a number of user–adjustable parameters in the SATParam
structure embedded in SATSolve. Randfun is called with argument
randaux to generate random numbers between 0 and 231–1; it defaults
to lrand (see rand(2)). Errfun is called on fatal errors (see
DIAGNOSTICS). Additionally, a number of
finetuning parameters are defined in sat.h. By tweaking their
values, the run–time for a given problem can be reduced. 
EXAMPLE
Find all solutions to the example clause from above:

SOURCE
/sys/src/libsat 
SEE ALSO
Donald Knuth, ``The Art of Computer Programming'', Volume 4, Fascicle
6. 
DIAGNOSTICS
Satnew returns nil on certain fatal error conditions (such as
malloc(2) failure). Other routines will call errfun with an error
string and erraux. If no errfun is provided or if it returns,
sysfatal (see perror(2)) is called. It is permissible to use setjmp(2)
to return from an error condition. Call satfree to clean up the
SATSolve structure in this case. Note that calling the satadd
or satrange routines with nil first argument will invoke sysfatal
on error, since no errfun has been defined yet. 
BUGS
Variable numbers should be consecutive numbers starting from 1,
since variable data is kept in arrays internally. Large clauses of several thousand literals are probably inefficient and should be split up using auxiliary variables. Very large clauses exceeding about 16,000 literals will not work at all. There is no way to remove clauses (since it's unclear what the semantics should be). The details about the tuning parameters are subject to change. Calling satadd or satrange after satsolve or satmore may reset variable values. Satmore will always return 1 when there are no assigned variables in the solution.
Some debugging routines called under "shouldn't happen" conditions
are non–reentrant. 
HISTORY
Libsat first appeared in 9front in March, 2018. 