Theoretical Analysis of Davis-Putnam Procedure and Propositional Satisfiability

1 Introduction

This paper presents a statistical analysis of the Davis­ Putnam procedure [Davis and Putnam, 60] that solves propositional satisfiability problems (SAT}. SAT is the problem to judge whether a given logical formula, given as a conjunctive normal form (cnf}, can be satisfied or not. It has been researched in AI because of its strong relationship to automated reasoning such as theorem proving arrl planning. Recently, it is also concerned as a benchmark problem for constraint satisfaction algorithms [Selman, Levesque and Mitchell, 92][Yugami, Ohta and Hara, 94]. The Davis-Putnam procedure is one of the most famous algorithms for SAT.

A number of papers discussed the difficulty of SAT theoretically. Because of its NP-completeness, SAT requires more than polynomial time in the worst case, assuming NP#P, and the analysis of SAT concentrated on the average case behavior. Goldberg et. al. showed that the Davis­ Putnam procedure, on average, could solve SAT in polynomial time of the number of variables [Goldberg, Purdom and Brown, 82]. They assumed the constant probability model as a distribution model of formulas to be tested. Franco and Paull pointed out that this easiness of SAT strongly d:pended on the distribution model ani proposed a new distribution model, the fixed clause length model [Franco and Paull, 83][Franco, 86]. They showed that the Davis-Putnam procedure required exponential time for finding all solutions, assignments that satisfied the given formula, on this distribution model [Franco and Paull , 83][Franco, Plotkin and Rosenthal, 87]. This result is relevant to the original SAT, satisfiability checking, when few assignments satisfy the formula. Chao and Franco showed that the Davis-Putnam procedure with the unit clause rule could solve SAT without backtracking, i.e. it required only polynomial time on the fixed clause length model with a small clauses-to-variables ratio (smaller than 2.9 for 3-SAT}. [Williams and Hogg, 94] analyzed the difficulty of general constraint satisfaction problems by using the structure of the assumption lattice. Recent experimental works showed more precise results of the average case behavior of the Davis-Putnam procedure. Mitchell et. al . reported the dependency of the Davis-Putnam procedure's average case complexity on the clauses-to­ variables ratio and showed its drastic change near the 50% satisfiable point [Mitchell , Selman and Levesque, 92]. The complexity became maximum near the 50% satisfiable point and decreased rapidly when the ratio became larger or smaller. [Crawford and Auton, 93] reported similar results by using tableau based satisfiability checking algorithm.

The purpose of this paper is to analyze the Davis­ Putnam procedure's average case behavior on the fixed clause length model, especially its dependency on the clauses-to-variables ratio. I discuss two complexities, the complexity for satisfiability checking and the complexity for finding all solutions . I also discuss the probability of satisfiability.

The organization of this paper is as follows . I first review the Davis-Putnam procedure and the fixed clause length model in the following two sections. Section 4 gives the statistical analysis of the average case complexities arrl the probability of satisfiability. The results of section 4 are compared with experimental results in section 5. I summarize my results in section 6.

2 Davis-Putnam Procedure

Figure 1 shows the Davis-Putnam procedure (DP). It takes a cnf as an input and returns whether the cnf is "satisfiable" or "unsatisfiable". It solves SAT by searching an assignment that satisfies all clauses. DP uses the unit propagation (unit clause rule) to improve its performance. The unit propagation selects a variable in an unit clause, a clause containing a single literal, and assigns a value to the variable to satisfy the clause. In the original DP, the pure literal rule is also used to improve DP, but I ignore it in this paper because the unit propagation is much more powerful.

I use the number of DP calls as the complexity of DP. I modify DP to simplify the analysis. Figure 2 shows the modified procedure, SDP. The only difference between DP and SDP is that SDP does not check whether all clauses are satisfied or not. It finds all clauses are satisfied when all variables are bound and no empty clause exists. The difference is not essential because if a partial assignment satisfies all clauses, then no backtrack occurs after that. This means that the number of SDP calls for satisfiability checking is larger than the number of DP calls by at most the number of variables and usually the difference is very small. For finding all solutions, there is no difference betweenDP andSDP.

3 The Fixed Clause Length Model

The complexity of SDP, and DP, strongly depends on the distribution of cnfs to be tested. It this paper, I use the fixed clause length model as the distribution model. This model has three parameters, the number of variables, N, the clause length, K and the number of clauses, M . A cnf on this model consists of M clauses a:O.d each clause contains K literals. In a clause, each variable appears at most once. A formula to be tested is randomly selected from the set of all cnfs that satisfy these conditions. The important feature of this model is that the clauses in the cnf are mutually independent. SAT on the fixed clause length model with clause length K, is calledK-SAT.

4 Analysis

4.1 Probabilities of becoming empty and unit

