The representation of the set of falsifying assignments of clauses via binary patterns has been useful in the design of algorithms for solving #FAL (counting the number of falsifying assignments of conjunctive forms (CF)). Given as input a CF formula F expressed by m clauses de ned over n variables, we present a deterministic algorithm for computing #SAT (F ). Initially, our algorithm computes non-intersecting subsets of falsifying assignments of F until the space of falsifying assignments de ned by F is covered. Due to #SAT(F ) = 2n-#FAL(F ), results about #FAL can be established dually for #SAT. The time complexity of our proposals for computing #SAT(F ) is established according with the number of clauses and the number of variables of F .
The problem of counting models for a Boolean formula (#SAT problem) can be reduced to several problems in approximate reasoning. For example, estimating the degree of belief in propositional theories, generating explanations to propositional queries, repairing inconsistent databases, Bayesian inference and truth maintenance systems [1, 9{11]. The above problems come from several AI applications such as planning, expert systems, approximate reasoning, etc.
The combinatorial problems that we are going to address are the computation
of the number of models and falsifying assignments for Boolean formulas in
Conjunctive Forms (CF), denoted as #SAT and #FAL respectively, based on
string patterns formed by its set of falsifying assignments. Both problems are
classical #P -complete problems even for the restricted cases of monotone and
Horn formulas. We generalize the approach presented in [
Among the class of #P-complete problems, #SAT is considered a fundamental instance due to both its application in deduction issues and its relevance to establish a boundary between e cient and intractable counting problems.
Given a 2-CF F with n variables and m clauses, it is common to analyze
the computational complexity of the algorithms for solving #SAT and #FAL
regarding to n or m or any combination of both [
In [
Since #SAT (F ) = 2n #F AL(F ), it is the case that analogous results can be proved for #SAT (F ) and #F AL(F ). In this paper, we present a method for compute #FAL(F ) in an incremental way with respect to the set of clauses in F . Some reductions among clauses are presented, as subsumed clauses and the independent reduction, in order to accelerate the computation of #FAL(F ).
The paper is organized as follows. In Section 2 we give the basic notation as well as several de nitions. In Section 3 we describe the binary pattern based approach for 2-CF cases, and we extend such approach for CF cases. Section 4 provides the algorithm associated with our proposal. Section 5 concludes. 2
Let X = fx1; : : : ; xng be a set of n Boolean variables. A literal is either a variable xi or a negated variable xi. As usual, for each xi 2 X, xi0 = xi and xi1 = xi.
A clause is a disjunction of di erent and non-contradictory literals (sometimes, we also consider a clause as a set of literals, e.g. x1 _ x2 = fx1; x2g). For k 2 IN , a k-clause is a clause consisting of exactly k literals. A variable x 2 X appears in a clause c if either x or x is an element of c.
A conjunctive form (CF) F is a conjunction of non-tautological clauses. We say that F is a monotone positive CF if all of its variables appear in unnegated form. A k-CF is a CF containing only k-clauses. ( k)-CF denotes a CF containing clauses with at most k literals. A 2-CF formula F is said to be strict only if each clause of F consists of two literals. The size of a formula F is de ned as the sum of the number of clauses and variables of F .
We use (X) to represent the variables involved in the object X, where X could be a literal, a clause or a CF. For instance, for the clause c = fx1; x2g, (c) = fx1; x2g. Lit(F ) is the set of literals involved in F , i.e. if X = (F ), then Lit(F ) = X [ X = fx1; x1; :::; xn; xng. We denote f1; 2; :::; ng by [[n]] and the cardinality of a set A by jAj.
An assignment s for F is a function s : (F ) ! f0; 1g. An assignment s can also be considered as a set of literals without a complementary pair of literals, e.g., if l 2 s, then l 62 s, in other words s turns l true and l false or viceversa. Let c be a clause and s an assignment, c is satis ed by s if and only if c \ s 6= ;. On the other hand, if for all l 2 c, l 2 s, then s falsi es c. If n = j (F )j, then there are 2n possible assignments de ned over (F ). Let S(F ) be the set of 2n assignments de ned over (F ).
Let F be a CF, F is satis ed by an assignment s if each clause in F is satis ed by s. F is contradicted by s if any clause in F is falsi ed by s. A model of F is an assignment for (F ) that satis es F . A falsifying assignment of F is an assignment for (F ) that contradicts F . The SAT problem consists of determining whether F has a model. SAT(F ) denotes the set of models of F , then SAT(F ) S(F ). The set FAL(F ) = S(F ) n SAT (F ) consists of the assignments from S(F ) that falsify F .
The #SAT problem (or #SAT(F ) problem) consists of counting the number of models of F de ned over (F ), while #F AL(F ) denotes the number of falsifying assignments of F . Thus, #FAL(F ) = 2n- #SAT(F ) and #2SAT denotes #SAT for 2-CF formulas.
A 2-CF F can be represented by an undirected graph, called the constrained graph of F , and determined as: GF = (V (F ); E(F )), where V (F ) = (F ) and E(F ) = ff (x); (y)g : fx; yg 2 F g. I.e. the vertices of GF are the variables of F , and for each clause fx; yg in F there is an edge f (x); (y)g 2 E(F ).
The neighborhood for x 2 V (F ) is N (x) = fy 2 V (F ) : fx; yg 2 E(F )g and its closed neighborhood is N (x)[fxg denoted as N [x]. The degree of a variable x, denoted by (x), is jN (x)j, and the degree of F is (F ) = maxf (x) : x 2 V (F )g. The size of the neighborhood of x, (N (x)), is (N (x)) = Py2N(x) (y).
An algorithm to compute #SAT (F ), considers the set of connected components of its constrained graph GF . It has been proved that the set of connected components of a constrained graph can be determined in linear time with respect to the number of clauses in the formula.
Thus, #SAT (F ) = #SAT (GF ) = Qk
i=1 #SAT (Gi); where fG1; : : : ; Gkg is
the set of connected components of GF [
The set of connected components of GF conforms a partition of F . So, from now on, we will work with a formula F represented by just one connected component. 3
Let F = fC1; C2; : : : ; Cmg be a strict 2-CF (each clause has length 2) and let n = j (F )j. The size of F is n+m. Let k be a positive integer parameter such that k < 2n. The values of k, where #SAT(F ) = k, can be determined in polynomial time in the following cases.
If k = 0 or k = 1 the Transitive Closure procedure presented in [
If k is upper bounded by a polynomial function on n, e.g. k p(n), then
in [
So, the hard cases to answer whether #SAT(F ) = k are given when k > p(n).
In [
Theorem 1. [
Lemma 1. [
It is known [
Lemma 2. [
Binary patterns have been introduced to represent the set of falsifying assignments of any clause de ned on n variables. Those patterns allow us to design e cient procedures for computing #FAL(F ).
Let F = fC1; : : : ; Cmg be a 2-CF and n = j (F )j. Assume an enumeration over the variables of (F ), e.g. x1; x2; : : : ; xn. For each clause Ci = fxj ; xkg, let Ai be a set of binary strings of length n such that the values at the j-th and k-th positions of each string, 1 j < k n, represent the truth value of xj and xk that falsi es Ci. E.g., if xj 2 Ci then the j-th element of Ai is set to 0. On the other hand, if xj 2 Ci then the j-th element of Ai is set to 1. The same argument applies to xk. It is easy to show that if Ci = fxj ; xkg, then xj and xk have the same values in each string of Ai in order to be a falsifying assignment of F . Those variables not contained in the clause can take any truth value since the clause has been already falsi ed.
Example 1. Let F = fC1; C2g be a 2-CF and j (F )j = 3. If C1 = fx1; x2g and C2 = fx2; x3g then A1 = f000; 001g and A2 = f000; 100g.
We will use the symbol to represent the variables that can take any truth value in the set Ai, e.g. if F = fC1; : : : ; Cmg is a 2-CF, n = j (F )j, C1 = fx1; x2g and C2 = fx2; x3g then we will write A1 = 00 : : : and A2 = 00 : : : . This | {nz } | {nz } abuse of notation will allow us to present a concise and clear representation in the rest of the paper, for considering the string Ai as a binary pattern that represents the set of falsifying assignments of the clause Ci.
We de ne falsifying string as a binary pattern Ai which represents the set of
falsifying assignments of Ci. Let F = fC1; : : : ; Cmg be a 2-CF, n = j (F )j, we
denote by F als String(Ci) the procedure which constructs the falsifying string
(with n symbols) of Ci. Given a falsifying string Ai, the positions where 0 or 1
appear in Ai are called the xed values of the string, while the positions where
the symbol appears are called the free values of the string. We de ne the string
representing the null clause as the full string : : : .
| {z }
n
Lemma 3. [
We propose to generalize the previous de nitions and results to any CF and then consider #SAT and #F AL problems for CF formulas in general, not only the 2-CF cases. We consider now any CF without restriction on the length of its clauses.
De nition 1. [
De nition 1 can be written in terms of falsifying strings as follows: De nition 2. Given two falsifying strings A and B both of the same length, if there is an i such that A[i] = x and B[i] = 1 x, x 2 f0; 1g, it is said that they have the independence property. Otherwise, we say that both strings are dependent.
De nition 3. Let F = fC1; C2; Cmg be a CF. F is called independent if each pair of clauses Ci; Cj 2 F; i 6= j, has the independence property, otherwise F is called dependent.
Let F = fC1; C2; Cmg be a CF, n = j (F )j. Let C be a clause in F and x 2 (F ) n (C) be any variable, we have that
C = (C _ x) ^ (C _ x) (1)
Furthermore, this reduction preserves the number of falsifying assignments of C with respect to F , since #F AL(C) = 2n jCj = 2n (jCj+1) + 2n (jCj+1) = #F AL((C _ x) ^ (C _ x)), because (C _ x) ^ (C _ x) are two independent clauses. In terms of falsifying strings, let F = fC1; C2; : : : Cmg, n = (F ), if A is the falsifying string of a clause Cj such that there is an index i; A[i] = then the falsifying string A can be replaced by two falsifying strings say A1 and A2 as follows: 1. A1[j] = A[j] if j 6= i and A1[j] = 1 if j = i. 2. A2[j] = A[j] if j 6= i and A2[j] = 0 if j = i.
It is easy to show that the falsifying assignments represented by A with respect to F are equal to the sum of the falsifying assignments represented by A1 and A2 with respect to F .
Given a pair of dependent clauses C1 and C2. Let us assume that there are literals in C1 which are not in C2, let x1; x2; :::; xp be these literals. There exists a reduction to transform C2 to be independent with C1, we call at this transformation the independent reduction, and this works as follows: By (1) we can write: C1 ^ C2 = C1 ^ (C2 _ :x1) ^ (C2 _ x1). Now C1 and (C2 _ :x1) are independent. Applying (1) to (C2 _ x1):
C1 ^ C2 = C1 ^ (C2 _ :x1) ^ (C2 _ x1 _ :x2) ^ (C2 _ x1 _ x2)
The rst three clauses are independent. Repeating the process of being independent between the last clause with the previous ones, until xp is considered, we have that C1 ^ C2 can be written as: C1^(C2_:x1)^(C2_x1_:x2)^:::^(C2_x1_x2_:::_:xp)^(C2_x1_x2_:::_xp).
The last clause contains all literals of C1, so it can be eliminated, and then C1 ^ C2 = C1 ^ (C2 _ :x1) ^ (C2 _ x1 _ :x2) ^ ::: ^ (C2 _ x1 _ x2 _ ::: _ :xp) (2)
We obtain on the right hand side of (2) an independent set of p + 1 clauses. Let us present the independent reduction transformation in terms of falsifying strings.
Given a pair of falsifying strings A and B. Let us assume that there are indices x1; x2; :::; xp such that A[xi] = 1 or A[xi] = 0 and B[xi] = , for all i 2 [[p]]. There exists a reduction to transform B to be independent with A, we call at this transformation the independent reduction, and this works by replacing the falsifying string B by p falsifying strings say B1; B2; : : : Bp as follows: { B1[i] = B[i] if i 6= x1 and B1[i] = 1 A[i] if i = x1. { B2[i] = B[i] if i 6= x1 and i 6= x2, B2[i] = A[i] if i = x1 and B1[i] = 1 if i = x2. { { Bp[i] = B[i] if i 6= xj; j 2 f1 pg and Bp[i] = A[i] if i = xj; j 2 f1 p 1g, and Bp[i] = 1 A[i] if i = xp.
We will denote the independent reduction between two clauses C1 and C2 or their corresponding falsifying strings A and B as: reduc(C1; C2) or reduc(A; B) respectively. Notice that the independent reduction is not commutative, in the sense that reduc(C2; C1) builds an independent set of jLit(C2) (Lit(C1) \ Lit(C2))j clauses. However, reduc(C1; C2) and reduc(C2; C1) are logically equivalent because they determine the same set of falsifying assignments. Furthermore, when (Lit(C1) (Lit(C1) \ Lit(C2))) = ; then the set of falsifying assignments of C2 is a subset of the set of falsifying assignments of C1, that is, F AL(C2) F AL(C1), and then reduc(C1; C2) = C1.
Reduction that contains the smallest number of clauses can be obtained by computing both jLit(C1) (Lit(C1)\Lit(C2))j and jLit(C2) (Lit(C1)\Lit(C2))j or if we are working with falsifying strings by computing the set of indices fi j A[i] = 1 or A[i] = 0 and B[i] = g and fi j B[i] = 1 or B[i] = 0 and A[i] = g. The set with the smallest cardinality can be chosen to be reduced.
For formulas in CF, a pair of dependent clauses has either at least one common literal or not variables in common.
Let Ci; Cj be two dependent clauses with at least one common literal, in a CF F with n variables. Let A and B the falsifying strings of Ci and Cj. That A and B are dependents with at least one common literal means that the following conditions hold: 1. if A[i] = x then B[i] 6= 1 x for all i 2 f1 : : : ng, 2. there is a non-empty set of indices xj such that A[xj] = B[xj] and 3. there is a set of indices xj such that (A[xj] = 0 or A[xj] = 1 and B[xj] = ) or (B[xj] = 0 or B[xj] = 1 and A[xj] = ). Example 2. The following table shows two falsifying strings of two dependent clauses with a common literal The application of reduc(A; B) modi es the string B as follows xn 1 xn Falsifying string * * 1**. . . 1. . . ** A * * 01*. . . 1. . . ** B Lemma 4. Let Ci; Cj be two dependent clauses with no common literals, in a formula F with n variables. The number of falsifying assignments for this pair of clauses is:
jCij 2n jCij + X 2n jCjj i Example 3. Let Ci; Cj 2 F , where Ci = (x1 _ x2) and Cj = (x3 _ x4) are dependent clauses. By lemma 4, #F AL(Ci ^ Cj) = 2n 2 + 2n 3 + 2n 4. The transformation to obtain independent clauses can be applied over Cj as (x1 _ x2) ^ (x3 _ x4) = (x1 _ x2) ^ (x1 _ x3 _ x4) ^ (x1 _ x2 _ x3 _ x4). Lemma 5. For any independent formula F = fC1; : : : ; Cmg involving n variables #F AL(F ) = Pim=1 2n jCij.
Corollary 1. If F is an independent k-CF then #F AL(F ) = Pim=1 2n k.
F is a contradiction when #FAL(F ) = 2n, then all k-CF with at least 2k independent clauses will be a contradiction.
Furthermore, let F be a CF, n = j (F )j and F is not necessarily an independent formula. Let C be an independent clause with each clause of F , based on the iterative application of lemma 3, it holds #F AL(F ^ C) = #F AL(F ) + 2n jCj (3)
The independent reduction determines a procedure to compute #FAL(F ^C) when #F AL(F ) has already been computed. The procedure consists of applying the independent reduction on C and the clauses in F involving the variables (C) until we build a new set of clauses C0 which will be independent with each clause Ci 2 F .
For example, let F = ffx1; x2g; fx3; x2g; fx4; x3g; fx4; x5g; fx5; x6gg. #FAL(F ) can be computed incrementally using the falsifying strings of the clauses of F . The matrix of Table 1 represents the falsifying string of each clause. x1 x2 x3 x4 x5 x6 C1 1 1 * * * *
C2 * 0 1 * * * C3 11 0 * 0 1 * *
C3 12 1 0 0 1 * * Table 2. The falsifying strings after applying the independent reduction between C1 and C3.
Clauses C1 and C2 are independent so no reduction is needed between those clauses. The clause C3 is not independent with C1, even more, this pair of clauses does not have a common literal hence the independent reduction has to be applied either to C1 or C3. Applying it to C3 we obtain the strings of Table 2.
Now, the four clauses are independent each other. Consider now C4 whose falsifying string is 00 . Again it is not independent with C1, applying the independent reduction rule we obtain the strings of Table 3.
Both C4 11 and C4 12 are independent with C1. The new clauses have to be checked to be independent with the rest of the clauses. It can be noticed that the new clause C4 11 is not independent with the clause C2 so the procedure is repeated until each clause in F is independent with each other. The independent reduction application gives the results shown in Table 4.
From lemma 5, #FAL(F ) = i1=012n jCij = 24 + 24 + 23 + 22 + 22 + 20 + 20 + 20 + 20 + 20 = 53. Then, #SAT(F ) = 2n #F AL(F ) = 64 53 = 11. 3.1
Reducing the sizes of CF's In order to reduce the number of clauses while applying the independent reduction principle, the following rule can be applied.
Subsumed clause Rule. Given two clauses Ci and Cj of a CF F , if Lit(Ci) Lit(Cj), then Cj is subsumed by Ci, and then Cj can be deleted from F .
Namely, all satisfying assignments of Cj are satisfying assignments of Ci: SAT(Cj) SAT(Ci). Thus, it is enough to keep Ci (the clause which subsumes) in the CF. In terms of falsifying strings.
De nition 4. Let A and B be two falsifying strings of length n. It is said that B subsumes A if there is a set of indices I = fi1; : : : ; ikg f1; : : : ; ng such that the following conditions hold: { 8i 2 I; (A[i] = 0 or A[i] = 1) and B[i] = { 8j 2= I, j 2 [[n]], A[j] = B[j].
The subsumed clause rule requests that each falsifying string will be compared with the rest in the Table of falsifying strings in order to nd a subsumed clause, if it exists. That implies the order of O(n m2) basic operations in the worst case.
Given F (n; m) a CF, Algorithm 1 computes #SAT (F ) based on the computation of #F AL(F ). We start with the rst clause C1 2 F , and continue adding the following clause making it independent with the previous processed clauses, until all the original clauses in F are processed. The algorithm is tailor-made to compute SAT (F ), however, it can also be used to compute #SAT (F ) and #F AL(F ).
The procedure Simplif y(Ti) works on a set of falsifying strings Ti, looking for pair of strings representing subsumed clauses in order to delete the string corresponding to the subsumed clause. The procedure Simplif y(Ti) keeps or reduces the cardinality of the set of strings Ti. As Simplif y(Ti) involves to compare each falsifying string A with the following strings in Ti, it has a time complexity of O(n jTij2).
The procedure Count F alsif yings(Tm) counts the number of falsifying assignments of an independent set of clauses represented by the set of falsifying strings Tm, and this computation is done in time O(jTmj). Furthermore, the function Count F alsif yings can be performed into the body of the main loop of the procedure #F alsif ying(F ) in order to detect any minimum unsatis able subset of clauses of F .
The total time complexity of our proposal is polynomial on n and on the size of the falsifying table Ti. Then, we have to compute the growing size of the set Ti when each new falsifying string Aj is processed into the loop of #F alsif ying(F ). Of course, a non-tight upper bound for jTmj is #FAL(F ) itself, because at most each falsifying string can have n xed values and there are at most #FAL(F ) falsifying strings in Tm. However, the representation of each F AL(Ci), Ci 2 F by a falsifying string guarantees that is not needed to express in exhaustive way all falsifying assignment of F AL(Ci). 5
Given as input a CF F expressed by m clauses de ned on n variables, we have shown a deterministic algorithm for computing #F AL(F ). Our method is incremental on the set of clauses of F . We start computing excluded subsets of falsifying assignments of F until all the space of falsifying assignments de ned by F is covered, and as #SAT(F ) = 2n-#FAL(F ), results about #SAT(F ) can be dually established. Some reductions in our procedure are used, as subsumed clauses and the independent reduction between dependent clauses, in order to accelerate the computation of #FAL(F ).