SAT(2) SAT(2)
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 {
void (*errfun)(char *msg, void *erraux);
void *erraux;
long (*randfn)(void *randaux);
void *randaux;
/* + finetuning parameters, see sat.h */
};
struct SATSolve {
SATParam;
/* + internals */
};
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 assign-
ment to the variables that makes it true, or report that
this is impossible. The input formula must be in conjunc-
tive normal form (CNF), i.e. of the form
(x1 ∨ x2 ∨ x3 ∨ ...) ∧ (y1 ∨ y2 ∨ y3 ∨ ...) ∧ ...,
where each x_i or y_i can optionally be negated.
For example, consider
(x1 ∨ x2 ∨ x3) ∧ (¬x1 ∨ ¬x2) ∧ (¬x2 ∨ ¬x3) ∧ (¬x1 ∨
Page 1 Plan 9 (printed 11/11/25)
SAT(2) SAT(2)
¬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. Nega-
tion 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 vari-
adic 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 undeter-
mined 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.
Page 2 Plan 9 (printed 11/11/25)
SAT(2) SAT(2)
Satreset resets all solver state, deleting all learned
clauses and variable assignments. It retains all user pro-
vided 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 2^31-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:
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 per-
missible 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.
Page 3 Plan 9 (printed 11/11/25)
SAT(2) SAT(2)
Large clauses of several thousand literals are probably
inefficient and should be split up using auxiliary vari-
ables. 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" con-
ditions are non-reentrant.
HISTORY
Libsat first appeared in 9front in March, 2018.
Page 4 Plan 9 (printed 11/11/25)