On K-SAT, a clause contains K literals first and becomes satisfied or becomes shorter when SDP assigns values to variables incrementally. In SDP, an empty clause and an unit clause perform important roles. I first discuss the probabilities of becoming empty or unit when b variables are bound and r variables are removed. "Remove a variable" means deleting both of positive and negative literals of the variable from the cnf. SDP, and DP, does not do such a thing but I will use removed variables to discuss the

procedure D P

Input : A cnf to be tested

Output : "satisfiable" or "unsatisfiable"

step 1 : Unit Propagation

While there is no empty clause and an unit clause exists, select an unit clause and bind a variable in it to satisfy it.

step 2 : Satisfiability Checking

If all clauses are satisfied, return "satisfiable".

step 3 : Unsatisfiability Checking

If an empty clause exists, return "unsatisfiable".

step 4 : Splitting Rule

Select a variable whose value is not assigned. Assign true to it and call DP. If the result is "satisfiable" then return "satisfiable". Otherwise, assign false to the variable and call DP again. Return the result of it.

Figure 1: Davis-Putnam Procedure

procedure S D P

Input : A cnf to be tested

Output : "satisfiable" or "unsatisfiable"

step 1 : Unit Propagation

While there is no empty clause and an unit clause exists, select an unit clause and bind a variable in it to satisfy it.

step 2 : Unsatisfiability Checking

If an empty clause exists, return "unsatisfiable".

step 3 : Satisfiability Checking

If all variables are bound, return "satisfiable".

step 4 : Splitting Rule

Select a variable whose value is not assigned. Assign true to it and call SDP. If the result is "satisfiable" then return "satisfiable". Otherwise, assign false to the variable and call SDP agam.

• Return the result of it.

Figure 2: SDP, a variant of Davis-Putnam Procedure

probability of satisfiability. For simplicity, I use "at (b,r)" to represent "when b variables are bound and r variables are removed". Letpe(b,r) be the probability of becoming empty at (b,r) . A clause becomes empty when all variables in it are bound or removed and values of bound variables violate the corresponding literals. Thus the desired probability is

Where, n is the number of bound variables in the clause am K- n variables in the clause are removed. The probability of becoming unit can be obtained by the same way. 1be only difference is that the clause contains one variable that is not bound nor removed. If b + r = N orb+ r s K- 2 , the probability is 0 and otherwise,

Next, I discuss the transition probabilities from unit clause to empty clause, unit clause to unit clause and so on. An unit clause becomes empty if the variable of the remaining literal in it is bound and the assigned value violates the literal, or the variable is removed. Thus a clause that is unit at (bl'ri) becomes empty at (b 2 ,r 2 ) (bisb 2 , 'I sr 2 ) with probability

