Consider this an unfinished work in progress for now.
The GSAT algorithm is a straightforward hill-climbing algorithm for solving 3-SAT satisfiability problems. This problem domain is known to be NP-complete, and is used extensively for constraint-based scheduling by several large companies, and thus a fast hardware-based system for attacking satisfiability problems is quite interesting. The algorithm works on a logical statement which is a conjunction of disjunctions -- that is, if written in C the format of a statement would look like:
(A || !B || C) && (D || B || !F) && (!E ||
!G || A) && (....The GSAT algorithm works by making an initial random assignment to all variables in the logical statement, and counting the number of satisfied clauses. It then picks a variable from a uniform distribution on all variables in the statement, and logically toggles its value. It then checks again the number of satisfied clauses; if the number has increased, the change is kept, and if not the change is reverted. This continues until either the statement is fully satisfied, or a sufficient amount of time has elapsed that the GSAT run is terminated. It is important to note that GSAT is not complete. That is, GSAT cannot say whether a given statement has a solution or not -- it is possible that GSAT will miss a solution to a statement. But if it does find a solution, the algorithm is sound -- that is, if it finds a solution it is a correct solution.
The "difficult" range of statements involve statements such that the number of clauses is approximately 3 to 4 times the number of variables -- outside this range, most SAT problems are relatively trivial because it can be quickly determined that there are no solutions, or many solutions (the problems are over- or under-constrained). Additionally, the problems become interesting from a runtime standpoint as the number of variables increases above about 200, although the 100-200 range is still fair game. The hardest SAT problems being solved today (according to Dr. Subramanian) are on the order of 50,000 variables, for reference.
The implementation of this algorithm needs several components. First, it needs a memory to store both the variable values and the clause structure. One proposal for this is to store the clause structure as 3-tuples of 8-bit values: 1 bit for negation, and 7 bits as a variable number. The variables are stored as bits. The advantage of this is that clauses fit nicely into 3-byte sequences, however it limits the size of the problem domain to 128 variables, which is on the borderline of the set of interesting problems, but more than adequate for a "proof of concept" implementation.
Pin limitations are going to be a big constraint on this project -- we will need 8 pins for byte-sized input, plus 10 to 12 address output bits for the clause lookup. This is because clauses will require either 3 or 4 bytes per clause, and there should be between 3 and 4 times as many clauses as there are variables -- this means that if we have 7 bits of variable namespace, we need at least 10 (preferably 11) bits of byte-addressable memory.
Another pin need is for a random input. It has been suggested that we hook up the output of a PC's parallel port for randomness, sending random data to the parallel port and picking selected bits from the parallel port output. This could either be done with a full set of input random values, or have a clock-based scheme where on each clock cycle a random value is read from the Random Input pin and assigned to a bit in the register which is used for the random choice of variable in the GSAT algorithm. As a new random value is not required on every clock tick, the one-pin random input solution has promise but again is slightly more complex than simply reading a byte value in.
Last, we will need assorted pins for state machine control, and some mechanism for retrieving and/or monitoring the results as the algorithm progresses through solving a given statement.
Internally, we will need a number of registers. First, we need a huge register bank to store the 128 variables (each one bit). Second, a place to store the structure of the current clause, so that the variable values can be tested against the clause structure. Third, we need two registers, an adder, and a comparator to test the number of satisfied clauses for a given variable set. We also need a register to store the index of the variable currently selected, and another register to store the random bits for random selection. That totals to seven internal registers, one adder, and a comparator -- plus the clause addressing logic which requires an additional register or two and another adder.