Analysis of Algorithm for Solving CNF-SAT

------------CS575 Programming Assignment 4

Ruofei Zhang

Abstract

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.

1. Introduction and Problem Description

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.

2. GSAT Algorithm and Two Variations of It

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)

for i:=1 to Max-tries

T:= random truth assignment

for j:=1 to Max-flips

if T satisfies Form then

return T

else

Poss-flips:= set of vars which increase SAT most

V:= a random element of Poss-flips

T:= T with V’s truth assignment flipped

end

end

return “no satisfying assignment found”

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:
  2. 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.

  3. The pseudocode of GSATV2:

Procedure GSATV2(CNF-FORMULA Form)

T:= random truth assignment

for i:=1 to Max-tries

if T satisfies Form then

return T

C:= one randomly selected clause from unsatisfied clauses

V:= one randomly selected variable from clause C

T:= T with V’s truth assignment flipped

end

return “no satisfying assignment found”

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

3. Implementation of GSATV1 AND GSATV2

  1. The implementation of formula’s data structure

I implement the formula’s data structure by using a structure array:

/*The structure to store each literal in one clause */

typedef struct literal {

int flag; /* the flag of literal, 1: denotes + */

/* 0: denotes - */

int variable; /* variable ID */

}literal;

/* The structure to store each clause */

typedef struct clause {

int literalnumber; /* number of literals in this clause */

literal *pointtoliteral; /* the pointer points to the list of literals

/* in this clause */

}clause;

clause formula[MAX_CLAUSES_NUMBER]; /* formula, a array of clauses*/

2. The implementation of reading in the formula

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

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

/* read number of variables from test file */

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

/* read number of clauses from test file */

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

{

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

formula[i].pointtoliteral= new literal[temp_variable_counter];

formula[i].literalnumber=temp_variable_counter;

for(j=0;j<temp_variable_counter;j++)

{

fscanf(fp,"%s",inputliteral);

temp=strlen(inputliteral)-1;

for(k=0;k<=temp;k++)

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 */

3. Initialize the variable truth assignment by using randomizing

int initclause( int number, int *variableassign)

{ /* variableassign is the array storing assignment

/* value of variables */

int i;

/* Seed the random number generator function */

srand( (unsigned)time( NULL ) );

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

{

if(rand()%2==0)

variableassign[i]=1;

else

variableassign[i]=0;

printf("the %d variable is: %d\n", i,variableassign[i]);

}

return 0;

}

4. The implementation of satisfability checking in GSATV2

int checksat(int num_var,int num_clauses,int *variableassign, clause *form, int *unsatvar)

{

int truenumber=0;

int numunsat=0;

int findsat,trynum,tryvar;

int unsat[2000];

for(int i=0;i<num_clauses;i++) /* check satisfability of each clause */

{

findsat=0; /* the flag of whether one clause is true */

for(int j=0;j<form[i].literalnumber;j++)

{

if(variableassign[(form[i].pointtoliteral+j)->variable]==1)

{

if((form[i].pointtoliteral+j)->flag==1)

/*+v, and v is trure (1) */

{

findsat=1;

truenumber++;

break;

}

}

if(variableassign[(form[i].pointtoliteral+j)->variable]==0)

{

if((form[i].pointtoliteral+j)->flag==0)

/*-v, and v is false(0) */

{

findsat=1;

truenumber++;

break;

}

}

}

if(findsat==0) /* this clause is not satisfiable */

{

unsat[numunsat]=i;

numunsat++; /* the number of unsatisfiable clauses */

}

}

if(numunsat!=0)

{

srand( (unsigned)time( NULL ) );

trynum=rand() % numunsat;

/* randomly select one unsatisfiable clause */

tryvar=rand() % form[unsat[trynum]].literalnumber;

/* randomly select one variable in this clause */

*unsatvar=(form[unsat[trynum]].pointtoliteral+tryvar)->variable;

}

return truenumber;

}

4. Experiment Results and Performance Analysis

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):

Test File

Running time

GSATV2

Running time

GSATV1

Satprob0 (N=3, L=2)

<0 millsec

<0 millsec

Satprob1 (N=100, L=20)

50 millsec

150 millsec

Satprob2 (N=200, L=100)

160 millsec

530 millsec

Satprob3 (N=1000, L=200)

820 millsec

2300 millsec

Satprob4 (N=1000, L=600)

1820 millsec

5500 millsec

Satprob1a (N=4, L=3)

<0 millsec

30 millsec

Satprob2a (N=100, L=50)

110 millsec

530 millsec

Satprob3a (N=500, L=200)

770 millsec

2100 millsec

Satprob4a (N=1000, L=900)

6970 millsec

12200 millsec

Satprob5a (N=2000,L=1500)

13070 millsec

38000 millsec

Hardsat1 (N=100, L=500)

52500 millsec

Can’t find solution

Hardsat2 (N=200, L=1000)

183720 millsec

Can’t find solution

Hardsat3 (N=300, L=3000)

Can’t find solution

Can’t find solution

Hardsat4 (N=400, L=3000)

Can’t find solution

Can’t find solution

Hardsat5 (N=500, L=4000)

Can’t find solution

Can’t find solution

Because these two algorithms are randomized, the running time is slightly different in each test on a test file, so the figure of running time in above table is a mean value.

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):

Test File

Approximate probability of that first random truth assignment satisfies the formula

Satprob0 (N=3, L=2, M=2)

0.421

Satprob1(N=100, L=20, M=15)

0.999

Satprob2(N=200, L=100, M=5)

0.0418

Satprob3(N=1000, L=200, M=8)

0.457

Satprob4(N=1000, L=600, M=10)

0.556

Satprob1a(N=4, L=3, M=3)

0.670

Satprob2a(N=100, L=50, M=3)

1.260e-3

Satprob3a(N=500, L=200, M=3)

2.521e-12

Satprob4a(N=1000, L=900, M=3)

6.416e-53

Satrprob5a(N=2000, L=1500, M=3)

1.028e-87

Hardsat1(N=100, L=500, M=3)

1.009e-29

Hardsat2(N=200, L=1000, M=3)

1.019e-58

Hardsat3(N=300, L=3000, M=3)

1.057e-174

Hardsat4(N=400, L=3000, M=3)

1.057e-174

Hardsat5(N=500, L=4000, M=3)

1.077e-232

This probability is computed by supposing all literals truth assignment of literals in each clauses are independent, in fact, it’s not true in the test file cases. But when the number of variables is very large, the computation result is approximate to the precise probability value

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.

5. Conclusion

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.

Referenced books and papers

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 and hardware

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

Hardware: Pentium II 400MHZ, Memory 64M PC