The probability that an unit clause at (bi ,ri) is also unit at (b 2 ,r 2 ), Pu-+u(q,ri,bz,r2 ), and the probability of becoming satisfied at (b 2 ,r 2 ), Pu-+s(ht, '~> bz ,r2 ), can be calculated by the same way.

Let Po-+e (bi, 'I ,b2 , r2 ) be a probability that a clause, which is not empty nor unit at (hi ·'I), becomes empty at (b 2 ,r 2 ). Because a clause is not empty nor unit at (bi,ri) with probability 1 - Pe(bi, 'i)-Pu (bi, ri),

Especially,

because a value assignment to one variable can make a new empty clause only from an unit clause.

The probability of becoming unit can be calculated with the similar discussion.

For simplicity, I will use the following notations.

4.2 Unit Propagation

The effectiveness of SDP, and DP, is mainly based on the unit propagation. In this subsection, I discuss the statistical behavior of the unit propagation when SDP is called with b bound variables and u (sb) of them are bound by the unit propagation. Because SDP calls SDP recursively only in the splitting rule, there is no empty nor unit clause when b - 1 variables are bound. The number of variables whose values are assigned by the unit propagation, u, means u clauses selected for the unit propagation must be satisfied.

To analyze the statistical behavior of the unit propagation, I discuss three probabilities, the probability that the unit propagation binds at least l::!..u variables, Punir(b,u,l::!..u), the probability that SDP detects an empty clause after the unit propagation binds l::!..u variables, PJail(b,u,l::!..u), and the probability that the unit propagation terminates after binding l::!..u variables because there is no unit clause nor empty clause,psplit(b,u,l::!..u) . Because of their definitions, they relate to each other through the following equations.

When l::!..u=O, i.e. when SDP is called, a clause that is not selected for the unit propagation before the current SDP is called, becomes unit with probability Po-+u (b) and does not become empty because Po-+e(b -1,0,b,O) = 0 . Thus,

If b s K - 2 , all unsatisfied clauses contain at least two literals and the unit propagation can not find an unit clause. SDP must apply the splitting rule (there must be an unbound variable because N <!: K) and the probabilities for the unit propagation are

I assume b ~ K -1 in the remaining part of this subsection.

When !1u :2:1 , Ptail andpsplit dependon the number of unit clauses after the previous variable binding in the unit propagation. Let n be the number of unit clauses after the unit propagation binds L1u -1 variables. The unit propagation selects one of n unit clauses and binds the variable in it to satisfy it. This value assignment may make a new empty clause from the remaining n -1 unit clauses. Because each unit clause becomes empty with probability Pu-+e (b + L1u) ,

Where, Pnum (b, u, L1u -1, n) is the probability that there are n (~ 1) unit clauses after the unit propagation binds L1u -1 variables on the conditions that there is no empty clause and there is at least one unit clause, i.e. on the condition that the unit propagation binds one more variable.

The probability that there is no empty nor unit clause, Pspz;t<b,u,!1u), can be obtained as follows . To remove the remaining n -1 unit clauses, the variable binding for the selected unit clause must satisfy all of them and the binding must not make a new unit clause from M- u- (L1u -1)- n non-unit clauses (u clauses are already satisfied by the unit propagation before the current SDP is called, L1u -1 are satisfied by the unit propagation .in the current SDP and n are unit now). Thus, Psplit(b,u,!1u) is

The remaining problem is to obtain the probability Pnum(b,u, L1u -1,n) . I calculate it as a recursion formula with respect to !1u. As I mentioned above, I need to calculate it on the conditions that no empty clause exists and at least one unit clause exists. Thus, a clause that is unit after the unit propagation binds L1u -1 variables, is also unit after the /1uth binding with probability

The probability that there are n 1 unit clauses after the !1uth binding in the unit propagation on the condition that there are n (:2:1) unit clauses before the binding, is

Where, m is the number of clauses that are unit before the !1uth variable binding in the unit propagation and also unit after the binding. This means that the variable binding causes n 1 -m new unit clauses. The range of m is

This probability leads the following recursion formula.

The denominator is a correction for the condition that there is at least one unit clause. When 11u=0, i.e. when the unit propagation starts, Pnum is

because all of M- u clauses, that are not selected for the unit propagation before the current SDP is called, are not empty nor unit when the splitting rule is applied and the value assignment to one variable by the splitting rule can not make an empty clause.

As a result, Pnum can be obtained from (8}--(9) and with this probability, I can obtain the probabilities, Pun it· Ptail arrl Psplit that decide the statistical behavior of the unit propagation from (1)-(6).

4.3 After the Unit Propagation

What happens after the unit propagation finishes? There are three possibilities, returning "unsatisfiable" because an empty clause exists, returning "satisfiable" because no empty clause exists and all variables are bound, and applying the splitting rule. The definitions of Punit· Ptail and Psplit leal the probabilities of these three cases as follows .

The unit propagation step binds !:J.u variables and SDP

4.4 Average Case Complexities

In this subsection, I discuss two average case complexities, the complexity for satisfiability checking and the complexity for finding all solutions . I use the number of SDP calls as the complexity.

Let tscheck(b,u) and tsau(b,u) be the SDP's complexity for satisfiability checking and the complexity for finding all solutions when SDP is called with b bound variables and u of them are bound by the unit propagation. SDP calls SDP recursively only in the splitting rule and, for satisfiability checking, the splitting rule calls the second descendant SDP only when the first one returns "unsatisfiable". Thus,

Where, Psnp(b,u) is the probability that SDP returns "satisfiable" when it is called with b bound variables and u of them are bound by the unit propagation. I discuss this probability in the next subsection. For finding all solutions, the splitting rule always calls the second descendent SDP.

These two recursion formulas reduce the complexities of SDP with N- b unbound variables to the complexities with less number of unbound variables. When b=N, i.e. when all variables are bound, SDP does not apply the splitting rule am

When SDP is called first, i.e. when no variable is bound, the unit propagation does not bind a variable because a cnf on K-SAT (K:?:2) does not contain an unit clause. SDP applies the splitting rule and the complexity of each descendant SDP is tscheck(1,0) or tsau(1,0). Thus the average case complexities forK-SAT are

4.5 Probability of Satisfiability

This subsection discuss the probability, Psnp(b,u), that SDP returns "satisfiable" when it is called with b bound variables and u of them are bound by the unit propagation. The probability is, of course, a probability that the cnf with the partial value assignment to b variables is satisfiable.

Let Ps(b 1 ,upb 2 ,r 2 ) be the probability that the cnf with b 2 bound variables and r 2 removed variables is satisfiable on the conditions that the cnf does not contain an empty nor unit clause and contains at least u 1 satisfied clauses when b 1 variables are bound and no variable is removed. Because SDP applies the splitting rule and calls SDP recursively only when there is no empty nor unit clause, the probability of returning "satisfiable" is

When b 2 + r 2 < N , let x be a variable that is not bound nor removed. The cnf with b 2 bound variables and r 2 removed variables, is satisfiable iff one of the two cnfs, the cnf generated by assigning true to x and the cnf generated by assigning false to x, is satisfiable. Because of the definition of Ps· each of the two cnfs is satisfiable with probability P.(bl'ul'b 2 + 1 ,r 2 ) . To obtain Ps(bl'ul'b 2 ,r 2 ), I need the probability that both of the two cnfs are satisfiable. It is very difficult to calculate it and I approximate it with its lower bound, the probability that the two cnfs share an assignment that satisfies both of them. In other words, the lower bound is the probability that the conjunction of the two cnfs is satisfiable. The conjunction is generated by removing x from the cnf and the lower bound is Ps(b 1 ,u 1 ,b 2 ,r 2 + 1). This is the reason I introduced "removed variables" to the analysis. The above discussion leads the following recursion formula.

When b2 + r2 = N, i.e. when all variables are bound or removed, a clause in the cnf is satisfied with probability 1-Po-+e(b1 ,0.~.r2) am

The probability, Psnp(b,u), can be obtained from (14}--(16).

Because a cnf generated on K-SAT (K2:.2) contains neither empty nor unit clause, the probability of satisfiability forK-SAT is

4.6 The complexity for computing complexities

It is not so easy to calculate the complexities with the result of this section because the result contains many recursion formulas. The bottleneck of the computation is to calculate p1 ( b, u, L1u, n, n'). It requires O(M) time to compute p 1 for the given b, u, flu, n, n' am O(N 2 M 3 ) to compute all elements of p 1 because of the following relation.

It is polynomial time but not practical when N and M are large. But we don't need to calculate all elements of p 1 because many of them are probabilities for very rare possibilities. For example, when b, u, flu and n are fixed, the average of n' is

and the standard deviation is

The approximation, p 1 ( b, u, L1u, n, n' ) = 0 , is reasonable when kn'- < n' >) I SDI is large.

Another reasonable approximation is ignoring the probabilities of the unit propagation for large D.u. Because P . (b u D.u) monotonically decreases with respect to D.u, if umt ' ' P . (b u D.u) becomes very small, the approximation untt ' '

does not affect the result. This approximation also decreases the number of elements of p 1 to be calculated and shortens the computation time.

5 Comparison with Empirical Results

Figure 3 and 4 show the statistical and empirical results of the probability of satisfiability, Psatisfiable· the complexity for satisfiability checking, a:check· and the complexity for finding all solutions, a:a/1' for 3-SAT and 4-SAT with 50 variables. The complexities are the number of SDP calls that are required for satisfiability checking and for finding all solutions . The empirical results were obtained by solving randomly generated 1,000 problems at each clauses-to­ variables ratio for 3-SAT and by solving 100 problems at each ratio for4-SAT.

The probability of satisfiability coincided with the empirical result well. The 50% satisfiable points by the statistical analysis (4.6 for3-SAT and 10.4 for 5-SAT) were a little larger than the empirical results (4.3 for 3-SAT ard 10.0 for 4-SAT). This difference is caused by the approximation I used for calculating the recursion formula for Ps· The approximation makes Ps larger than the real value and causes the overestimation of PsDP andpsatisfiabze·

The complexity for finding all solutions coincided with the empirical result very well at all clauses-to-variables ratios. On the other hand, the complexity for satisfiability checking coincided with the empirical result above the 50% satisfiable point, but became smaller than the experimental result bellow the point. It became maximum near the 50% satisfiable point and the statistical results at the peak (532 for 3-SAT and 29,500 for 4-SAT) were about 20% smaller for 3-SAT and about 15% smaller for 4-SAT than the empirical results (671 for 3-SAT and 34,700 for 4-SAT). These results suggests that the analysis of the unit propagation, that are commonly used for both of two complexities, gives the accurate result. The overestimation of PsDP decreases the probability of calling the second descendant SDP and decreases the complexity for satisfiability checking. Above the 50% satisfiable point, the statistical prediction for satisfiability checking coincided with the empirical result because PsoP becomes very small and the approximation for it does not affect the statistical result.

6 Conclusions

In this paper, I analyzed the average case behavior of the Davis-Putnam procedure on the fixed clause length model. The analysis included two average case complexities, the complexity for satisfiability checking and the complexity for finding all solutions. I also discussed the probability of satisfiabili ty.

The results, especially the complexity for finding all solutions, coincided with experimental results well . The complexity for satisfiability checking coincided with experiments above the 50% satisfiable point but became smaller below the point because of the overestimation of the probability that a cnf with a partial assignment is satisfiable.