CS 540 - Introduction To Artificial Intelligence  Spring(2000)

Homework #4 - Propositional Logic, Simulated Annealing & Games

Part I - a) The board-splitting game

This game consists of an N x N board (N is a power of 2) where each cell contains a randomly chosen integer. The two players, MAX and MIN, take turns in splitting the board in two and removing (or covering) the unwanted half. MAX splits the board along a vertical cut and chooses the right or left half. MIN splits the board horizontally, choosing the upper or lower half.

To make the game interesting, MIN promises to pay MAX as many dollars as the number indicated on the last remaining square. MAX and MIN take turns going first and each game is played with a randomly created board.

You are given the following board:
 
 

5

3

4

1

4

1

3

2

8

2

5

2

6

9

7

6


 
 

b) Use Propositional Logic to solve the following logical puzzle:

Four Friends - Artur, Betty, Charles and Dorothy - are suspected of murder. They testify as follows:

Arthur: if Betty is guilty, so is Dorothy.

Betty: Arthur is guilty, but Dorothy is not.

Charles: I am not guilty, but either Arthur or Dorothy is guilty.

Dorothy: if Arthur is not guilty, then Charles is guilty.

b1) Are the four statements consistent (satisfiable)?

b2) If everyone is telling the truth, who is guilty?

b3) Is the statement- if Dorothy is not guilty then Betty is not guilty- a logical consequence of Artur's statement?

Answer this by three different ways.

 

Part II - GSAT vs. WALKSAT vs. Simulated Annealing

Problem Ib is an example of a satisfiability problem, abbreviated as SAT. SAT was the first computational task shown to be NP-complete, i.e. a problem that requires an exponential amount of computing time to solve. If we have N propositions, each one can have the value of T or F, therefore the number of possible interpretations of the propositions is 2N. Many interesting problems in Computer Science turn out to be NP-complete, such as N-queens, graph coloring, and the traveling salesman problem. The completeness property of NP-complete problems means that if an efficient algorithm for solving just one of these problems could be found, one would immediately have an efficient algorithm for all NP-complete problems. However a fundamental conjecture of complexity theory is that no such efficient algorithm exists. You should see that SAT is not just about conjunctions and disjunctions in logic, but central to solving a number of important problems in computer science.

For this problem of the homework, we will examine four non-exhaustive algorithms which try to solve SAT problems. The first is GSAT,  which we describe below (another version of it is also described in your textbook as problem 6.15 on pg. 182). You should read this problem for an understanding of how SAT problems are represented, in particular for this assignment we will be dealing with 3SAT. GSAT is a random-restart, hill-climbing search algorithm. Rather than solving Problem Ib using truth-table, you could tranform the wffs into 3-CNF and use the GSAT algorithm, generate random truth assignments for the propositions, and then search until you found a solution. You should implement the version given below. You should also implement two other variants: Gsat with Walk, and WalkSat. They are also given below.

The fourth algorithm you will implement is Simulated Annealing (SA), found on pg. 113. In all problems, your nodes will be instances of the ThreeCNF.java class provided for you (you may have to modify the file a little). In SA, successor nodes are reached by randomly flipping the truth value of one of the propositions. Your score, or value for each node, will be the number of satisfied clauses. The goal is to have all clauses of your sentence satisfied, the more clauses the better the node. As for the temperature schedule used, we will begin with a temperature T. Each iteration of the algorithm we will reduce the temperature by a percentage amount. For instance, we could start our temperature at 100, and reduce it each time by 10%. Our schedule would then become 100, 90, 81, 72.9 ... . To stop our algorithm we specify a minimum temperature, such at 0.01, and return the best node found so far. Since each problem requires its own specific parameters, you should tune the starting temperature and reduction percentage to best fit this 3SAT problem.

What to do

Write a program in Java called Satisfiable.java which implements GSAT, GSAT with Walk, WalkSAT and Simulated Annealing for 3SAT problems. Your program should not take any arguments, and when executed, it should run the following experiment. Use your program to solve randomly generated 3SAT problems of different sizes. There are two key parameters: N, the number of propositional symbols, and C, the number of clauses. Investigate the effects of the C/N ratio on the execution time of your two algorithms. With N fixed at 20, record the average number of restarts and climbs used by GSAT, GSAT with Walk, WalkSAT, for C/N from 1 to 10. Record the average number of steps taken and the average temperature for Simulated Annealing for C/N from 1 to 10. Do not consider instances when your algorithms do not find solutions. Also record the number of times a solution is found. You should run your algorithms 20 times for each C/N ratio. Use N as the value of max-restarts and 5N as the value of max-climbs.

 

