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][10][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 fundamental 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 ) = 2 n − #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.

Let X = {x 1 , . . . , x n } be a set of n Boolean variables. A literal is either a variable x i or a negated variable x i . As usual, for each x i ∈ X, x 0 i = x i and x 1 i = x i . A clause is a disjunction of different and non-contradictory literals (sometimes, we also consider a clause as a set of literals, e.g.

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

] 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 ∈ 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 = ∅. On the other hand, if for all l ∈ c, l ∈ s, then s falsifies c. If n = |υ(F )|, then there are 2 n possible assignments defined over υ(F ). Let S(F ) be the set of 2 n 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 falsifying assignments of F . Thus, #FAL(F ) = 2 n -#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: G F = (V (F ), E(F )), where V (F ) = υ(F ) and E(F ) = {{υ(x), υ(y)} : {x, y} ∈ F }. I.e. the vertices of G F are the variables of F , and for each clause {x, y} in F there is an edge {υ(x), υ(y)} ∈ E(F ).

The

An algorithm to compute #SAT (F ), considers the set of connected components of its constrained graph G F . 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 (

The set of connected components of G F conforms a partition of F . So, from now on, we will work with a formula F represented by just one connected component.

Let F = {C 1 , C 2 , . . . , C m } 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 < 2 n . 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.

It is known [5] that for any pair of clauses C i and C j , it holds that #F AL(

The following lemmas show when the number of models can be reduced.

Binary patterns have been introduced to represent the set of falsifying assignments of any clause defined on n variables. Those patterns allow us to design efficient procedures for computing #FAL(F ).

Let F = {C 1 , . . . , C m } be a 2-CF and n = |υ(F )|. Assume an enumeration over the variables of υ(F ), e.g. x 1 , x 2 , . . . , x n . For each clause C i = {x j , x k }, let A i 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 x j and x k that falsifies C i . E.g., if x j ∈ C i then the j-th element of A i is set to 0. On the other hand, if x j ∈ C i then the j-th element of A i is set to 1. The same argument applies to x k . It is easy to show that if C i = {x j , x k }, then x j and x k have the same values in each string of A i 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. 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 C i and C j , if they have at least one complementary 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.

Let C be a clause in F and x ∈ υ(F ) \ υ(C) be any variable, we have that

Furthermore, this reduction preserves the number of falsifying assignments of C with respect to

is the falsifying string of a clause C j such that there is an index i, A[i] = * then the falsifying string A can be replaced by two falsifying strings say A 1 and A 2 as follows:

1.

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 A 1 and A 2 with respect to F .

Given a pair of dependent clauses C 1 and C 2 . Let us assume that there are literals in C 1 which are not in C 2 , let x 1 , x 2 , ..., x p be these literals. There exists a reduction to transform C 2 to be independent with C 1 , we call at this transformation the independent reduction, and this works as follows: By (1) we can write:

The first three clauses are independent. Repeating the process of being independent between the last clause with the previous ones, until x p is considered, we have that C 1 ∧ C 2 can be written as:

The last clause contains all literals of C 1 , so it can be eliminated, and then

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 x 1 , x 2 , ..., x p such that A[

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 B 1 , B 2 , . . . B p as follows:

-

and

We will denote the independent reduction between two clauses C 1 and C 2 or their corresponding falsifying strings A and B as: reduc(C 1 , C 2 ) or reduc(A, B) respectively. Notice that the independent reduction is not commutative, in the sense that reduc(C 2 , C 1 ) builds an independent set of |Lit(C 2 ) − (Lit(C 1 ) ∩ Lit(C 2 ))| clauses. However, reduc(C 1 , C 2 ) and reduc(C 2 , C 1 ) are logically equivalent because they determine the same set of falsifying assignments. Furthermore, when (Lit

Reduction that contains the smallest number of clauses can be obtained by computing both |Lit( 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 C i , C j 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 C i and C j . That A and B are dependents with at least one common literal means that the following conditions hold: Example 2. The following table shows two falsifying strings of two dependent clauses with a common literal

The application of reduc(A, B) modifies the string B as follows

The transformation to obtain independent clauses can be applied over C j as (

Lemma 5. For any independent formula

F is a contradiction when #FAL(F ) = 2 n , then all k-CF with at least 2 k independent clauses will be a contradiction.

Furthermore, let F be a CF, n = |υ(F )| 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

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 which will be independent with each clause C i ∈ F .

For example, let F = {{x 1 , x 2 }, {x 3 , x 2 }, {x 4 , x 3 }, {x 4 , x 5 }, {x 5 , x 6 }}. #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. 2. The falsifying strings after applying the independent reduction between C1 and C3.

Clauses C 1 and C 2 are independent so no reduction is needed between those clauses. The clause C 3 is not independent with C 1 , even more, this pair of clauses 3. The falsifying strings after applying the independent reduction between C1 and C4.

The falsifying strings after applying the independent reduction between C1 and C4.

does not have a common literal hence the independent reduction has to be applied either to C 1 or C 3 . Applying it to C 3 we obtain the strings of Table 2. Now, the four clauses are independent each other. Consider now C 4 whose falsifying string is * * * 00 * . Again it is not independent with C 1 , applying the independent reduction rule we obtain the strings of Table 3.

Both C 4−1 1 and C 4−1 2 are independent with C 1 . The new clauses have to be checked to be independent with the rest of the clauses. It can be noticed that the new clause C 4−1 1 is not independent with the clause C 2 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 ) = Σ 10 i=1 2 n−|Ci| = 2 4 + 2 4 + 2 3 + 2 2 + 2 2 + 2 0 + 2 0 + 2 0 + 2 0 + 2 0 = 53. Then, #SAT(F ) = 2 n − #F AL(F ) = 64 − 53 = 11.

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 C i and C j of a CF F , if Lit(C i ) ⊆ Lit(C j ), then C j is subsumed by C i , and then C j can be deleted from F .

Namely, all satisfying assignments of C j are satisfying assignments of C i : SAT(C j ) ⊆ SAT(C i ). Thus, it is enough to keep C i (the clause which subsumes) in the CF. In terms of falsifying strings. The subsumed clause rule requests that each falsifying string will be compared 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 • m 2 ) basic operations in the worst case.