GSAT: Initial Proposal

128-Variable GSAT Satisfiability Solver

This is the intial proposal - we have written it to be brief. More background on the problem, algorithm, and our plans is available in the preliminary Functional Description.

One Sentence Summary

Our project is to implement GSAT, a hill-climbing algorithm for satisfying large Boolean expressions (the 3-SAT problem), to operate on expressions involving 128 variables.

The 3-SAT Problem

Instance: a set of n Boolean variables a₁ to a_n, and an expression F of the form (a_i OR NOT a_i OR NOT a_i) AND (NOT a_i OR a_i OR NOT a_i) AND ... that is, consisting of a conjuntion of an arbitrary number of clauses, each of which are a disjunction of three variables, which may be complemented.

Question: does there exist an assignment of truth values for each of the variables such that F is satisfied (that is, true)?

More background on this problem than you can shake a stick at. Also: these lecture notes on satisfiability. But consider: the solution-space for a 128-variable problem is 2¹²⁸ - if a machine could try 1 billion solutions per second, it would still take over 10 trillion years to try every one. (Big numbers are cool.)

The GSAT Algorithm

• Randomly initialize a_1..n
• Do
  • Select a_i at random
  • Complement(a_i)
  • If that increased the number of satisfied clauses
    • Continue
    Else
    • Complement a_i
  While F is not satisfied
• Output a_1..n

Paper: An Empirical Analysis of Search in GSAT

Modules Needed

• On-chip register space for the variable bit-vector a_1..n, 128, 256, or 512 bits
• Off-chip RAM for storing the expression, on the order of 4 kilobits
• A source of randomness to select a variable to complement
• An accumulator for counting the number of satisfied clauses, and a register for storing the former value of this count
• A comparator to evaluate the effectiveness of the variable complement
• A controller to manage it all