What to turn in for Part II

 

Create a directory called HW2 in your ~/CS540-handin/ directory, and put your Java files there. Also turn in a printout of your commented code and a neatly written lab report that includes the material and answers requested above for Part II. Answer the following questions: Is the GSAT algorithm sound? Is it complete? Report on your results, the difficulty of 3SAT problems for different values of C/N, which algorithm you believe worked better for this problem and why.

 

The GSAT, GSAT with Walk, WalkSAT algorithm are as follows:

 

Procedure GSAT(Sentence, MAX-TRIES, MAX-FLIPS)

Input: Sentence: a set of 3-clauses, and integers MAX-FLIPS, and MAX-TRIES.

Output: a satisfying truth assignment of Sentence, if any is found.

{

for i := 1 to MAX-TRIES:

{

T := a randomly generated truth assignment;

for j := 1 to MAX-FLIPS:

{

if T satisfies Sentence then return T;

for each variable v:

{

let MAKE[v] = the number of clauses currently unsatisfied

by T that would become satisfied if the truth value of

v were reversed ("flipped").

let BREAK[v] = the number of clauses currently satisfied

by T that would become unsatisfied if the truth value of

v were flipped.

let DIFF[v] = MAKE[v] - BREAK[v];

}

let MAX_DIFF_LIST = list of variables with the greatest DIFF;

v := a random member of MAX_DIFF_LIST;

T := T with the truth assignment of v flipped;

}

}

return "no satisfying assignment found";

}

 

GSAT is thus a "greedy" algorithm, that tries to flip variables so that as many clauses as possible are satisfied. Note that if the chosen variable p is such that DIFF[p] > 0, then the total number of unsatisfied clauses decreases. We call this a "downward" move. If DIFF[p] = 0, then the total number of satisfied clauses remains constant; we call this a "sideways" move. Finally, if the flipped variable has DIFF[p] < 0, then an "upwards" move is performed, in which the number of satisfied clauses decreases. We refer to each iteration of the inner loop as a "flip", and each iteration of the outer loop as a "try".
 
 

Procedure GSAT_RANDOM_WALK(Sentence, MAX-TRIES, MAX-FLIPS)
{

Input: Sentence: a set of 3-clauses, and integers MAX-FLIPS, and MAX-TRIES.

Output: a satisfying truth assignment of Sentence, if any is found.

for i = 1 to MAX-TRIES
{
T = a randomly generated truth assignment
for j = 1 to MAX-FLIPS
{
if T satisfies Sentence then return T
With probability p, pick a variable occurring in some
unsatisfied clause and flip its truth assignment.
With probability 1-p do the following:

for each variable v:

{

let MAKE[v] = the number of clauses currently unsatisfied

by T that would become satisfied if the truth value of

v were reversed ("flipped").

let BREAK[v] = the number of clauses currently satisfied

by T that would become unsatisfied if the truth value of

v were flipped.

let DIFF[v] = MAKE[v] - BREAK[v];

}

let MAX_DIFF_LIST = list of variables with the greatest DIFF;

v := a random member of MAX_DIFF_LIST;

T := T with the truth assignment of v flipped;
}
}
return "No satisfying assignment found"
}
 

  Procedure WALKSAT(Sentence, MAX-TRIES, MAX-FLIPS)

{

for i = 1 to MAX-TRIES

{

T = a randomly generated truth assignment

for j = 1 to MAX-FLIPS

{

if T satisfies Sentence then return T

else

{

Choose a random unsatisfied clause C. Select and flip a variable from that clause:

Denote C's variables x,y,z. Let t1,t2,t3 be the truth assignments obtained by toggling t on variables x,y,z, respectively. Whichever of t1,t2,t3 satisfies the most clauses, let T be that truth assignment. (Break ties arbitrarily.)

}

}

}

return "No satisfying assignment found"

}