3 satnew, satadd1, sataddv, satrange1, satrangev, satsolve, satmore, satval, satreset, satfree \- boolean satisfiability (SAT) solver
16 void (*errfun)(char *msg, void *erraux);
18 long (*randfn)(void *randaux);
20 /* + finetuning parameters, see sat.h */
28 .ta +\w'\fLSATSolve* \fP'u
29 SATSolve* satnew(void);
30 void satfree(SATSolve *s);
31 SATSolve* satadd1(SATSolve *s, int *lit, int nlit);
32 SATSolve* sataddv(SATSolve *s, ...);
33 SATSolve* satrange1(SATSolve *s, int *lit, int nlit,
35 SATSolve* satrangev(SATSolve *s, int min, int max, ...);
36 int satsolve(SATSolve *s);
37 int satmore(SATSolve *s);
38 int satval(SATSolve *s, int lit);
39 int satget(SATSolve *s, int i, int *lit, int nlit);
40 void satreset(SATSolve *s);
44 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.
45 The input formula must be in conjunctive normal form (CNF), i.e. of the form
47 .if t (x\d\s71\s10\u ∨ x\d\s72\s10\u ∨ x\d\s73\s10\u ∨ …) ∧ (y\d\s71\s10\u ∨ y\d\s72\s10\u ∨ y \d\s73\s10\u ∨ …) ∧ …,
48 .if n (x1 ∨ x2 ∨ x3 ∨ ...) ∧ (y1 ∨ y2 ∨ y3 ∨ ...) ∧ ...,
51 .if t x\d\s7i\s10\u or y\d\s7i\s10\u
53 can optionally be negated.
57 .if t (x\d\s71\s10\u ∨ x\d\s72\s10\u ∨ x\d\s73\s10\u) ∧ (¬x\d\s71\s10\u ∨ ¬x\d\s72\s10\u) ∧ (¬x\d\s72\s10\u ∨ ¬x\d\s73\s10\u) ∧ (¬x\d\s71\s10\u ∨ ¬x\d\s73\s10\u).
58 .if n (x1 ∨ x2 ∨ x3) ∧ (¬x1 ∨ ¬x2) ∧ (¬x2 ∨ ¬x3) ∧ (¬x1 ∨ ¬x3).
60 This formula encodes the constraint that exactly one of the three variables be true. To represent this as input for
62 we assign positive integers to each variable.
63 Negation is represented by the corresponding negative number, hence our example corresponds to the set of "clauses"
73 To actually solve this problem we would create a
75 structure and add clauses one by one using
81 array, the latter a variadic list terminated by 0).
84 is modified inplace but returned for convenience.
87 as a first argument will create and return a new structure.
90 will create an empty structure.
92 Once clauses have been added,
94 will invoke the actual solver.
95 It returns 1 if it found an assignment and 0 if there is no assignment (the formula is unsatisfiable).
96 If an assignment has been found, further clauses can be added to constrain it further and
100 performs this automatically, excluding the current values of the variables.
103 if no variables have assigned values.
105 Once a solution has been found,
107 returns the value of literal
109 It returns 1 for true, 0 for false and -1 for undetermined.
110 If the formula is satisfiable, an undetermined variable is one where either value will satisfy the formula.
111 If the formula is unsatisfiable, all variables are undetermined.
118 brethren but rather than adding a single clause they add multiple clauses corresponding to the constraint that at least
122 literals from the provided array be true.
123 For example, the clause from above corresponds to
125 .B "satrangev(s, 1, 1, 1, 2, 3, 0);"
127 For debugging purposes, clauses can be retrieved using
129 It stores the literals of the clause with index
131 (starting from 0) at location
133 If there are more than
135 literals, only the first
138 If it was successful, it returns the total number of literals in the clause (which may exceed
142 was out of bounds) it returns -1.
145 resets all solver state, deleting all learned clauses and variable assignments.
146 It retains all user provided clauses.
148 deletes a solver structure and frees all associated storage.
150 There are a number of user-adjustable parameters in the
152 structure embedded in
155 is called with argument
157 to generate random numbers between 0 and
158 .if t 2\u\s731\s10\d-1;
165 is called on fatal errors (see DIAGNOSTICS).
166 Additionally, a number of finetuning parameters are defined in
168 By tweaking their values, the run-time for a given problem can be reduced.
170 Find all solutions to the example clause from above:
176 s = sataddv(s, 1, 2, 3, 0);
177 s = sataddv(s, -1, -2, 0);
178 s = sataddv(s, -1, -3, 0);
179 s = sataddv(s, -2, -3, 0);
180 while(satmore(s) > 0)
181 print("x1=%d x2=%d x3=%d\\n",
189 Donald Knuth, ``The Art of Computer Programming'', Volume 4, Fascicle 6.
194 on certain fatal error conditions (such as
197 Other routines will call
199 with an error string and
203 is provided or if it returns,
208 It is permissible to use
210 to return from an error condition.
215 structure in this case.
216 Note that calling the
222 first argument will invoke
226 has been defined yet.
228 Variable numbers should be consecutive numbers starting from 1, since variable data is kept in arrays internally.
230 Large clauses of several thousand literals are probably inefficient and should be split up using auxiliary variables.
231 Very large clauses exceeding about 16,000 literals will not work at all.
233 There is no way to remove clauses (since it's unclear what the semantics should be).
235 The details about the tuning parameters are subject to change.
245 may reset variable values.
248 will always return 1 when there are no assigned variables in the solution.
250 Some debugging routines called under "shouldn't happen" conditions are non-reentrant.
253 first appeared in 9front in March, 2018.