Consider the problem of satisfying a Boolean expression--finding an
assignment to the variables such that the value of the expression is ``true''.
It turns out that this problem is both very hard and very important!
Satisfiability (SAT) finds applications in things like scheduling--both
project scheduling (Continental and NASA are both known to use the GSAT
algorithm for this purpose) and compiler instruction scheduling--and logic
network verification.
Unfortunately, SAT falls in the class of problems computer scientists call
NP-complete. This means that the best known solution takes time proportional
to an exponential function of the number of variables, a very long time
for non-trivial problems. Other problems in this class include brute-forcing
cryptography and the famous ``Travelling Salesman Problem''. Consider: the
solution-space for a 128-variable problem is
2128 - if a machine could try
1 billion solutions per second, it would still take over 10 trillion years to
try every one.
How can we attack such a problem? We elected to use the GSAT algorithm, which
is simple enough to implement in the amount of hardware we have, and quite
effective in practice. Some of the benefits of this approach:
- We can use a regularized form for SAT problems called 3CNF (``3-variable
conjunctive normal form''). This is a ``product of sums'' form with 3
variables (each possibly negated) in each clause. All of the clauses must be
satisfied.
- GSAT is a randomized, incremental algorithm which will keep searching
for a solution until one is found. This means that, rather than running to
completion (which we know from complexity theory must in general take
exponential time) without showing any clear progress, GSAT will continually
improve the solution, and can be paused (or aborted) at any time to examine
the current best answer.
Once you understand the SAT problem and 3CNF, the GSAT algorithm is easy to
follow. Begin with a random assignment to each of the variables. Check the
expression, counting the number of clauses which are satisfied. If there are
unsatisfied clauses, the algorithm searches for a solution with this
procedure: choose a variable at random and flip its value. Check the
expression again and see if the number of satisfied clauses decreased. If so,
flip it back (if the number of satisfied clauses increased or remained the
same, leave it). While there are still unsatisfied clauses, repeat that loop.
In summary:
- Randomly initialize a1..n
- While F is not satisfied, do:
- Select ai at random
- Complement(ai)
- If that decreased the number of satisfied clauses, undo it
- Output a1..n