=Paper=
{{Paper
|id=Vol-1287/lanmr2014_paper_2
|storemode=property
|title=Counting Falsifying Assignments of Conjunctive Forms Using Binary Patterns
|pdfUrl=https://ceur-ws.org/Vol-1287/lanmr2014_paper_2.pdf
|volume=Vol-1287
|dblpUrl=https://dblp.org/rec/conf/lanmr/LunaMP14
}}
==Counting Falsifying Assignments of Conjunctive Forms Using Binary Patterns==
https://ceur-ws.org/Vol-1287/lanmr2014_paper_2.pdf
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.