SAT(2)SAT(2)
NAME
satnew, satadd1, sataddv, satrange1, satrangev, satsolve, satmore, satval, satreset, satfree – boolean satisfiability (SAT) solver
SYNOPSIS
unhandled troff command .de
unhandled troff command ..
unhandled troff command .PB
#include <u.h>
#include <libc.h>
#include <sat.h>
unhandled troff command .PB
struct SATParam {
void (*errfun)(char *msg, void *erraux);
void *erraux;
long (*randfn)(void *randaux);
void *randaux;
/* + finetuning parameters, see sat.h */
};
unhandled troff command .PB
struct SATSolve {
SATParam;
/* + internals */
};
unhandled troff command .PB
SATSolve* satnew(void);
void satfree(SATSolve *s);
SATSolve* satadd1(SATSolve *s, int *lit, int nlit);
SATSolve* sataddv(SATSolve *s, ...);
SATSolve* satrange1(SATSolve *s, int *lit, int nlit,
int min, int max);
SATSolve* satrangev(SATSolve *s, int min, int max, ...);
int satsolve(SATSolve *s);
int satmore(SATSolve *s);
int satval(SATSolve *s, int lit);
int satget(SATSolve *s, int i, int *lit, int nlit);
void satreset(SATSolve *s);
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
(x1 ∨ x2 ∨ x3 ∨ …) ∧ (y1 ∨ y2 ∨ y 3 ∨ …) ∧ …,
where each
xi or yi
can optionally be negated.
For example, consider
(x1 ∨ x2 ∨ x3) ∧ (¬x1 ∨ ¬x2) ∧ (¬x2 ∨ ¬x3) ∧ (¬x1 ∨ ¬x3).
This formula encodes the constraint that exactly one of the three variables be true. To represent this as input for
libsat
we assign positive integers to each variable.
Negation is represented by the corresponding negative number, hence our example corresponds to the set of "clauses"
1, 2, 3
-1, -2
-1, -3
-2, -3
To actually solve this problem we would create a
SATSolve
structure and add clauses one by one using
satadd1
or
sataddv
(the former takes an
int
array, the latter a variadic list terminated by 0).
The
SATSolve
is modified inplace but returned for convenience.
Passing
nil
as a first argument will create and return a new structure.
Alternatively,
satnew
will create an empty structure.
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
satrangev(s, 1, 1, 1, 2, 3, 0);
For debugging purposes, clauses can be retrieved using
satget.
It stores the literals of the clause with index
i
(starting from 0) at location
lit.
If there are more than
nlit
literals, only the first
nlit
literals are stored.
If it was successful, it returns the total number of literals in the clause (which may exceed
nlit).
Otherwise (if
idx
was out of bounds) it returns -1.
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:
unhandled troff command .PB
SATSolve *s;
s = nil;
s = sataddv(s, 1, 2, 3, 0);
s = sataddv(s, -1, -2, 0);
s = sataddv(s, -1, -3, 0);
s = sataddv(s, -2, -3, 0);
while(satmore(s) > 0)
print("x1=%d x2=%d x3=%d\\n",
satval(s, 1),
satval(s, 2),
satval(s, 3));
satfree(s);
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.
unhandled troff command .P
Some debugging routines called under "shouldn’t happen" conditions are non-reentrant.
HISTORY
Libsat
first appeared in 9front in March, 2018.