=Paper=
{{Paper
|id=None
|storemode=property
|title=The computation of #2SAT by a fixed-parameter tractable algorithm
|pdfUrl=https://ceur-ws.org/Vol-2264/paper9.pdf
|volume=Vol-2264
|authors=Guillermo de Ita,Pedro Bello,Miguel Rodríguez
|dblpUrl=https://dblp.org/rec/conf/lanmr/ItaBR18
}}
==The computation of #2SAT by a fixed-parameter tractable algorithm==
https://ceur-ws.org/Vol-2264/paper9.pdf
The Computation of #2SAT by a
Fixed-Parameter Tractable Algorithm
Guillermo de Ita, Pedro Bello, and Miguel Rodriguez
Benémerita Universidad Autónoma de Puebla, Mexico
{deita,pbello,mrodriguez}@cs.buap.mx
Abstract. The counting of models for two conjunctive forms (2-CF),
problem know as #2SAT, is a classic #P problem. We determine different
structural patterns on the underlying graph of a 2-CF F that allows the
efficient computation of #2SAT(F ). We show that if the constrained
graph GF of a 2-CF F is acyclic or it has cycles without common edges
with other cycles, then #2SAT(F ) is computed efficiently.
Finally, if GF has entwined cycles (set of cycles with common edges),
we have designed a deterministic fixed-parameter algorithm for #2SAT,
that is, an algorithm whose time complexity is O(2k · poly(|F |)), where
poly(|F |) is a polynomial function on the size of F , and k denotes the
maximum ‘edge-entwined’ of GF , that is, k is a parameter equal to the
maximum number of fundamental cycles of GF with a common edge.
Keywords: #SAT Problem, · Counting models,· Efficient Enumerative
Algorithms,· Parameterized Complexity
1 Introduction
#SAT (the problem of counting models for a Boolean formula) is of special con-
cern to Artificial Intelligence (AI), and it has a direct relationship to Automated
Theorem Proving, as well as to approximate reasoning [5, 6, 18]. #SAT can be
reduced to several different problems in approximate reasoning.
For example, in the cases of; the estimation of the degree of belief in propo-
sitional theories, the generation of explanations to propositional queries, the
reparation of inconsistent databases, the approximation in Bayesian inference
[1, 5, 6, 18, 19]. In general approach used to compute the degree of belief, consists
of assigning an equal degree of belief to all basic ”situations”. In this manner, we
can compute the probability that Σ (an initial knowledge base which involves
n variables) will be satisfied, denoted by PΣ , as: PΣ = P rob(Σ ≡ >) = µ(Σ) 2n ,
where > stands for the Truth value, Prob is used to denote the probability, and
µ(Σ) denotes the number of models that Σ has.
#SAT is as hard as the SAT problem, but in many cases, even when SAT is
solved in polynomial time, there is not any efficient method known for #SAT.
For example, 2SAT problem (SAT restricted to consider two conjunctive forms),
it can be solved in linear time. However, the corresponding counting problem
#2SAT is a #P-complete problem.
101
The counting of combinatorial objects on graphs is an interesting and impor-
tant area of research in Mathematics, Physics, and Computer Sciences. For exam-
ple, the maximum polynomial class recognized for #2SAT is the class (≤ 2, 2µ)-
CF (two conjunctive forms where each variable appears twice at most) [18, 19].
Earlier works on #2-SAT include papers by Dubois [8], Zhang [22] and
Littman [12]. More recently, new upper bounds for exact deterministic algo-
rithms for #2-SAT have been found by Angelsmark [1], Dahllöf [2], Fürer [11],
and Wahlstr¨(o)m [21].
All the above proposals are part of the class of exponential algorithms, and
several of them follow the branch and backtracking technique begun in the pi-
oneering algorithm by Davis & Putnam (D&P). Notable improvements include
Kullmann’s work on complexity measures [15], and Eppstein’s work on solving
multivariate recurrences through quasiconvex analysis [9]. Still, one limitation
that remains in Eppstein’s framework is that it is difficult to introduce (non-
trivial) restrictions on the applicability of a possible recursion [21].
Parameterized complexity theory relaxes the classical notion of tractability
and allows us to solve some classically hard problems in a reasonable time. It
turned out that many intractable problems can be solved efficiently ”by the
slice”, that is, in time O(f (k) · nc ), where f is any function of some parameter
k, n is the size of the instance, and c is a constant independent from k.
In this case, the problem is called fixed-parameter tractable (FPT). If a prob-
lem is in the class FPT, then large instances can be solved efficiently, although
it can be an exponential-time that depends on the fixed-parameter [20].
Bacchus et al. [3] consider structural restrictions on the input formula and
propose an algorithm for #SAT whose complexity is polynomial in its number
of variables and exponential in the ’branch-width’ of the underlying constraint
graph. Gottlob et al. [13] provide a similar result in terms of the ‘tree-width’ of
the constrained graph. Fischer et al. [10] extend this to a similar result in terms
of ‘cluster-width’ [4].
Then, although it exists parameterized algorithms to solve #SAT, they re-
quest to build a k-tree decomposition or the k-branch decomposition of the con-
strained graph of the input formula (a problem that is known to be NP-complete
if we want the minimum value for k). Furthermore, the time complexity on the
fixed-parameter algorithms comes from being doubly exponential in k [16] to
be of order 4k [10].
All of the previous procedures are parameterized algorithms, where a pa-
rameter k, bounded more by the topologies that lye in the formula than in the
number of variables (or clauses) of the formula, determines the exponential com-
plexity for solving the #2SAT problem. Indeed, for those previous algorithms to
find an optimal value for the parameter k for any input formula request to solve
a NP-complete problem.
We focus toward the identification of underlying structures on the constrained
graph GF of the input formula F , that allow us the efficient computation of the
number of models of F . We extend here the procedures presented in [6, 7], where
different structural patterns on the constrained graph are identified in order to
102
compute #2SAT in an incremental and efficient way, at the same time that its
constrained graph is being traversing systematically.
The new result presented is a novel deterministic fixed-parameter tractable
algorithm for #2SAT, based on our previous procedures and that works on
the constrained graph GF of the input formula F . The time function for the
parameter k in our algorithm is upper bounded by 2k . Furthermore, our proposal
does not build the tree-width of the formula, instead we show how to compute the
parameter k in an efficient way. Our parameter k represents the ‘edge-entwined’
of the constrained graph.
While these improved bounds are only guaranteed to hold if dedicated algo-
rithms are used, these parameters can still be seen as ways in which an instance
can be easy, hopefully in ways that influence the behaviour of the ”popular” (i.e.
commonly used) algorithms as well [21].
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 literals (we also consider a clause as a set of
literals). For k ∈ N , a k-clause is a clause consisting of exactly k literals and, a
(≤ k)-clause is a clause with at most 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 clauses (we can also consider
a CF as a set of clauses). We say that F is a positive monotone CF if all of its
variables appear in unnegated form. A k-CF is a CF containing only k-clauses
and, (≤ k)- CF denotes a CF containing clauses with at most k literals. A kµ-
CF is a formula in which no variable occurs more than k times. A (k, jµ)-CF
((≤ k, jµ)-CF) is a k-CF ((≤ k)-CF) such that each variable appears no more
than j times.
We use ν(Y ) to express the set of variables involved in the object Y , where Y
could be a literal, a clause or a conjunctive formula. For instance, for the clause
c = {x1 , x2 }, ν(c) = {x1 , x2 }. And Lit(F ) is the set of literals that appears in a
CF F , i.e. if X = ν(F ), then Lit(F ) = X ∪ X = {x1 , x1 , . . . , xn , xn }. We denote
the cardinality of a set A, by |A|. We also denote {1, 2, . . . , n} by [[n]].
An assignment s for F is a Boolean function s : ν(F ) → {0, 1}. An assignment
can also be considered as a set of non complementary pairs of literals. If l ∈ s,
being s an assignment, then s turns l true and l false. Considering a clause c
and an assignment s both as a set of literals, c is satisfied by s if and only if
(c ∩ s) 6= ∅, and if for all l ∈ c, l ∈ s then s falsifies c. If F1 ⊂ F is a formula
consisting of some clauses of F , then ν(F 1) ⊂ ν(F ), and an assignment over
ν(F1 ) is a partial assignment over ν(F ). Assuming n = |ν(F )| and n1 = |ν(F1 )|,
any assignment over ν(F1 ) has 2n−n1 extensions as assignments over ν(F ).
Let F be a Boolean formula in Conjunctive Form (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 contradicted by s. A model of F is an assignment for ν(F ) that
103
satisfies F . Given a CF F , the SAT problem consists of determining if F has
a model. The #SAT problem consists of counting the number of models of F
defined over ν(F ). #2SAT denotes #SAT for formulas in 2-CF.
2.1 The Constrained graph of a 2-CF
There are some graphical representations of a conjunctive form (see e.g. [10, 20]).
We use here the signed primal graph of a two conjuctive form. Let F be a 2-CF,
its signed constrained undirected graph (constrained graph) is denoted by GF =
(V (F ), E(F )), with V (F ) = ν(F ) and E(F ) = {{ν(x), ν(y)} : {x, y} ∈ F }, that
is, 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 ). Each edge c = {ν(x), ν(y)} ∈ E is associated
with an ordered pair (s1 , s2 ) of signs, assigned as labels of the edge that connect
the variables appearing in the clause. The signs s1 and s2 are related to the signs
of the literals x and y respectively. For example, the clause {x ∨ y} determines
the labelled edge: ”x −+ y” which is equivalent to the edge ”y +− x”.
Let S = {+, −} be a set of signs. A graph with labelled edges on a set S is
a pair (G, ψ), where G = (V, E) is a graph, and ψ is a function with domain
E and range S. ψ(e) is called the label of the edge e ∈ E. Let G = (V, E, ψ)
be a signed graph with labelled edges on SxS. Let x and y be nodes in V . If
e = {x, y} is an edge and ψ(e) = (s, s0 ), then s(s0 ) is called the adjacent sign to
x(y). From now on, the term for describing the topology of a constrained graph
GF is inherited to its original 2-CF formula F .
Two vertices v and w of a constrained graph GF are called adjacent if there
is an edge {v, w} ∈ E(GF ), joining them. The neighbourhood of x ∈ V (GF ) is
N (x) = {y ∈ V : {x, y} ∈ E(GF )} and its closed neighbourhood is N (x) ∪ {x}
which is denoted by N [x]. Note that v is not in N (v), but is in N [v]. The degree
of a vertex x ∈ V (GF ), denoted by δ(x), is |N (x)|. If A is a set of vertices from
a graph G, N (A) is the set of neighbour vertices from any vertex of A, that is,
N (A) = ∪x∈A N (x), while N [A] = N (A) ∪ A. The maximum degree of GF or
just the degree of GF is ∆(GF ) = max{δ(x) : x ∈ V (GF )}.
Notice that a constrained graph of a 2-CF can be a multigraph since two
fixed variables can be involved in more than one clause of the formula forming
parallel edges. Furthermore, an unitary clause is represented by a loop in the
constrained graph (an edge to join a vertex to itself).
3 Processing Constrained Graphs with Cycles
Let GF = (V, E) be a simple cycle with m nodes, that is, all the variables in υ(F )
appear twice, m = n = |V | = |E|. F can be decomposed as F = F 0 ∪ cm , where
F 0 = {c1 , ..., cm−1 } is a path and cm = (xm−1 m
, xδ1m ) is the edge that conforms
with GF 0 a simple cycle: x1 , x2 , ..., xm−1 , x1 . We will call GF 0 the internal path
of the cycle and cm the back edge of the cycle.
δb
Lemma 1. If F = {Ci }m−1 a
i=1 ∪ {{xa , xb }} is such that
104
– xaa or x1−
a
a
∈ Cj for some j = 1, . . . m − 1 and
δb 1−δb
– xb or xb ∈ Ck for some k = 1, . . . m − 1 then
#SAT ({Ci }m−1
i=1 ) ≥ #SAT (F )
Proof. Let s be a satisfying assignment of {ci }m−1 a
i=1 . Then either xa or xa
1−a
∈s
δb 1−δb a δb
and also xb or xb ∈ s. If xa & xb ∈ s, then s is also a satisfying assignment
of F . Similarly, if xaa & x1−δ
b
b
∈ s or x1−
a
a
& xδbb ∈ s results in s is also a
1−δb
satisfying assignment of F . If xa 1−a
& xb ∈ s then the clause {xaa , xδbb } does
not hold, so this assignment is not a model of F .
So that a model of F ∪ {{xaa , xδbb }} is not a model of F ∪ {{x1−
a
a
}, {x1−δ
b
b
}}
since (xaa ∨ xδbb ) = x1−
a
a
∧ x1−δ
b
b
.
Let Y = {ci }i=1 ∪ {{xa }, {x1−δ
m−1 1−a
b
b
}}, then #SAT (Y ) can be computed as
a path with two unitary clauses on the extremes of the path.
In order to process cycles of a constrained graph, we use computing threads or
just threads. A computing thread is a sequence of pairs (αi , βi ), i = 1, . . . , m used
for computing the number of models over a path of m nodes. Any simple cycle
C request two computing threads. The main thread denoted by Lp processes the
internal path on the cycle, and its subordinated thread denoted by LC computes
#SAT(Y ). When the last node xb on the cycle is visited by the linear search,
the last pair (αb , βb )C associated to LC is substracted from the the pair (αb , βb )p
associated with the thread LP , as it is shown in Figure (1).
X1 X2 X3 X4 X5 X6
+ + + + + + + + + +
+
+
(α1 , β1 ) → (α2 , β2 ) → (α3 , β3 ) → (α4 , β4 ) → (α5 , β5 ) → (α6 , β6 )
Lp : (1, 1) → (2, 1) → (3, 2) → (5, 3) → (8, 5) → (13, 8)
LC : (0, 1) → (1, 0) → (1, 1) → (2, 1) → (3, 2) → (5, 3)
⇒ (13, 8) − (0, 3) = (13, 5)
Fig. 1. Computing #SAT (F ) when GF is a simple cycle
Example 1. Let F = {ci }6i=1 = {{x1 , x2 }, {x2 , x3 }, {x3 , x4 }, {x4 , x5 }, {x5 , x6 }, {
x6 , x1 }} be a monotone 2-CF which represents a cycle: GF =(V, E). Let G0 =
(V, E 0 ) where E = E 0 ∪ {c6 }, that is, the new graph G0 is F minus the edge c6 .
we have that #SAT (F ) = #SAT (F 0 ) − #SAT (F 0 ∧ x6 ∧ x1 ) = 21 − 3 = 18.
This example is illustrated in Figure 1.
Let GF = (V, E, {+, −}) be a signed connected graph of an input formula
F in 2-CF, with n = |V | and m = |E|. We will use the notation #2SAT(F ) or
#2SAT(GF ) to denote the number of models for a 2-CF F expressed as a set of
clauses or through its constrained graph GF .
105
If a depth-first search (df s) is applied over GF , starting the search, for ex-
ample, with the node vr ∈ V of minimum degree, and selecting among different
potential nodes to visit the node with minimum degree first and with minimum
value in its label as a second criterion, we obtain an unique depth-first graph G,
which we will denote as G = df s(GF ). This df s also builds an unique spanning
tree TG with vr as the root node.
In time O(m + n), the df s allows us to detect if G has cycles or not, as well
as the edges forming each cycle. The edges in TG are called tree edges, whereas
the edges in E(G)\E(TG ) are called back edges. Let e ∈ E(G)\E(TG ) be a back
edge, the union of the path in TG between the endpoints of e with the edge e
itself forms a simple cycle, such cycle is called a fundamental (or basic) cycle
of G with respect to TG . Each back edge e = {x, y} holds the maximum path
contained in the basic cycle that it is part of. Assuming that x is visited first
than y during the df s, we say that x is the start-node and y is the end-node of
the back edge e = {x, y}.
If two distinct cycles Ci and Cj from an graph G have common edges then
we say that both cycles are intersected, that is, Ci 4Cj form a new cycle, where
4 denotes the symmetric difference operation between the set of edges in both
cycles. In fact, Ci 4Cj = (E(Ci ) ∪ E(Cj )) − (E(Ci ) ∩ E(Cj )) forms a composed
cycle. If two cycles are non-intersected we say that they are independent. I.e. two
independent cycles (Ci , Cj ) hold (E(Ci ) ∩ E(Cj )) = ∅.
A cycle basis of a graph is a family of cycles which spans all cycles of the
graph. The cycles can be considered as vectors indexed by edges. The entry for
an edge is one if the edge belongs to the cycle and is zero otherwise. Addition
of cycles corresponds to vector addition modulo 2 (symmetric difference of the
underlying edge sets) denoted as Z2 -vector space. In this way, the cycles of a
graph form a vector space and a cycle basis is simply a basis of this vector space
[14].
According with our particular depth-first search G = df s(GF ) on GF , let
C = {C1 , ..., Ct } be the set of fundamental cycles found during such depth-first
search. Notice that t = m − n + 1 is the dimension of the Z2 -vector space with
the symmetric difference on the edge sets as addition, and C is a cycle basis for
the constrained graph GF .
3.1 Processing Intersected Cycles
In order to show how to process a set of intersected cycles, we show first how to
process a pair of them. Assume Ci , Cj are two basic cycles such that E(Ci ) ∩
E(Cj ) 6= ∅, and let ei = x → y and ej = u → v be its corresponding back edges.
Let GF be the constrained graph of the formula F containing both cycles Ci
and Cj .
A main thread denoted by Lp will be associated with the computation of
#2SAT(F ). Lp is always active during all the computation of #2SAT(F ).
While the threads LCi and LCj will be used for computing the number of
assignments to be substracted from Lp when the cycles Ci and Cj are found.
106
We say that both threads LCi and LCj are subordinated threads of Lp and that
Lp dominates LCi and LCj .
We apply our deterministic df s on GF , and let us assume that the start-
node x of Ci is always visited first than the start-node u of Cj . When the node
x is visited, the thread LCi becomes active. And when the node u is visited,
two new threads (LCj 7→p and LCj 7→Ci ) are created. LCj 7→p carries the value that
will be associated with the thread Lp and LCj 7→Ci carries the value that will be
associated with the thread LCi .
Assuming (αx , βx )i as the pair of a dominant thread Li at a start-node x,
then the initial pair (αx , βx )e for its subordinated thread Le7→i is computed as:
(0, βx )i if + is the sign of x ∈ e
(αx , βx )e =
(αx , 0)i if − is the sign of x ∈ e
In fact, when a start-node of a new cycle is visited, then the number of
current threads will be duplicated, building a new subordinate thread for each
previous current active thread. When the end-node y of the cycle Ce is visited,
the pair (αy , βy )e of any subordinated thread Le is computed as:
(0, βy )e if + is the sign of y ∈ e
(αy , βy )e =
(αy , 0)e if − is the sign of y ∈ e
and the subordinated thread Le is closed, substracting the resulting pair (αy , βy )e
from the corresponding pair of its dominant thread.
x u v y
Cj
Ci
Fig. 2. Case with embedded intersected cycles
In the first case, if Cj is embedded into Ci , i.e. E(Cj ) − E(Ci ) = {ej }, then
the end-node v of Cj is visited first than the end-node y of Ci (see Figure 2 and
Table 1).
In the first case, as v is visited before y, then the cycle Cj finishes before
visit all node of Ci , and the two threads (LCj 7→p and LCj 7→Ci ) are closed before
the threads LP and LCi finish.
The last pair associated to the threads LCj 7→p and LCj 7→Ci at the node v are
substracted from its corresponding pairs on its dominant threads Lp and LCi ,
respectively. After this, the processing of the two remaining threads Lp and LCi
continue, as it is shown in Table 1.
For the second pattern, we assume that end-node y of Ci is visited before the
end-node v of Cj , then the cyle Ci begins and finishes before visit all node of the
cycle Cj (see Figure 3 and Table 2 ). The threads (LCi and LCj 7→Ci ) are closed
when the node y is visited and the last pair of those threads are substracted
107
Table 1. Computing embedded intersected cycles
Node x ... u ... v ... y
Lp : (αx , βx )p . . . (αu , βu )p . . . (αv , βv )p − . . . (αy , βy )p −
(0, βv )Cj ,p = (0, βy )Ci =
(αv , βv )p (αy , βy )p
Lci : (0, βx )Ci . . . (αu , βu )Ci . . . (αv , βv )Ci − . . . (αy , βy )Ci ⇒
(αv , 0)Cj ,Ci = (0, βy )Ci
(αv , βv )Ci closed
Lcj →p : (αu , 0)Cj ,p . . . (αv , βv )Cj ,p ⇒
(0, βv )Cj ,p
closed
Lcj →ci : (0, βu )Cj ,Ci . . . (αv , βv )Cj ,Ci ⇒
(αv , 0)Cj ,Ci
closed
Cj
x u y v
Ci
Fig. 3. Case with intersected cycles (not embedded)
from its corresponding pairs on the threads Lp and LCj →p , respectively. After
this, the processing of the two remaining threads Lp and LCj →p continue, until
visit all node of the cycle Cj .
Sometimes, the pair associated to a computing thread Lx results to be (0,0);
in such cases Lx is closed (stops being active) because it will not affect the
value of any other active thread. A relevant point to consider in our procedure,
is to recognize which threads have to keep being active and which have to be
closed when an end-node of a cycle is visited,i.e. which of the two patterns for
intersected cycles has to be applied.
4 Computing #2SAT for General Graphs
We present, the general case for computing #2SAT. Let F be the input 2-CF and
G its constrained graph, we assume that GF = df s(G) has intersected cycles. Let
TF be the unique spanning tree formed during the df s and let C = {C1 , C2 , ..., Ct }
be the unique set of fundamental cycles found during such depth-first search.
For each edge e ∈ E(GF ), we define κ(e) as the number of basic cycles where
κ(e) = |{C ∈ C : e ∈ E(C)}|. Notice that κ(e) = 1, ∀e ∈ (E(GF ) − E(TF )).
κ(e) denotes the number of entwined cycles of G where the edge e is a common
108
Table 2. Computing intersected cycles (not embedded)
Node x ... u ... y ... v
Lp : (αx , βx )p . . . (αu , βu )p . . . (αy , βy )p − . . . (αv , βv )p −
(0, βy )Ci = (0, βv )Cj ,p =
(αy , βy )p (αv , βv )p
Lci : (0, βx )Ci . . . (αu , βu )Ci . . . (αy , βy )Ci ⇒
(0, βy )Ci
closed
Lcj →p : (αu , 0)Cj ,p . . . (αy , βy )Cj ,p − . . . (αv , βv )Cj ,p ⇒
(αy , 0)Cj ,Ci = (0, βv )Cj ,p
(αy , βy )Cj ,p closed
Lcj →ci : (0, βu )Cj ,Ci . . . (αy , βy )Cj ,Ci ⇒
(αy , 0)Cj ,Ci
closed
edge among them. We call the edge-entwined of a graph, denoted as $(GF ), the
maximum value of κ(e), ∀e ∈ E(GF ). I.e. $(GF ) = max{κ(e) : e ∈ E(GF )}.
Therefore, κ(e), ∀e ∈ E(GF ) is a function denoting the degree in which all
cycles with the same edge e are entwined. As a result, we also obtain an unique
value for the edge-entwined $(GF ) of the constrained graph GF .
In a previous work [6] (the Count Models procedure), we have presented a
polynomial time algorithm for computing #2SAT when the constrained graph of
the input formula has non-intersected cycles. As in the Count Models procedure,
we build an orientation on each edge {u, v} in GF by directing: u → v, if v is an
ancestor node of u in TF . GF is traversing in post-order according to the orien-
tation given to the edges. A main thread denoted by Lp is associated with the
computation of #SAT(TF ). Lp keeps always active during all the computation
of #2SAT(F ).
The computation of #2SAT(F ) is done as it was done in the Count Models
procedure, and only a light extension has to be done when a start-node of a back
edge e = x → y is visited. The following cases consider how to process the new
cycle Ce that has been found while GF is being traversing.
1. If Ce is an independent cycle then we process it as a Ring, as it was explained
in the Count Models procedure.
2. If Ce is part of a set of intersected cycles, then the number of current threads
will be duplicated, building a new subordinate thread for each previous cur-
rent active thread, it was shown in section 3.1.
When a start-node of a back edge e = {x → y} of a cycle is visited, the
number of current thread is duplicated. In the worst case, we will have at most 2k
active threads, where k = κ(e) is the degree of entwined among cycles containing
the edge e and e is an adjacent edge to the current node that is being visited.
Thus, in our procedure, the maximum number of active computing threads at
109
any moment will be 2$(GF ) , where $(GF ) is the edge-entwined number of the
constrained graph GF .
We apply this algorithm to the constrained graph GF shown in figure 4.
We split the computation of #2SAT(F ) according to the two parts of the graph
show in figures 5 and 6.
C1 C3
- +
+ +
+ + + - - + - - + +
X X5 X X3 X X1
6 4 2 +
-
C2 +
+
C4
+
X - -
11
- + + + -
X X X
+ 9 8 7
+
+ -
X 10
C5
Fig. 4. A constrained graph with intersected cycles
C1 C3
- +
+ +
+ + + - - + - - + +
X X5 X X3 X X1
6 4 2
- +
C2
N odes : x6 x5 x4 x3 x2 x1
Lp : (1, 1) →(2, 1) → (2, 3) → (5, 3) − (2, 0) = (3, 3) → (3, 6) → (9, 3)
C1 : (0, 1) → (1, 0) → (1, 1) → (2, 1) ⇒ (2, 0)
C2 → Lp : (2, 0) → (2, 2) → (4, 2) − (2, 0) = (2, 2)
(2, 2) − (2, 0) = (0, 2) → (2, 2) → (4, 2) ⇒ (0, 2)
C2 → C1 : (1, 0) → (1, 1) → (2, 1) ⇒ (2, 0)
C3 → Lp : (0, 3) → (3, 3) − (2, 0) = (1, 3)
(1, 3) − (1, 0) = (1, 2) → (2, 3) → (5, 2) ⇒ (0, 2)
C3 → C1 : (0, 1) → (1, 1) ⇒ (1, 0)
C3 → C2 : (0, 2) → (2, 2) − (2, 0) = (0, 2)
(0, 2) − (1, 0) = (0, 2) → (2, 2) → (4, 2) − (0, 2) = (4, 0)
C3 → C2 → C1 : (0, 1) → (1, 1) ⇒ (1, 0)
⇒ (9, 3)− (0, 2)− (0, 2) = (9, 0)
Fig. 5. First part of the Computation of #SAT (GF )
The last pair obtained in the first part of the graph is (α1 , β1 ) = (9, 0)
and the pair for the second part of the graph is (α1 , β1 ) = (6, 0). Both pairs
corresponds with the value for the same node x1 , then the last pair associated
to x1 is (54, 0) = (9 ∗ 6, 0 ∗ 0), and #2SAT(F ) = 54 models.
110
C4
-
+
+ - - + + + - +
X X9 X X X
11 8 7 1
+
-
+ +
C5
X 10
N odes : x11 x10 x9 x8 x7 x1
Lp : (1, 1) → (1, 2) ∗ (2, 1) = (2, 2) → (4, 2) → (6, 4) − (4, 0) = (2, 4) → (6, 4)
C4 : (0, 2) → (2, 2) → (4, 2) ⇒ (4, 0)
C5 → Lp : (4, 0) → (4, 4) − (2, 0) = (2, 4)
(2, 4) − (4, 0) = (0, 4) → (4, 4) ⇒ (0, 4)
C5 → C4 : (2, 0) → (2, 2) ⇒ (2, 0)
⇒ (6, 4) − (0, 4) = (6, 0)
Fig. 6. Second part of the computation of #SAT (GF )
4.1 Time Complexity Analysis
The Count M odels has a time complexity of O(n + m), n being the number of
nodes and m the number of edges of the constrained graph of an formula F .
The marking of edges forming part of fundamental cycles during the df s can
be done at most in time O(m · n) since a fundamental cycle has length at most
n. Consequently, the computation of κ(e), ∀e ∈ E(GF ), is done in time O(m · n).
The identification of the value edge-entwined of a graph $(G), representing the
value of the parameter k for our fixed-parameter algorithm, also involves at most
O(m · n) basic operations.
Now, we analyze the time-complexity for processing intersected cycles. Let κ
be a set of k intersected cycles with common edges.
In each beginning of a cycle of κ, the number of current thread has to be
duplicated so that in the worst case, we will have at most 2k active threads.
And we have shown that O(poly(n, m)) operations are enought to travers by the
nodes x ∈ V (GF ) at the same time that its pair (αx , βx ) is computed.
Given that the size of the formula is (n + m), we obtain that the complexity
time for our proposal is of order O(2$(GF ) · p(n, m)), where p(n, m) represents
a polynomial function based on n and m, and $(GF ) is a non-negative integer
parameter representing the edge-entwined number of the constrained graph GF
of the input F .
Then, the complexity-time for the general case is in the worst case, upper
bounded by O(2$ (GF ) · p(n, m)). Then, one can afford (mildly) simple expo-
nential behaviour of our algorithm in terms of the parameter k = $(GF ) - the
edge-entwined number of the constrained graph, as long as the overall running
time is polynomial on the size of the 2-CF when considering the parameter as a
fixed constant, and this shows that #2SAT is in the class FPT (the class of all
fixed-parameter tractable problems).
The computation of the edge-entwined number k = $(GF ) of a graph GF
is polynomial on the zise of the graph and its value is usually smaller than the
111
number of nodes (n) of the graph. Also, the computation of $(GF ) does not
require the tree-decomposition of the graph. Furthermore, the complexity time
of O(2k · p(n, m)) is usually smaller than the exponential upper bounds based
on n or m, expressed in classical works for the computation of #2SAT .
The generated results can be compared with the results showed in [2], where
a n parameter was used in the order of complexity. In contrast in this work a k
parameter was used that improves the complexity for some instances.
On the other hand, if the value for $(GF ) is increased adding intersected
cycles to GF , then the value #2SAT(F ) will decrease, for example, #2SAT(F ) ≤
n5 , n = |υ(F )|, then #2SAT(F ) could be computed in polynomial time for the
algorithm proposed in [7].
In order to formalize the results obtained, an formal argumentation can be
used. For example, semantic argumentation can be characterized as a two-value
model, in this way, the ST ABLE argumentation model proposes interesting
logic properties [17].
5 Conclusion
#SAT problem for the class of Boolean formulas in 2-CF is a classical #P-
complete problem. However, there are several instances of 2-CF’s for which
#2SAT can be solved efficiently.
We have shown here different polynomial-time procedures for counting mod-
els of Boolean formulas for subclasses of 2-CF’s. For example, for formulas whose
contrained graph is acyclic, its corresponding number of models is computed in
linear time. Furthermore, if the cycles in a constrained graph GF can be arranged
as independent cycles, then we can count the number of models of F efficiently.
Finally, according with the parameter k = $(GF ) - the ’edge-entwined’ of
the constrained graph of the 2-CF F , we have designed a deterministic fixed-
parameter tractable algorithm for #2SAT, that is, an algorithm whose time
complexity is O(2k · poly(|F |)), where poly(|F |) is a polynomial function on the
size of F and k is equal to the maximum number of fundamental cycles with a
common edge on the constrained graph of the input formula.
References
1. Angelsmark O., Jonsson P.: Improved Algorithms for Counting Solutions in Con-
straint Satisfaction Problems, In ICCP: Int. Conf. on Constraint Programming,
Springer, Berlin,1991.
2. Dahllöf, V., Jonsonn, P., Wahlström, M.: Counting models for 2SAT and 3SAT
formulae, J. Theoretical Computer Sciences,332(1-3), 2005, 265–291.
3. Bacchus F., Dalmao S., Pitassi T.: Algorithms and complexity results for #SAT and
Bayesian inference, Proc. of FOCS-03: 44th Annual Symposium on Foundations of
Computer Science, USA,2003.
4. Gomes C. P., Sabharwal A., Selman B.: Model Counting,in: Handbook of Satisfabil-
ity, Chap. 20, Armin Biere, Marijn Heule, Hans van Maaren and Toby Walsch Eds.,
IOS Press, 2008.
112
5. Darwiche A.: On the Tractability of Counting Theory Models and its Application to
Belief Revision and Truth Maintenance, J. of Applied Non-classical Logics, 11(1-2),
2001, 11–34.
6. De Ita G., Bello P., Contreras M.: New Polynomial Classes for #2SAT Established
via Graph-Topological Structure, Engineering Letters, 15 (2), 2007, 250–258.
7. De Ita G., Marcial-Romero R., Hernández A. : A Threshold for a Polynomial Solu-
tion of #2SAT, Fundamenta Informaticae, 113(1), 2011, 63–77.
8. Dubois, O.: Counting the number of solutions for instances of satisfiability, J. The-
oretical Computer Sciences,81(1), 1991, 49–64.
9. Eppstein D.: Quasiconvex analysis of backtracking algorithms, Proc. of the 15th
annual ACM-SIAM symp. on Discrete algorithms (SODA-2004),ACM, New York,
USA,2004.
10. Fischer E., Makowsky J.A., Ravve E.V.: Counting truth assignments of formulas
of bounded tree-width or clique-width, Discrete Applied Mathematics, 156(4), 2008,
511–529.
11. Fürer, M., Prasad, S. K.: Algorithms for Counting 2-SAT Solutions and Coloring
with Applications, Technical Report 33, Electronic Colloqium on Comp. Complex-
ity,2005.
12. Littman M. L., Pitassi T., Impagliazzo R.: On the Complexity of counting satisfying
assignments, Technical Report Unpublished manuscript.
13. Gottlob G., Scarcello F., Sideri M.: Fixed-parameter complexity in AI and non-
monotonic reasoning, Artificial Intelligence, 138(1-2),2002, 55–86.
14. Kavitha T., Liebchen C., Mehlhorn K., Michail D., Rizzi R., Ueckerdt T., Zweig K.:
Cycle bases in graphs: Characterization, algorithms, complexity, and applications,
Computer Science Rev., 3(4), 2009, 199–243.
15. Kullmann O.: New methods for 3-SAT decision and worst-case analysis, Theoretical
Computer Science, 223, 1999, 1–72.
16. Makowsky J.A.: Algorithmic uses of the Feferman-Vaught theorem, Ann. Pure
Appl. Logic 126, 2004, 1–3.
17. Nieves J.C, Osorio M.:Extending Well-Founded Semantics with Clark’s Completion
for Disjunctive Logic Programs, Scientific Programming, 2018, Article ID 4157030,
10 pages.
18. Roth D.: On the hardness of approximate reasoning, J. Artificial Intelligence, 82,
1996, 273–302.
19. Russ B.: Randomized Algorithms: Approximation, Generation, and Counting, Dis-
tinguished dissertations, Springer,2001.
20. Szeider Stefan.: On Fixed-Parameter Tractable Parameterizations of SAT, Theory
and Applications of Satisfiability Testing(E. Giunchiglia, A. Tacchella, Ed.), LNCS
2919, Springer-Verlag,Berlin, 2004.
21. Wahlström M.: Algorithms, Measures and Upper Bounds for Satisfiability and Re-
lated Problems, Dissertation No. 1079, Linkping, 2007.
22. Zhang, W.: Number of models and satisfiability of set of clauses, J. Theoretical
Computer Sciences, 155(1), 1996, 277–288.
113