Counting Falsifying Assignments of Conjunctive Forms Using Binary Patterns Guillermo De Ita1 , J. Raymundo Marcial-Romero2 , Pilar Pozos-Parra3 and Nancy Barragán1 1 Faculty of Computer Sciences, BUAP 2 Facultad de Ingenierı́a, UAEM 3 Universidad Juárez Autónoma de Tabasco deita@cs.buap.mx, jrmarcialr@uaemex.mx, pilar.pozos@ujat.mx, nan.ba.he@gmail.com Abstract. 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 con- junctive forms (CF)). Given as input a CF formula F expressed by m clauses defined 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 assign- ments defined 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 . Keywords: #SAT, #FAL, Binary Patterns, Enumerative Combina- torics. 1 Introduction The problem of counting models for a Boolean formula (#SAT problem) can be reduced to several problems in approximate reasoning. For example, esti- mating 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 [4] which considers only 2-CF formulas. Among the class of #P-complete problems, #SAT is considered a fundamen- tal instance due to both its application in deduction issues and its relevance to establish a boundary between efficient 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 [11, 12]. In [3], some cases are presented where #SAT(F ) is computed in polynomial time considering the graph-topological structure of the constrained graph of F . Additionally, in [2] a new way to measure the degree of difficulty for solving #SAT is presented. It is shown that there is a threshold, determined by the same number of models, where #SAT is computed in polynomial time. 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 definitions. 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 Preliminaries Let X = {x1 , . . . , xn } be a set of n Boolean variables. A literal is either a variable xi or a negated variable xi . As usual, for each xi ∈ X, x0i = xi and x1i = xi . A clause is a disjunction of different and non-contradictory literals (some- times, we also consider a clause as a set of literals, e.g. x1 ∨ x2 = {x1 , x2 }). For k ∈ IN , a k-clause is a clause consisting of exactly k literals. A variable x ∈ 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 con- taining 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 defined 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 = {x1 , x2 }, υ(c) = {x1 , x2 }. Lit(F ) is the set of literals involved in F , i.e. if X = υ(F ), then Lit(F ) = X ∪ X = {x1 , x1 , ..., xn , xn }. We denote {1, 2, ..., n} by [[n]] and the cardinality of a set A by |A|. An assignment s for F is a function s : υ(F ) → {0, 1}. An assignment s can also be considered as a set of literals without a complementary pair of literals, e.g., if l ∈ s, then l 6∈ s, in other words s turns l true and l false or viceversa. Let c be a clause and s an assignment, c is satisfied by s if and only if c ∩ s 6= ∅. On the other hand, if for all l ∈ c, l ∈ s, then s falsifies c. If n = |υ(F )|, then there are 2n possible assignments defined over υ(F ). Let S(F ) be the set of 2n assignments defined over υ(F ). Let F be a CF, F is satisfied by an assignment s if each clause in F is satisfied by s. F is contradicted by s if any clause in F is falsified by s. A model of F is an assignment for υ(F ) that satisfies 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 ) \ 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 defined over υ(F ), while #F AL(F ) denotes the number of falsi- fying 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 ) = {{υ(x), υ(y)} : {x, y} ∈ F }. I.e. the vertices of GF are the variables of F , and for each clause {x, y} in F there is an edge {υ(x), υ(y)} ∈ E(F ). The neighborhood for x ∈ V (F ) is N (x) = {y ∈ V (F ) : {x, y} ∈ E(F )} and its closed neighborhood is N (x)∪{x} denoted as N [x]. The degree of a variable x, denoted by δ(x), is |N (x)|, and the degree of F is ∆(F ) = max{δ(x) P : x ∈ V (F )}. The size of the neighborhood of x, δ(N (x)), is δ(N (x)) = y∈N (x) δ(y). An algorithm to compute #SAT (F ), considers the set of connected compo- nents 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. Qk Thus, #SAT (F ) = #SAT (GF ) = i=1 #SAT (Gi ), where {G1 , . . . , Gk } is the set of connected components of GF [9]. 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 com- ponent. 3 Computing #FAL via Binary Patterns Let F = {C1 , C2 , . . . , Cm } be a strict 2-CF (each clause has length 2) and let n = |υ(F )|. 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 [6] can be applied. Such procedure has a linear time complexity on the size of the 2-CF. If k is upper bounded by a polynomial function on n, e.g. k ≤ p(n), then in [2], an exact algorithm was shown for determining k in polynomial time on the size of F . So, the hard cases to answer whether #SAT(F ) = k are given when k > p(n). In [4], several hard cases for solving #SAT(F ) are identified. Such identification depends on the relation between its number of clauses (m) and the variables (n) of the instances F . E.g. the following theorem was proved. Theorem 1. [4] Let F = {C1 , C2 , . . . , Cm } be a 2-CF and n = |υ(F )|. The hard cases to answer whether #SAT(F ) = k, are given when m > n. Lemma 1. [4] Let F = {C1 , . . . , Cm } be a 2-CF and n = |υ(F )|, if F is not a tautology then #F AL(F ) ≥ 2n−2 or the number of Falsifying Assignments is at least 2n−2 . It is known [5] that for any pair of clauses Ci and Cj , it holds that #F AL(Ci ∪ Cj ) = #F AL(Ci ) + #F AL(Cj ) − #F AL(Ci ∩ Cj ). The following lemmas show when the number of models can be reduced. Lemma 2. [4] Let F be a 2-CF, n = |υ(F )|. If Ci ∈ F and Cj ∈ F , i 6= j have non-complementary pairs of literals, but they share a literal (e.g. Ci ∩ Cj 6= ∅), then there are exactly 2n−2 + 2n−3 assignments from S(F ) falsifying Ci ∪ Cj . Binary patterns have been introduced to represent the set of falsifying as- signments of any clause defined on n variables. Those patterns allow us to design efficient procedures for computing #FAL(F ). Let F = {C1 , . . . , Cm } be a 2-CF and n = |υ(F )|. Assume an enumeration over the variables of υ(F ), e.g. x1 , x2 , . . . , xn . For each clause Ci = {xj , xk }, 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 falsifies Ci . E.g., if xj ∈ Ci then the j-th element of Ai is set to 0. On the other hand, if xj ∈ 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 = {xj , xk }, 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 falsified. Example 1. Let F = {C1 , C2 } be a 2-CF and |υ(F )| = 3. If C1 = {x1 , x2 } and C2 = {x2 , x3 } then A1 = {000, 001} and A2 = {000, 100}. We will use the symbol ∗ to represent the variables that can take any truth value in the set Ai , e.g. if F = {C1 , . . . , Cm } is a 2-CF, n = |υ(F )|, C1 = {x1 , x2 } and C2 = {x2 , x3 } then we will write A1 = |00 ∗ {z ∗ . . . ∗} and A2 = ∗00 | {z∗ . . . ∗}. This n n 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 define falsifying string as a binary pattern Ai which represents the set of falsifying assignments of Ci . Let F = {C1 , . . . , Cm } be a 2-CF, n = |υ(F )|, 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 fixed values of the string, while the positions where the symbol ∗ appears are called the free values of the string. We define the string representing the null clause as the full string ∗| ∗{z . . . ∗}. n Lemma 3. [4] Let F be a 2-CF, n = |υ(F )|. If Ci ∈ F and Cj ∈ F , i 6= j contain a complementary pair of literals, that is xk ∈ Ci and xk ∈ Cj , the falsifying set of assignments Ai and Aj of Ci and Cj respectively, forms a disjoint set of falsifying assignments. Consequently, both clauses suppress exactly 2n−2 + 2n−2 = 2n−1 assignments from S(F ). We propose to generalize the previous definitions 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. Definition 1. [5] Given two clauses Ci and Cj , if they have at least one com- plementary literal, it is said that they have the independence property. Otherwise, we say that both clauses are dependent. Definition 1 can be written in terms of falsifying strings as follows: Definition 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 ∈ {0, 1}, it is said that they have the independence property. Otherwise, we say that both strings are dependent. Definition 3. Let F = {C1 , C2 , · · · Cm } be a CF. F is called independent if each pair of clauses Ci , Cj ∈ F, i 6= j, has the independence property, otherwise F is called dependent. Let F = {C1 , C2 , · · · Cm } be a CF, n = |υ(F )|. Let C be a clause in F and x ∈ υ(F ) \ υ(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−|C| = 2n−(|C|+1) + 2n−(|C|+1) = #F AL((C ∨ x) ∧ (C ∨ x)), because (C ∨ x) ∧ (C ∨ x) are two independent clauses. In terms of falsifying strings, let F = {C1 , C2 , . . . Cm }, 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 first three clauses are independent. Repeating the process of being inde- pendent 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 ∈ [[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 − A[i] if i = x2 . – ··· – Bp [i] = B[i] if i 6= xj , j ∈ {1 · · · p} and Bp [i] = A[i] if i = xj , j ∈ {1 · · · p−1}, 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 |Lit(C2 ) − (Lit(C1 ) ∩ Lit(C2 ))| clauses. However, reduc(C1 , C2 ) and reduc(C2 , C1 ) are logically equiv- alent because they determine the same set of falsifying assignments. Further- more, when (Lit(C1 ) − (Lit(C1 ) ∩ Lit(C2 ))) = ∅ then the set of falsifying as- signments 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 |Lit(C1 )−(Lit(C1 )∩Lit(C2 ))| and |Lit(C2 )−(Lit(C1 )∩Lit(C2 ))| or if we are working with falsifying strings by computing the set of indices {i | A[i] = 1 or A[i] = 0 and B[i] = ∗} and {i | B[i] = 1 or B[i] = 0 and A[i] = ∗}. 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 com- mon 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 ∈ {1 . . . n}, 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 x1 x2 x3 · · · xk · · · xn−1 xn Falsifying string C1 1 * * · · · 1 · · · * * 1**. . . 1. . . ** A C2 * 1 * · · · 1 · · · * * *1*. . . 1. . . ** B The application of reduc(A, B) modifies the string B as follows x1 x2 x3 · · · xk · · · xn−1 xn Falsifying string C1 1 * * · · · 1 · · · * * 1**. . . 1. . . ** A C2 0 1 * · · · 1 · · · * * 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: |Ci | X n−|Ci | 2 + 2n−|Cj |−i i=1 Proof. By applying |Ci |-times the independent reduction on Ci and Cj . Example 3. Let Ci , Cj ∈ 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 Pmindependent formula F = {C1 , . . . , Cm } involving n varia- bles #F AL(F ) = i=1 2n−|Ci | . Pm Corollary 1. If F is an independent k-CF then #F AL(F ) = i=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 = |υ(F )| and F is not necessarily an indepen- dent 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−|C| (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 C 0 which will be independent with each clause Ci ∈ F . For example, let F = {{x1 , x2 }, {x3 , x2 }, {x4 , x3 }, {x4 , x5 }, {x5 , x6 }}. #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 x1 x2 x3 x4 x5 x6 C1 1 1 * * * * C1 1 1 * * * * C2 * 0 1 * * * C2 * 0 1 * * * C3 * * 0 1 * * C3−11 0 * 0 1 * * C4 * * * 0 0 * C3−12 1 0 0 1 * * C5 * * * * 0 0 Table 2. The falsifying strings after apply- Table 1. The falsifying strings for the ing the independent reduction between C1 clauses in F 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 x1 x2 x3 x4 x5 x6 C1 1 1 * * * * x1 x2 x3 x4 x5 x6 C2 * 0 1 * * * C1 1 1 * * * * C3 0 * 0 1 * * C2 * 0 1 * * * C4 1 0 0 1 * * C3−11 0 * 0 1 * * C5 0 1 * 0 0 * C3−12 1 0 0 1 * * C6 0 0 0 0 0 1 C4−11 0 * * 0 0 * C7 1 0 0 0 0 1 C4−12 1 0 * 0 0 * C8 0 1 1 1 0 0 Table 3. The falsifying strings after C9 0 0 0 0 0 0 applying the independent reduction be- C10 1 0 0 * 0 0 tween C1 and C4 . Table 4. The falsifying strings after applying the independent reduction be- tween C1 and C4 . 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. 10 n−|Ci | From lemma 5, #FAL(F ) = Σi=1 2 = 24 + 24 + 23 + 22 + 22 + 20 + 20 + 0 0 0 n 2 + 2 + 2 = 53. Then, #SAT(F ) = 2 − #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 reduc- tion 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. Definition 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 = {i1 , . . . , ik } ⊂ {1, . . . , n} such that the following conditions hold: – ∀i ∈ I, (A[i] = 0 or A[i] = 1) and B[i] = ∗ – ∀j ∈/ I, j ∈ [[n]], A[j] = B[j]. The subsumed clause rule requests that each falsifying string will be com- pared with the rest in the Table of falsifying strings in order to find a subsumed clause, if it exists. That implies the order of O(n · m2 ) basic operations in the worst case. 4 An Incremental Computation for #FAL Given F (n, m) a CF, Algorithm 1 computes #SAT (F ) based on the computa- tion of #F AL(F ). We start with the first clause C1 ∈ 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 ). Algorithm 1 Procedure #Falsifying(F ) Input: A CF F with m clauses and n variables Output: (True /False )= (SAT (F ) = ∅ or not) Simplif y(F ); {delete all subsumed clause} m = |F |; {count the new number of clauses} for all Ci ∈ F do Ai = F als String(Ci ); end for T1 = A1 ; {Begin the table of falsifying strings for F } for all i = 2 to m do Ti = reduc(Ai , Ti−1 ); {Apply independent reduction} Simplif y(Ti ); {delete all subsumed clause} if (Ti has a full string) then Returns(F ‘is unsatisfiable’); {Fals(F ) cover all the assignments} end if end for Ct = Count F alsif yings(Tm ); {Count number of falsifying assignments} if ((2n − Ct) > 0) then Returns(F ‘is satisfiable’); else Returns(F ‘is unsatisfiable’); end if 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 · |Ti |2 ). The procedure Count F alsif yings(Tm ) counts the number of falsifying as- signments of an independent set of clauses represented by the set of falsifying strings Tm , and this computation is done in time O(|Tm |). 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 unsatisfiable 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 |Tm | is #FAL(F ) itself, because at most each falsifying string can have n fixed values and there are at most #FAL(F ) falsifying strings in Tm . However, the representation of each F AL(Ci ), Ci ∈ F by a falsifying string guarantees that is not needed to express in exhaustive way all falsifying assignment of F AL(Ci ). 5 Conclusions Given as input a CF F expressed by m clauses defined on n variables, we have shown a deterministic algorithm for computing #F AL(F ). Our method is in- cremental on the set of clauses of F . We start computing excluded subsets of falsifying assignments of F until all the space of falsifying assignments defined 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 ). References 1. Dahllöf V., Jonsson P., Wahlström M., Counting models for 2SAT and 3SAT for- mulae., Theoretical Computer Sciences, 332(1-3), (2005), pp. 265-291. 2. De Ita G., Marcial-Romero R., Hernández J.A., A threshold for a Polynomial Solution of #2SAT, Fundamenta Informaticae, 113:1(2011), pp. 63-77. 3. De Ita G., Bello P., Contreras M., New Polynomial Classes for #2SAT Established Via Graph-Topological Structure, Engineering Letters, Vol. 15;2, Int. Assoc. of Engineers, www.engineeringletters.com, (2007), pp. 250-258. 4. De Ita G., Marcial-Romero J.R., Computing #2SAT and #2UNSAT by Binary Patterns, LNCS, Vol. 7329 - 4th Mexican Conf. on Pattern Recognition, (2012), pp. 273-282. 5. Dubois Olivier, Counting the number of solutions for instances of satisfiability, Theor. Comp. Sc. 81, (1991), 49-64. 6. Gusfield D., Pitt L., A bounded approximation for the minimum cost 2-Sat pro- blem, Algorithmica 8, (1992), 103-117. 7. Linial N., Nisan N. Approximate inclusion-exclusion. Combinatorica, Vol. 10, No. 4, (1990), pp. 349-365. 8. Lozinskii E., Counting propositional models, Inf. Proc. Letters 41, (1992), pp. 327- 332. 9. Roth D., On the hardness of approximate reasoning, Artificial Intelligence 82, (1996), pp. 273-302. 10. Vadhan Salil P., The Complexity of Counting in Sparse, Regular, and Planar Graphs, SIAM Journal on Computing, Vol. 31, No.2, (2001), pp. 398-427. 11. Wahlström M., A Tighter Bound for Counting Max-Weight Solutions to 2SAT Instances, LNCS, Vol. 5018 - Parameterized and Exact Computation: Third Int. Workshop, (2008), pp. 202-213. 12. Zhou Junping, Yin Minghao, Zhou C., New Worts-Case Upper Bound for #2-SAT and #3-SAT with the Number of Clauses as the Parameter, Proc. of the AAAI, (2010), pp. 217-222.