Ruofei Zhang

In this report, I describe a study of CNF-boolean satisfiability (SAT) and two feasible algorithms for this NP-complete problem. These two algorithms are two variations of GSAT, an approximation procedure for solving SAT problem. The two algorithms I provided perform randomized greedy hill-climbing on the number of satisfied clauses in a truth assignment. In addition to the description of the two algorithms and the implementation approach of these algorithms, I also analyze the relation of hardness of problems and features of algorithms as well as the running performance on the test files.

An instance of boolean satisfiability (SAT) problem is a boolean formula φ composed of:

1. Boolean variables: x1, x2, ….;
2. Boolean connectives: any boolean function with one or two inputs and one output, such as Ù (AND), Ú (OR), ┐(NOT); and
3. Parentheses.

A truth assignment for a boolean formula φ is a set of values for the variables of φ, and a satisfying assignment is a truth assignment that causes it to evaluate 1. A formula with a satisfying assignment is a satisfiable formula. The SAT problem asks whether a given boolean formula is satisfiable; If the formula is satisfiable, then we should find a boolean value assignment for the set of variables in the formula, such that the output of this formula is true. For example, if we have (A+B)(!A+C), we could satisfy this equation with A=true, B=don't-care, C=true.

The naive algorithm to determine whether an arbitrary boolean formula is satisfiable does not run in polynomial time. There are possible assignments in a formula φ with n variables. If the length of <φ> is polynomial in n, then checking every assignment requires superpolynomial time. In fact, it is proved that satisfiablility of boolean formulas is NP-complete, in other word, a polynomial-time algorithm is unlikely to exist. Among the research and applications of SAT problems, the most attractive and representative problem is CNF-SAT. In this report, I will discuss algorithms exactly for CNF-SAT problem. First we define CNF-SAT using the following terms:

1. A literal in a boolean formula is an occurrence of a variable or its negation.
2. A boolean formula is in conjunctive normal form, or CNF, if it is expressed as an AND of clauses, each of which is the OR of one or more literals.

For example, the boolean formula is in CNF.

There has been considerable interest in the CNF-SAT problem of propositional logic since this problem was noted by people. Because the CNF-SAT problem is fundamental to many practical problems in mathematics, computer science, and electrical engineering, efficient methods that can solve a large subset of CNF-SAT problems are eagerly sought. Empirical research has been very fruitful for the development of efficient methods for CNF-SAT problems, such as classical Davis-Puthnam method, greedy SAT (GSAT) method and neural network SAT method, etc. The two algorithms studied and implemented for solving CNF-SAT problem in the report are variations of GSAT method, a randomized hill-climbing procedure.

The rest of the report is organized as follows. First I describe the GSAT algorithm and its two variations in Section 2. Sections 3 provides the implementation approach of the pertinent algorithms. Experimental results and performance analyses as well as features of hard problems are shown in Section 4. And finally I finish my report by conclusion in section 5.

GSAT is a randomized hill-climbing procedure, it deals with CNF formula. GSAT starts with a randomly generated truth assignment, then hill-climbs by “flipping” the variable assignment which gives the largest increase in the number of clauses satisfied (called the “score” from now on). Given the choice between several equally good flips, GSAT picks one at random. If no flip can increase the score, then a variable is flipped which does not change the score or (failing that) which decreases the score least. Thus GSAT starts in a random part of the search space and searches for a global solution using only local information, in other word, it’s a greedy algorithm. Despite its simplicity, this procedure has been shown to give good performance on hard satisfiability problems. The pseudocode of GSAT algorithm is shown as follows:

Procedure GSAT(CNF-FORMULA Form)

Many variations and improvements of GSAT are emerging, as it appears to be able to solve large and difficult satisfiability problems beyond the range of conventional procedure like Davis-Putnam algorithm. These variations all improve the performance of GSAT algorithm in different degree. In this project, I implement and analyze two variations of GSAT, which will be denoted as GSATV1 and GSATV2 in the following parts.

1. The pseudocode of GSATV1:

Procedure GSATV1(CNF-FORMULA Form)

T:= random truth assignment

for i:=1 to Max-tries

if T satisfies Form then

return T

for j:=1 to Max-flips

V:= one randomly selected variable

T:= T with V’s truth assignment flipped

end

Find most increasements of satisfiability in these Max-flips flipping and set T as such pattern

end

return “no satisfying assignment found”

The purpose of this variation is to increase the number of flipping variables in each round of flipping (at most Max-flips) compared with GSAT algorithm (which flip only one variable in each round of flipping). This variation is thought out by me because I wish by increasing number of variables flipped each time we can improve the search performance in some degree. In later section I will show its efficiency on solving problems of test files.

