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 3/28/24)

     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 3/28/24)

     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 3/28/24)

     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 3/28/24)