GSAT Tracing
---- -------
GSAT is a `greedy local search' procedure for satisfying
propositional formulae in CNF form. You have been asked
to code the GSAT algorithm, and as a first step, you are
to code a variation of the core of this algorithm and
output a trace of its execution.
A propositional formula is a formula containing boolean
variables and the operators AND, OR, and NOT. A propo-
sitional formula is in `conjunctive normal form', or
CNF, if it has the syntax:
CNF-formula ::= clause { AND clause }*
clause ::= ( literal { OR literal }* )
literal ::= variable | NOT variable
Thus if v1, v2, v3, ... are boolean variables, an exam-
ple is
( v1 OR NOT v3 ) AND ( NOT v4 OR v5 OR v2 )
As a shorthand we will write such formula with the
following modifications:
A. We will omit OR's and AND's.
B. We will omit v's, representing variables by
integers.
C. We will replace NOT's by -'s, negating the integer
representing a variable that is to be NOT'ed. We
will omit space between the `-' and its following
integer.
Thus the above example becomes:
( 1 -3 ) ( -4 5 2 )
The goal of the GSAT algorithm is to find an assignment
of values (true or false) to variables so that the given
input CNF formula is satisfied (evaluates to true by the
rules of boolean algebra).
The core of the GSAT algorithm is:
1. Assign values (true or false) to all the variables
randomly.
2. If all clauses are satisfied (so the formula is
satisfied), stop.
3. For each variable i, compute the number of clauses
N[i] that will be satisfied if just the value of
variable i is changed.
4. Form the set of variables S whose N[i] is maximal.
5. Pick one variable from S randomly and change its
value.
6. Return to step 2.
You have been asked to program a first version of this
GSAT core that replaces random choices as follows:
1. In step 1, the initial variable assignments are
input.
5. In step 5, instead of picking a variable from S
randomly, the variable i with the smallest value
of
( i - iteration ) mod V
is chosen, where `iteration' is the iteration num-
ber, 1, 2, 3, etc., and V is the number of vari-
ables. This amounts to searching variables begin-
ning with variable
( ( iteration - 1 ) mod V ) + 1
and wrapping around from variable V to variable 1,
picking the first variable with maximum N[i] that
is found.
You are asked to print out all variable changes in step
5 and the set of currently unsatisfied clauses in step
2.
To simplify implementation, GSAT is usually programmed
to run only on CNF formula whose clauses contain at most
3 literals. All CNF formula can be easily converted to
such a form. To make coding easier, we require that all
clauses have exactly 3 literals. To make this work, we
introduce the special variable v0 whose value is ALWAYS
false. Thus the clause (v1 OR v2) with two literals is
changed to the clause (v1 OR v2 OR v0) with three
literals, the last of which, v0, is always false.
Input
-----
For each formula, integers V, C, and I, in that order,
which are respectively the number of variables, the
number of clauses, and the maximum number of algorithm
iterations. 1 <= V <= 100, 1 <= C <= 100, and 1 <= I
<= 100. These are followed by V integers, each 0 repre-
senting `false' or 1 representing `true', that are the
initial values of the variables, in order from variable
1 through variable V. And these are followed by the
clauses, represented as a sequence of integers, using
the abbreviations given above. As each clause has ex-
actly 3 literals, parentheses would be redundant infor-
mation, and are therefore omitted. If a clause contains
variable 0, it is the last one or two variables of the
clause.
The input ends with a line containing 3 zeros.
Output
------
For each data set, first a single line containing
`Formula #' where # is 1, 2, 3, etc., the number of the
formula in the input.
Then every time step 2 is executed, one or more lines
containing the clauses that are not satisfied. Each
clause is represented by three integers enclosed in
parentheses, with clauses being separated by a space.
Consecutive integers are separated by a space, but par-
entheses are NOT separated from integers by space. If
there are more than 5 clauses, then exactly 5 clauses
are printed on each line but the last, which may have
1 to 5 clauses. The clauses MUST be printed the order
they were input.
As a special case, if there are no unsatisfied clauses
at step 2, print a single line containing just `DONE'
and stop the algorithm.
Lastly, every time step 5 is execute print either
`# = true' or `# = false' to indicate that variable #
has been assigned the new value `true' or `false'
respectively.
Execution of the algorithm should stop immediately after
the algorithm executes step 2 for the I+1'st time, if
execution has not previously stopped because the formula
was satisfied.
Sample Input
------ -----
4 5 10
0 0 0 0
1 2 0
2 3 0
3 4 0
4 -1 0
-1 -2 0
4 4 10
0 0 0 0
1 -2 0
2 -3 0
3 -4 0
4 0 0
4 5 8
1 0 0 1
-2 3 0
-3 4 0
-4 -2 0
1 2 0
-1 2 0
0 0 0
Sample Output
------ ------
Formula 1
(1 2 0) (2 3 0) (3 4 0)
2 = true
(3 4 0)
3 = true
DONE
Formula 2
(4 0 0)
1 = true
(4 0 0)
2 = true
(4 0 0)
3 = true
(4 0 0)
4 = true
DONE
Formula 3
(-1 2 0)
1 = false
(1 2 0)
3 = true
(1 2 0)
3 = false
(1 2 0)
4 = false
(1 2 0)
1 = true
(-1 2 0)
2 = true
(-2 3 0)
3 = true
(-3 4 0)
4 = true
(-4 -2 0)
Notes:
-----
The full GSAT algorithm runs the core algorithm some
number of times, and claims, perhaps incorrectly, that
the formula is unsatisfiable if none of these runs
produces a satisfying variable assignment. Each core
run stops after some number of iterations if it fails
to find a satisfying variable assignment. Full GSAT has
a good record of finding satisfying variable assignments
if they exist for some important classes of formulae.
The original GSAT paper is Selman, Levesque, and
Mitchell, A New Method for Solving Hard Satisfiability
Problems, Proc 10th Conf on AI (AAAI-92), July 1992,
440-446.
File: gsat.txt
Author: Bob Walton
Date: Mon Oct 21 00:36:45 EDT 2002
The authors have placed this file in the public domain;
they make no warranty and accept no liability for this
file.
RCS Info (may not be true date or author):
$Author: walton $
$Date: 2002/10/21 04:39:01 $
$RCSfile: gsat.txt,v $
$Revision: 1.7 $