2. The pseudocode of GSATV2:

Procedure GSATV2(CNF-FORMULA Form)

This variation of GSAT is based on that we just flip one variable in a randomly selected unsatisfied clause because by this means this clause will change to true and we wish so the number of satisfiable clauses would increase.

Another important fact is that all GSAT-based algorithms are not complete. That is, each of these algorithms cannot say whether a given statement has a solution or not -- it is possible that it 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. Although GSAT-based algorithms are not complete, they are still effective methods to solve most CNF-SAT problems

/* The structure to store each clause */

fp=fopen("satprob4.txt","r"); /* open the data file */

fscanf(fp,"%d",&num_of_variables);

fscanf(fp,"%d",&num_of_clauses);

for(i=0;i<num_of_clauses;i++) /* read each clauses in */

templiteral[k]=inputliteral[k+1];

if(inputliteral[0]=='+')

(formula[i].pointtoliteral+j)->flag=1;

else

(formula[i].pointtoliteral+j)->flag=0;

(formula[i].pointtoliteral+j)->variable=atoi(templiteral);

}

}

fclose(fp); /* close the test file */

int initclause( int number, int *variableassign)

{ /* variableassign is the array storing assignment

/* value of variables */

srand( (unsigned)time( NULL ) );

for(i=1;i<=number;i++)

I tested the GSATV1 and GSATV2 algorithm many times on 15 test files provided by professor Madden (satprob0~4, satprob1a~5a, hardsat1~5). The experiment results are shown as follows (N denotes number of variables, L denotes number of clauses):

We can see from the table that the performance of GSATV2 is better than GSATV1, that’s because the GSATV1’s variable selection is more effective. It purposely select one random variable in an unsatisfiable clause to toggle, this may improve the search very well. On the other hand, although GSATV1 toggle several variables in one round of flipping, the effect seems not satisfactory. I think that is because in most test files there are only 3-5 literals in one clause, so randomly select several (such as 6) variables to flip together doesn’t do well. The search may retain in the “plateau” phase for a long time.

Another notable point I want to mention is the hardness of these test files. The approximate probability of the case that first random truth assignment will satisfy the formula is shown as follows, this probability is one of factors to evaluate the hardness of these test files (M is the mean number of literals in one clause):

We can see from this table that satprob0~satprob4 test files is rather easier than other test files because their number of literals in each clause is bigger.

In addition, from the table of running time for each test files we can also see that problems in random M-SAT with N variables, L clauses and M variables in each clause have following features on satisfiability: At lower L, most such problems are under-constrained and are thus satisfiable; at higher L, most problems are over-constrained and are thus unsatisfiable. It has been proved that for random 3NF-SAT, there is a phase transition from satisfiable to unsatisfiable when L is approximately 4.3N. So problems in the phase transition are typically much more difficult to solve than problems away from the transition. This point can be seen clearly by our running results. The region L>=4.3N (as the formula shown in hardsat* test file) is thus generally considered to be a good source of hard SAT problems and has been the focus of much experimental effort.

We can note from the experiment result of GSATV1 and GSATV2 program that search in each try is divided into two phases. In the first phase of a try, each flip increases the score. However, this phase is relatively short and is followed by a second phase in which most flips do not increase the score, but are instead sideways moves which leave the same number or just decrease the number of clauses satisfied. At the same time, by performing many times of experiment, we can see that neither greediness nor randomness is very important for the performance of the GSATV* algorithm, the performance seemed to be relatived tightly with problem size and pattern.

In this report, I describe a study of CNF-SAT and two feasible GSAT variation algorithms for this NP-complete problem. The two algorithms I provided perform randomized greedy hill-climbing on the number of satisfied clauses in a truth assignment. Although they both are based on GSAT method, they have prominent differences in the selection of variables to be flipped and in the heuristic method. In addition, the implementation approach of these algorithms is given. I also analyze the relation of hardness of problems and features of algorithms as well as the running performance on the test files. From the analysis and implementation of these two greedy algorithms, we can see that they are usually effective for most CNF-SAT problems, even for the hard CNF-SAT problems, although they are incomplete.

1. Introduction to Algorithms  Thomas H. Cormen, MIT Press

2. An Empirical Analysis of Search in GSAT Lan P. Gent, Toby Walsh

3. Efficient Generation of Test Patterns Using Boolean Satisfiability Tracy Larrabee

4. Simulated Annealing for Hard Satisfiability Problems William M. Spears

Compiler: Visual C++ 6.0 on Windows 98 operating system;