sys/man/2/sat

   1 .TH SAT 2
   2 .SH NAME
   3 satnew, satadd1, sataddv, satrange1, satrangev, satsolve, satmore, satval, satreset, satfree \- boolean satisfiability (SAT) solver
   4 .SH SYNOPSIS
   5 .de PB
   6 .PP
   7 .ft L
   8 .nf
   9 ..
  10 .PB
  11 #include <u.h>
  12 #include <libc.h>
  13 #include <sat.h>
  14 .PB
  15 struct SATParam {
  16         void (*errfun)(char *msg, void *erraux);
  17         void *erraux;
  18         long (*randfn)(void *randaux);
  19         void *randaux;
  20         /* + finetuning parameters, see sat.h */
  21 };
  22 .PB
  23 struct SATSolve {
  24         SATParam;
  25         /* + internals */
  26 };
  27 .PB
  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,
  34                         int min, int max);
  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);
  41 .SH DESCRIPTION
  42 .PP
  43 .I Libsat
  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
  46 .IP
  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 ∨ ...) ∧ ...,
  49 .PP
  50 where each
  51 .if t x\d\s7i\s10\u or y\d\s7i\s10\u
  52 .if n x_i or y_i
  53 can optionally be negated.
  54 .PP
  55 For example, consider
  56 .IP
  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).
  59 .PP
  60 This formula encodes the constraint that exactly one of the three variables be true. To represent this as input for
  61 .I libsat
  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"
  64 .IP
  65 1, 2, 3
  66 .br
  67 -1, -2
  68 .br
  69 -1, -3
  70 .br
  71 -2, -3
  72 .PP
  73 To actually solve this problem we would create a
  74 .B SATSolve
  75 structure and add clauses one by one using
  76 .I satadd1
  77 or
  78 .I sataddv
  79 (the former takes an
  80 .B int
  81 array, the latter a variadic list terminated by 0).
  82 The
  83 .B SATSolve
  84 is modified inplace but returned for convenience.
  85 Passing
  86 .B nil
  87 as a first argument will create and return a new structure.
  88 Alternatively,
  89 .I satnew
  90 will create an empty structure.
  91 .PP
  92 Once clauses have been added,
  93 .I satsolve
  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
  97 .I satsolve
  98 rerun.
  99 .I Satmore
 100 performs this automatically, excluding the current values of the variables.
 101 It is equivalent to
 102 .I satsolve
 103 if no variables have assigned values.
 104 .PP
 105 Once a solution has been found,
 106 .I satval
 107 returns the value of literal
 108 .I lit.
 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.
 112 .PP
 113 .I Satrange1
 114 and
 115 .I satrangev
 116 function like their
 117 .I satadd
 118 brethren but rather than adding a single clause they add multiple clauses corresponding to the constraint that at least
 119 .I min
 120 and at most
 121 .I max
 122 literals from the provided array be true.
 123 For example, the clause from above corresponds to
 124 .IP
 125 .B "satrangev(s, 1, 1, 1, 2, 3, 0);"
 126 .PP
 127 For debugging purposes, clauses can be retrieved using
 128 .IR satget .
 129 It stores the literals of the clause with index
 130 .I i
 131 (starting from 0) at location
 132 .IR lit .
 133 If there are more than
 134 .I nlit
 135 literals, only the first
 136 .I nlit
 137 literals are stored.
 138 If it was successful, it returns the total number of literals in the clause (which may exceed
 139 .IR nlit ).
 140 Otherwise (if
 141 .I idx
 142 was out of bounds) it returns -1.
 143 .PP
 144 .I Satreset
 145 resets all solver state, deleting all learned clauses and variable assignments.
 146 It retains all user provided clauses.
 147 .I Satfree
 148 deletes a solver structure and frees all associated storage.
 149 .PP
 150 There are a number of user-adjustable parameters in the
 151 .B SATParam
 152 structure embedded in
 153 .BR SATSolve .
 154 .I Randfun
 155 is called with argument
 156 .I randaux
 157 to generate random numbers between 0 and
 158 .if t 2\u\s731\s10\d-1;
 159 .if n 2^31-1;
 160 it defaults to
 161 .I lrand
 162 (see
 163 .IR rand (2)).
 164 .I Errfun
 165 is called on fatal errors (see DIAGNOSTICS).
 166 Additionally, a number of finetuning parameters are defined in
 167 .BR sat.h .
 168 By tweaking their values, the run-time for a given problem can be reduced.
 169 .SH EXAMPLE
 170 Find all solutions to the example clause from above:
 171 .PB
 172 .ta .5i 1i 1.5i
 173         SATSolve *s;
 174
 175         s = nil;
 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",
 182                         satval(s, 1),
 183                         satval(s, 2),
 184                         satval(s, 3));
 185         satfree(s);
 186 .SH SOURCE
 187 .B /sys/src/libsat
 188 .SH "SEE ALSO"
 189 Donald Knuth, ``The Art of Computer Programming'', Volume 4, Fascicle 6.
 190 .SH DIAGNOSTICS
 191 .I Satnew
 192 returns
 193 .B nil
 194 on certain fatal error conditions (such as
 195 .IR malloc (2)
 196 failure).
 197 Other routines will call
 198 .I errfun
 199 with an error string and
 200 .IR erraux .
 201 If no
 202 .I errfun
 203 is provided or if it returns,
 204 .I sysfatal
 205 (see
 206 .IR perror (2))
 207 is called.
 208 It is permissible to use
 209 .IR setjmp (2)
 210 to return from an error condition.
 211 Call
 212 .I satfree
 213 to clean up the
 214 .B SATSolve
 215 structure in this case.
 216 Note that calling the
 217 .I satadd
 218 or
 219 .I satrange
 220 routines with
 221 .B nil
 222 first argument will invoke
 223 .I sysfatal
 224 on error, since no
 225 .I errfun
 226 has been defined yet.
 227 .SH BUGS
 228 Variable numbers should be consecutive numbers starting from 1, since variable data is kept in arrays internally.
 229 .PP
 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.
 232 .PP
 233 There is no way to remove clauses (since it's unclear what the semantics should be).
 234 .PP
 235 The details about the tuning parameters are subject to change.
 236 .PP
 237 Calling
 238 .I satadd
 239 or
 240 .I satrange
 241 after
 242 .I satsolve
 243 or
 244 .I satmore
 245 may reset variable values.
 246 .PP
 247 .I Satmore
 248 will always return 1 when there are no assigned variables in the solution.
 249 .P
 250 Some debugging routines called under "shouldn't happen" conditions are non-reentrant.
 251 .SH HISTORY
 252 .I Libsat
 253 first appeared in 9front in March, 2018.