=Paper=
{{Paper
|id=Vol-286/paper-3
|storemode=property
|title=Efficient counting of models for boolean formulas represented by embedded cycles
|pdfUrl=https://ceur-ws.org/Vol-286/LANMR07_03.pdf
|volume=Vol-286
|authors=Guillermo de Ita Luna,Pedro Bello López,Meliza Contreras González
|dblpUrl=https://dblp.org/rec/conf/lanmr/LunaLG07
}}
==Efficient counting of models for boolean formulas represented by embedded cycles==
https://ceur-ws.org/Vol-286/LANMR07_03.pdf
Efficient Counting of Models for Boolean
Formulas Represented by Embedded Cycles
Guillermo De Ita Luna, Pedro Bello López, Meliza Contreras González
Faculty of Computer Sciences, Universidad Autónoma de Puebla
deita@cs.buap.mx, pbello@cs.buap.mx, mel 22281@hotmail.com
Abstract. To compute the number of models of a 2-CF (conjunction of
clauses with two literals at most), the well-known problem as #2-SAT,
is a classical #P-complete problem. We show here an extensive class of
instances of 2CF’s where to compute the number of models can be done
in polynomial time.
Given a 2-CF Σ, we show that if its constrained graph GΣ is acyclic or
if its set of cycles can be arranged as a set of independent and embed-
ded cycles then #2-SAT(Σ) can be computed in polynomial time. We
present a procedure for detecting if a set of cycles can be embedded one
into other. Furthermore, we design a polynomial reduction for given two
restricted intersected cycles redraw those as embedded cycles.
The resulting method for counting models for a 2-CF could be used to
impact directly in the reduction of the complexity time of the algorithms
for other counting problems. For example, for counting independent sets,
counting colouring of graphs, counting cover vertex, etc.
Keywords: #SAT Problem, Exact Combinatorial Algorithms, Embed-
ded Cycles.
1. Introduction
#SAT is a classical #P-complete problem even for formulas which are restricted
to conjunction of clauses with two literals at most, this last problem denoted as
#2-SAT. #SAT is a very hard counting problem, for example, Hunt, et. al. has
shown that #SAT to planar 3-CF formulae (its constrained graph is planar) is
#P-complete [6].
#2-SAT continues being a #P-complete problem if we consider only monotone
formulas or Horn formulas [9]. Even more, #SAT restricted to formulas in the
class (2, 3µ)-CF (the class of conjunctions of 2-clauses where each variable ap-
pears three times at most) is also #P-complete [8].
On the other hand, the maximum polynomial class recognized for #2SAT
is the class (≤ 2, 2µ)-CF (conjunction of binary or unitary clauses where each
variable appears two times at most) [3, 8, 9].
#SAT as well as its decision counterpart - the SAT problem, are a special
concern to Artificial Intelligence (AI), and it has a direct relationship to Au-
tomated Theorem Proving as well as in Approximate Reasoning. For example,
#SAT has applications in estimating the degree of reliability in a communi-
cation network, for computing the degree of belief in propositional theories, in
Bayesian inference, in a truth maintenance systems, for repairing inconsistent
databases [2, 8, 10]. The previous problems come from several AI applications
such as planning, expert systems, data-mining, approximate reasoning, etc.
For example, if we assign an equal degree of belief to all basic ’situations’
that appear in a knowledge base Σ of an intelligent agent, then we can compute
the probability that Σ will be satisified. If Σ involves n variables, the probabilty
to satisfies Σ, is: PΣ = P rob(Σ ≡ ) = #SAT 2n
(Σ)
, where stands for the Truth
value and P rob is used to denote the probability. Thus, to compute the degree
of belief of the agent in a propositional formula F with respect to its knowledge
base Σ, is the fraction of models of Σ that are consistent with the formula F ,
that is, the conditional probability of F with respect to Σ, which is denoted by
PF |Σ = P rob((Σ ∧ F ) ≡ |Σ ≡ ) = #SAT (Σ∧F )
#SAT (Σ) .
One important goal of research is to recognize the class of formulas for Σ
and F where the degree of belief PF |Σ can be done efficiently, and for this, to
develop smart algorithms for solving #SAT is key.
By other way, many combinatorial problems ask about embeddings of graphs
into other objects [7]. For instance, the polynomial time solvable graph planarity
problem ask whether a given graph G, it can be embedded in the plane in such
a way that no two edges intersect (except at a common endpoint).
In our case, we are interested in a particular subclass of planar graphs, those
graphs whose set of cycles can be arranged as independent cycles as well as
embedded cycles.
We have designed some procedures for counting models for 2-CF [3–5]. In this
article, we extend those procedures. Specially, we consider the previous reduction
presented in [5] for translating a pair of intersected cycles with exactly one
common edge to a pair of embedded cycles.The main contribution in this article
is to present a way to detect if a set of cycles can be embedded one into other,
and to show how to compute #SAT for formulas whose constrained graphs have
such topology.
2. Notation and Preliminaries
Let X = {x1 , . . . , xn } be a set of n Boolean variables. A literal is either a variable
x or a negated variable x. As is usual, for each x ∈ X, x0 = x and x1 = x. We
use υ(l) to indicate the variable involved by the literal l.
A clause is a disjunction of different literals (sometimes, we also consider a
clause as a set of literals). For k ∈ IN , a k-clause is a clause consisting of exactly
k literals and, a (≤ k)-clause is a clause with k literals at most. A unary clause
has just one literal and a binary clause has exactly two literals. The empty clause
signals a contradiction. A clause is tautological if it contains a complementary
pair of literals. From now on, we will consider just non-tautological and non-
contradictory clauses. A variable x ∈ X appears in a clause c if either x or x is
an element of c. Let υ(c) = {x ∈ X : x appears in c}.
A Conjunctive Form (CF) is a conjunction of clauses (we also consider a CF
as a set of clauses). We say that Σ is a 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, sµ)-CF, (≤ k, sµ)-CF is a
k-CF, (≤ k) − CF , such that each variable appears no more than s times. For
any CF Σ, let υ(Σ) = {x ∈ X : x appears in any clause of Σ}.
An assignment s for Σ is a function s : υ(Σ) → {0, 1}. An assignment can
be also considered as a set of no complementary pairs of literals. If l ∈ s, being
s an assignment, then s makes l true and makes l false. A clause c is satisfied
by s if and only if c ∩ s = ∅. If for all l ∈ c, l ∈ s then s falsifies c. A CF F is
satisfied by an assignment s if each clause in F is satisfied by s and s falsifies c
if c is not satisfied by s and F is contradicted if it is not satisfied.
Let SAT (Σ) be the set of models that Σ has over υ(Σ). Σ is a contradiction
or unsatisfiable if SAT (Σ) = ∅. Let µυ(Σ) (Σ) = |SAT (Σ)| be the cardinality of
SAT (Σ) and [[n]] denotes the set {1, 2, ..., n}.
Given Σ a CF, the SAT problem consists in determining if Σ has a model.
The #SAT consists of counting the number of models of F defined over υ(Σ).
We will also denote µυ(Σ) (Σ) by #SAT (Σ). When υ(Σ) will clear from the
context, we will omit it as a subscript.
The Graph Representation of a 2-CF
Let Σ be a 2-CF, the constrained graph of Σ is the undirected graph GΣ =
(V, E), with V = υ(Σ) and E = {(υ(x), υ(y)) : (x, y) ∈ Σ}, that is, the vertices
of GΣ are the variables of Σ and for each clause (x, y) in Σ there is an edge
(υ(x), υ(y)) ∈ E. The degree of a node v ∈ V is the number of incident edges to
v. We say that a 2-CF Σ is a cycle, a path or a tree if GΣ is a cycle, a path or a
tree, respectively.
When GΣ contains several cycles, they could be independent or intersected.
We say that to cycles Ci , Cj are independent one to the other if they don’t have
common edges. If a cycle C ∈ GΣ is independent with all the other cycles in G,
we say that C is an independent cycle in GΣ .
Given a 2-CF Σ, a connected component of GΣ is a maximal subgraph such
that for every pair of vertices x, y, there is a path in GΣ from x to y. We say
that the set of connected components of Σ are the subformulas corresponding to
the connected components of GΣ .
If {G1 , . . . , Gr } is a partition in connected components of Σ, then:
µυ(Σ) (Σ) = µυ(G1 ) (G1 ) ∗ · · · ∗ µυ(Gr ) (Gr ) (1)
In order to compute µ(Σ), first we should determine the set of connected
components of Σ, and this procedure is done in linear time [9]. Then, compute
µ(Σ) is translated to compute µυ(G) (G) for each connected component G of Σ.
From now on, when we mention a formula Σ, we suppose that Σ is a connected
component.
3. Basic Procedures for computing #2-SAT
For completeness purposes, we present in this chapter some procedures designed
for us in previous articles [3,4,5] although the new contributions will be devel-
oped until chapter 4.
Case A:
First, let us consider GΣ = (V, E) be a path (also called a chain). Let us write
down its associated formula Σ, without a loss of generality (ordering the clauses
andits literals, if it were necessary), as: Σ= {c1 , ..., cm }
= {x11 , xδ21 }, {x22 , xδ32 }, . . . , {xm−1
m
, xδmm } , where |υ(ci ) ∩ υ(ci+1 )| = 1, i ∈
[[m − 1]], and δi , i ∈ {0, 1}, i = 1, ..., m.
As Σ has m clauses then |υ(Σ)| = n = m + 1. We will compute µ(Σ) in base
to build a series (αi , βi ), i = 1, ..., m, where each pair of the series is associated
to the variable xi of υ(Σ). The value αi indicates the number of times that the
variable xi is ’true’ and βi indicates the number of times that the variable xi
takes value ’false’ over the set of models of Σ.
Let fi be a family of clauses of Σ built as follows: f0 = ∅,fi = {cj }j≤i ,
i ∈ [[m]]. Note that fi ⊂ fi+1 , i ∈ [[m − 1]]. Let SAT (fi ) = {s : s satisfies fi },
Ai = {s ∈ SAT (fi ) : xi ∈ s}, Bi = {s ∈ SAT (fi ) : xi ∈ s}. Let αi =
|Ai |; βi = |Bi | and µi = |SAT (fi )| = αi + βi . From the total number of models
in µi , i ∈ [[m]], there are αi of which xi takes the logical value ’true’ and βi
models where xi takes the logical value ’false’.
In general, we compute the values for (αi , βi ) associated to each node xi ,
i = 2, .., m, according to the signs (i , δi ) of the literals in the clause ci , by the
next recurrence equation:
(β i−1 ,αi−1 + βi−1 ) if (i , δi ) = (0, 0)
(αi−1 + βi−1 ,βi−1 ) if (i , δi ) = (0, 1)
(α , β ) =
i i
(αi−1 ,αi−1 + βi−1 ) if (i , δi ) = (1, 0)
(2)
(αi−1 + βi−1 ,αi−1 ) if (i , δi ) = (1, 1)
Notice that, as Σ = fm then µ(Σ) = µm = αm + βm . We denote with →
the application of one of the four rules of the recurrence (2).
If Σ is a path, we apply (2) in order to compute µ(Σ). The procedure has
a linear time complexity over the number of variables of Σ, since (2) is applied
while we are traversing the path, from the initial node to the final node.
Example 1 Let Υ be a monotone 2-CF with m clauses and where GΥ is a
path. I.e Υ = {(x1 , x2 ), (x2 , x3 ), . . . , (xm−1 , xm )}. Then, at the beginning of the
recurrence (2), (α1 , β1 ) = (1, 1) and (α2 , β2 ) = (2, 1) since (1 , δ1 ) = (1, 1), and
in general, as (i , δi ) = (1, 1), for i ∈ [[m]], then the rule: (αi , βi ) = (αi−1 +
βi−1 , αi−1 ) is always applied while we are scanning each node of the path, thus
the Fibonacci numbers appear!.
µ2 = α2 + β2 = α1 + β1 + α1 = 3,
µ3 = α3 + β3 = µ2 + α2 = 5,
(µi )i≥3 = αi + βi = µi−1 + µi−2
Applying the Fibonacci series for a monotone formula F , we obtain the values
(αi , βi ) : (1, 1) → (2, 1) → (3, 2) → (5, 3) → (8, 5) → (13, 8), ..., and this last
series coincides with the Fibonacci numbers: (F2 , F1 ) → (F3 , F2 ) → (F4 , F3 ) →
(F5 , F4 ) → (F6 , F5 ) → (F7 , F6 )... Then, we infer that (αi , βi ) = (Fi+2 , Fi+1 )
and then µi = Fi+2 + Fi+1 = Fi+3 , i = 1, ..., m. E.g. for m = 5, we have
#SAT (F ) = µ5 Thus, the following theorem follows:
Theorem 1 Let Σ be a monotone 2-CF with n nodes such that GΣ is a path,
then: #SAT (Σ) = Fn+2
Case B:
Let GΣ be a simple cycle with m nodes, that is, all the variables in υ(Σ)
appear twice, |V | = m = n = |E|. Ordering the clauses in Σ in such a way
that | υ(ci ) ∩ υ(ci+1
) |= 1, and ci1 = ci2 whenever i1 ≡ i2 mod m, hence
m
x1 = xm , then Σ = ci = {xi−1
i
, xδi i } , where δi , i ∈ {0, 1}. Decomposing
i=1
Σ as Σ = Σ ∪ cm , where Σ = {c1 , ..., cm−1 } is a path and cm = (xm−1
m
, xδ1m ) is
the edge which conforms with GΣ the simple cycle: x1 , x2 , ..., xm−1 , x1 . We can
apply the linear procedure described in the case A for computing µ(Σ ).
Every model of Σ had determined logical values for the variables: xm−1
and x1 since those variables appear in υ(Σ ). Any model s of Σ satisfies cm
if and only if (x1−
m−1 ∈
m
/ s and x1−δ
m
m
/ s), that is, SAT (Σ ∪ cm ) ⊆ SAT (Σ ),
∈
and SAT (Σ ∪ cm ) = SAT (Σ ) − {s ∈ SAT (Σ ) : s falsifies cm }. Let X =
Σ ∪ {(x1− 1−δm
m−1 ) ∧ (xm
m
)}, then µ(X) can be computed as a path with two unary
clauses, that is:
#SAT (Σ) = µ(Σ) = µ(Σ ) − µ(X)
(3)
= µ(Σ ) − µ(Σ ∧ (x1− 1−δm
m−1 ) ∧ (xm
m
))
For example, let us consider
Σ be a monotone m 2-CF with m clauses such
i δi
that GΣ is a simple cycle. Σ = ci = {xi−1 , xi } , where δi = i = 1, υ(ci ) ∩
i=1
υ(ci+1 ) = {xi }, and ci1 = ci2 whenever i1 ≡ i2 mod m, hence x1 = xm . Let Σ =
{c1 , ..., cm−1 }, then: µ(Σ ) = µm−1 = Fm+2 for theorem 1. As m = δm = 1 then
µ(X) = µ(Σ ∧(x1 )∧(xm−1 )) which is computed by the series: (α1 , β1 ) = (0, 1) =
(F0 , F1 ) since (x1 ) ∈ X, (α2 , β2 ) = (1, 0) = (F1 , F0 ); (α3 , β3 ) = (1, 1) = (F2 , F1 );
(α4 , β4 ) = (2, 1) = (F3 , F2 ); and in general (αi , βi ) = (Fi , Fi−1 ), then for the
variable xm−1 , (αm−1 , βm−1 ) = (Fm−1 , Fm−2 ), then µ(X) = βm−1 = Fm−2
since (xm ) ∈ X. Finally, #SAT (Σ) = µ(Σ) = µ(Σ ) − µ(X) = Fm+2 − Fm−2 .
Thus, the following theorem holds.
Theorem 2 Let Σ be a monotone 2-CF with m clauses and where GΣ is a
simple cycle, then: #SAT (Σ) = Fm+2 − Fm−2 .
Example 2 Let Σ = {ci }6i=1 = {{x1 , x2 }, {x2 , x3 }, {x3 , x4 }, {x4 , x5 }, {x5 , x6 },
{x6 , x1 }} be a monotone 2-CF which represents the cycle GΣ =(V ,E), see Figure
1. Let G = (V, E ) where E = E ∪ {c6 }, that is, the new graph G is Σ minus
the edge c6 . Applying theorem 2, #SAT (Σ) = F7 + F5 = 13 + 5 = 18
X1 X2 X3 X4 X5 X 6
(α1 , β1 ) → (α2 , β2 ) → (α3 , β3 ) → (α4 , β4 ) → (α5 , β5 ) → (α6 , β6 )
(1, 1) → (2, 1) → (3, 2) → (5, 3) → (8, 5) → (13, 8)
(0, 1) → (1, 0) → (1, 1) → (2, 1) → (3, 2) → (5, 3)
⇒ (13, 8) − (0, 3) = (13, 5)
Fig. 1. Computing #SAT (Σ) when GΣ is a cycle
Case C:
Let GΣ = (V, E) be a tree. As GΣ Notice that since GΣ is a tree, all of its edges
are tree edges and, there are no back edges. We denote with (αv , βv ) the associ-
ated pair to a node v (v ∈ GΣ ). We compute #SAT (Σ) while we are traversing
GΣ in depth-first search.
Algorithm Count Models for trees(AΣ )
Input: AΣ the tree defined by a depth-first search over GΣ
Output: The number of models of Σ
Procedure: Traversing AΣ in depth-first, and when a node v ∈ AΣ is left,
assign:
1. (αv , βv ) = (1, 1) if v is a leaf node in AΣ .
2. If v is a father node with a list of child nodes associated, i.e., u1 , u2 , ..., uk
are the child nodes of v, then as we have already visited all child nodes, then
each pair (αuj , βuj ) j = 1, ..., k has been defined based on ( 2). (αvi , βvi ) is
obtained by applying (2) over (αi−1 , βi−1 ) = (αuj , βuj ). This step is iterated
k
until computes the values (αvj , βvj ), j = 1, ..., k. Finally, let αv = j=1 αvj
k
and βv = j=1 βvj .
3. If v is the root node of AΣ then returns(αv + βv ).
This procedure returns the number of models for Σ in time O(n + m) which
is the necessary time for traversing GΣ in depth-first search.
Notice that the combination of the procedure for trees and the processing
of cycles (equation 3) can be applied for computing #SAT (Σ) if GΣ is a
graph where the depth-first search generates a tree and a set of independent
fundamental cycles.
Thus, the procedures presented in this section, for computing #SAT (Σ)
being Σ a cycle, a path, a tree, or a tree union independent cycles, each one
runs in linear time over the size of the graph.
The class of Boolean formulas Σ depth-first search builds a tree and a set
of fundamental independent cycles conforms a new polynomial instances for
#2-SAT. This class of instances is a superclass of (2, 2µ)-CF, and it has not
restrictions over the number of occurrences of a variable in the formulas, although
(2, 3µ)-CF is a #P -complete problem.
4. Processing Embedded Cycles
Given a constrained graph GΣ of a Boolean formula Σ, if GΣ contains some
intersected cycles, we look at if those cycles can be considered as embedded
cycles, see figure 2. It is possible that some cycles can be expressed as embedded
cycles although they are not initially recognized as such.
In order to recognize when two cycles Ci and Cj can be expressed as embed-
ded cycles, we use the or-exclusive operation. Given two intersected cycles Ci ,
Cj of a graph we say that Ci can be embedded into Cj , if:
a)V (Ci ) ⊂ V (Cj ) : the set of nodes of Ci is a subset of the nodes of Cj .
b)|E(Ci ) − E(Cj )| = 1 : there is only one edge from Ci which is not edge of Cj .
c)Ci ⊕ Cj = Ck : being Ck a new cycle distinct to Ci and Cj and ⊕ is the
or-exclusive operation between the edges of the cycles.
If the cycles Ci and Cj hold the previous three conditions, we say that Ci is
an internal embedded cycle of Cj while Cj is an external embedded cycle of Ci .
Notice that the embedded property can be extended to a set of embedded cycles.
Let D = (C1 , C2 , . . . , Ck ) be a tuple of cycles of GΣ such that Ci is embedded in
Ci+1 , i = 1, . . . , k − 1, then we say that C1 is the most internal embedded cycle
of D while Ck is the most external cycle of D.
Given a tuple of embedded cycles D = (C1 , C2 , . . . , Ck ), we present in this
section how to compute #SAT (D). First, the order of processing is from the most
internal embedded cycle to the most external embedded cycle. The beginning
of the processing of each cycle starts for traversing a cycle in depth-first order,
visiting the nodes of the cycle as a path from its initial node v0 to its end node
vf .
Three computing threads are used for carry on the values of the number of
models for each node which is visted during the depht-first search. So, a com-
puting thread is a sequence of pairs (αi , βi ), i = 1, ...m used for computing the
number of models over a path of m nodes. A main thread, denoted by Lp, is
associated to the spanning tree of the graph, this thread is always active during
all the counting process.
9 103 6 5 1 2 3 4 7 8 11
Fig. 2. An initial graph Ge with embedded cycles
Case 1: Processing an Internal Embedded Cycle
Consider that we are processing the most internal cycle C1 of a tuple D =
(C1 , C2 , . . . , Ck ) of embedded cycles. We starts the depht-first search in the first
node of the path defined by the cycle C1 and assigning the values (α10 , β01 ) =
(1, 1) to the main computing thread, the second thread starts with the values
(α20 , β02 ) = (1, 0) indicating that this thread carry on the number of models of C1
where the first variable x0 does not appear while the third thread starts with the
pair (α30 , β03 ) = (0, 1) indicating that this thread carry on the number of models
of C1 where the first variable x0 appears.
We traverse by C1 as a path from its initial node v0 to its end node vf .
Each time that a new node of the path in C1 is visited, the recurrence (2) is
applied, obtaining: (αi , βi ) → (αi+1 , βi+1 ). When the search arrives to the end
node of the cycle, we have obtained the pairs (α1f , βf1 ), (α2f , βf2 ) and (α3f , βf3 ) cor-
responding with the final pairs of the three different computing threads. Finally,
for processing the back edge in C1 we use the temporal variables αC1 and βC1
defined as: αC1 = α1f , βC1 = βf1 − βf3 , and the numbers of models for the internal
cycle C1 , is: #SAT (C1 ) = αC1 + βC1 .
Case 2: Processing an External Embedded Cycle
If a current cycle Ci is embedded into other Cj , the pairs (α2f , βf2 ) and (α3f , βf3 )
corresponding to the threads for processing Ci are used for processing the exter-
nal cycle Cj . Furthermore, after to process Ci , all the cycle is contracted into a
single node Crsf where s is the number of the initial node and f is the number
of the final node of the path in Ci . Then, the new node Crij is now part of the
path contained in the cycle Cj (see figure 4).
We use the three threads for processing the external cycle Cj , as it was
explained previously. The depth-first search is applied over the path defined by
Cj and the recurrence (2) is applied over each node of the path until arrive
to the node Crsf . When a computing thread arrive to Crsf , each current pair
(αix , βxi ), i = 1, 2, 3 is updated according to the following recurrence.
αix+1 = α2f ∗ αix + α3f ∗ βxi
i
(4)
βx+1 = βf2 ∗ αix + βf3 ∗ βxi , for i = 1, 2, 3.
Obtaining then the new pairs (αix+1 , βx+1 i
), for i = 1, 2, 3. We will denote the
application of the recurrence (4) as (αx , βx ) (αx+1 , βx+1 ).
How it exists an implicit back edge into the contracted node Crsf then we
have to update only the pair (α1x+1 , βx+1 1
) as (α1x+1 , βx+1
1
) = (α1x+1 , βx+1
1
−
1 3
βx ∗ βf ). We will denote the processing of a back edge as , then (αx , βx )
(αx+1 , βx+1 ) meaning the application of the formula (αx+1 , βx+1 ) = (αx+1 , βx+1 −
βx ∗ βf2 ).
The processing of the current cycle continues as in the Case 1 until arrives
to the final node vf of the external cycle Cj . Obtaining new current values for
(α1f , βf1 ),(α2f , βf2 ),(α3f , βf3 ). We illustrate in figures 2-5 how to process a set of
embedded cycles.
Example 3 Let Ge be a graph with embedded cycles (see Figure 2), applying the
case 1 for processing the internal cycle from node 1 to node 4, we obtain the new
node Cr14 . In Figure 4, appears a new graph G2 which contains a cycle from
node 6 to node 8, this cycle has a Cr14 as an internal node. Applying the case
2 the graph G3 is obtained (see Figure 5). This graph has the node Cr68 which
comes from the contracted cycle G2 . And again, the case 2 is applied obtaining
the value for #SAT (Ge ).
1 2 3 4
N odes : N ode1 N ode2 N ode3 N ode4
Lp : (1, 1) → (2, 1) → (3, 2) → (5, 3) = (α14 , β41 )
/ S : (1, 0) → (1, 1) → (2, 1) → (3, 2) = (α24 , β42 )
L1 ∈
L2 ∈ S : (0, 1) → (1, 0) → (1, 1) → (2, 1) = (α34 , β43 )
⇒ (5, 3) − (0, 2) = (5, 2)
Fig. 3. Processing the most internal cycle
6 5 1-4 7 8
G2 N ode6 N ode5 N ode1−4 N ode7 N ode8
Lp : (1, 1) → (2, 1) → (3, 2) (13, 8) (13, 6) → (19, 13) → (32, 19) = (α18 , β81 )
/ S : (1, 0) → (1, 1) → (2, 1) (8, 5) (8, 4) → (12, 8) → (20, 12) = (α28 , β82 )
L1 ∈
L2 ∈ S : (0, 1) → (1, 0) → (1, 1) (5, 3) (5, 2) → (7, 5) → (12, 7) = (α38 , β83 )
⇒ (32, 19) − (0, 7) = (32, 12)
Fig. 4. (G2 ) with the node Cr14 which represents an embedded cycle
4.1. Reducing Intersected Cycles to Embedded Cycles
Suppose that we want to process the graph G on Figure 6, the depth-first search
over G builds the graph on Figure 7, which has to be processed (count the number
of models) as it is illustrated in the same figure. But, if the graph G were reduced
to the equivalent graph on Figure 8, then the number of computing threads
is smaller. Furthermore, we can apply the procedure for processing embedded
9 10 6-8 11
G3 N ode9 N ode10 N ode6−8 N ode11
Lp : (1, 1) → (2, 1) → (3, 2) (84, 50) (84, 36) → (120, 84) = (α111 , β11
1
)
2 2
L1 ∈
/ S : (1, 0) → (1, 1) → (2, 1) (52, 31) (52, 24) → (76, 52) = (α11 , β11 )
L2 ∈ S : (0, 1) → (1, 0) → (1, 1) (32, 19) (32, 12) → (44, 32) = (α311 , β11
3
)
⇒ (120, 84) − (0, 32) = (120, 52)
Fig. 5. (G3 ) with two implicit embedded cycles
1 2
4 3
5 6
Fig. 6. An initial graph G
C2
1 2 3 4 5 6
C1
N odes : N ode1 N ode2 N ode3 N ode4 N ode5 N ode6
Lp : (1, 1) → (2, 1) → (3, 2) → (5, 3)
C1 : (0, 1) → (1, 0) → (1, 1) → (2, 1) closed
C2 → Lp : (0, 2) → (2, 0)
C2 → C1 : (0, 1) → (1, 0) closed
Lp : (5, 3) − (0, 1) = (5, 2) → (7, 5) → (12, 7)
C2 : (2, 0) − (0, 1) = (2, 0) → (2, 2) → (4, 2) closed
⇒ (12, 7) − (0, 2) = (12, 5)
Fig. 7. Computing #SAT (GΣ ) with intersected cycles
cycles as it was explained previously. We design a polynomial reduction whose
main purpose is to translate some intersected cycles as set of embedded cycles.
This polynomial graphical reduction is sketching in the following procedure.
Procedure Graph Reduction
Input: The graph TG = df s(G) and the set C = {C1 , C2 , ..., Ck } containing the
fundamental cycles of the graph G.
Output: An equivalent graph to TG where some of its fundamental cycles were
redrawn as embedded cycles.
Procedure:
1. for i = 1 to k
(a) If not (Ci is intersected with other cycle Cj ∈ C and Ci and Cj are not
embedded and |E(Ci ) ∩ E(Cj )| = 1) then continue
(b) /* in other case apply reduction * /
i. Choose the node vs which is incident to the back edge of Ci and to
the common edge e between Ci and Cj
ii. Redraw Cj starting with the node vs and its edge which is not in
E(Ci ). The cycle Cj is redrawed being the last redrawing edge: e
(the common edge between Ci and Cj ).
iii. From the last node vf of Cj , now we redrawing Ci using its incident
edge which is not e. All the nodes and edges of Ci are redrawing
being the back edge of Ci the last redrawing edge.
The original common edge e is translated now as a back edge.
(c) Continue
C1
3 6 5 4 1 2
C2
G2 N ode3 N ode6 N ode5 N ode4
Lp : (1, 1) → (2, 1) → (3, 2) → (5, 3) = (α14 , β41 )
/ S : (1, 0) → (1, 1) → (2, 1) → (3, 2) = (α24 , β42 )
L1 ∈
L2 ∈ S : (0, 1) → (1, 0) → (1, 1) → (2, 1) = (α34 , β43 )
⇒ (5, 3) − (0, 1) = (5, 2)
G3 N ode3−4 N ode1 N ode2
Lp : (1, 1) (5, 3) (5, 2) → (7, 5) → (12, 7) = (α12 , β21 )
/ S : (1, 0) (3, 2) (3, 2) → (5, 3) → (8, 5) = (α22 , β22 )
L1 ∈
L2 ∈ S : (0, 1) (2, 1) (2, 0) → (2, 2) → (4, 2) = (α32 , β23 )
⇒ (12, 7) − (0, 2) = (12, 5)
Fig. 8. Applying the method for embedded cycles for computing #SAT (G)
This reduction is helping for pre-processing cycles of G, since we have trans-
lated the maximum number of intersected cycles as embedded cycles before to
apply the algorithm for counting models over embedded cycles.
5. Conclusions
We present different efficient procedures to compute #SAT for subclasses of
2-CF. Let Σ be a 2-CF where GΣ (the constrained undirected graph of Σ) is
acyclic or, if GΣ contains cyles they can be drawn as independent cycles and
embedded cycles, in all those cases, we show that #SAT (Σ) is computed in
polynomial time over the length of the formula Σ.
We also show how to detect if a set of cycles can be embedded one into
other. Furthermore, we design a polynomial reduction for given two restricted
intersected cycles redraw those as embedded cycles.
The efficient methods presented here can be adapted for solving other count-
ing problems and then, to incide directly over the complexity time of those
problems.
References
1. Creignou N., Hermann M., Complexity of Generalized Satisfiability Counting Prob-
lems, Information and Computation 125, (1996), 1-12.
2. Darwiche Adnan, On the Tractability of Counting Theory Models and its Appli-
cation to Belief Revision and Truth Maintenance, Jour. of Applied Non-classical
Logics, 11(1-2), (2001), 11-34.
3. De Ita G., Polynomial Classes of Boolean Formulas for Computing the Degree of
Belief, Advances in Artificial Intelligence LNAI 3315, 2004, 430-440.
4. De Ita G., Tovar M., Applying Counting Models of Boolean Formulas to Proposi-
tional Inference, Advances in Computer Science and Engineering, Vol 19, 2006.
5. De Ita G., Contreras M., A Polynomial Graphical Reduction to Speed Up the Count-
ing of Models for Boolean Formulas, Proc. of the Workshop in Logic, Language and
Computation, CEUR Workshop Proceedings, Vol.220, 2006.
6. Harry B. Hunt, Madhav V. Marathe, Venkatesh Radhakrishnan, Richard E.
Stearn, The complexity of planar counting problems, SIAM Journal on Comput-
ing, 27(4):1142-1167, 1998.
7. Johnson David S., The NP-Completeness Column: An Ongoing Guide, J. Algorithms
3, 1982, pp. 89-99.
8. Roth D., On the hardness of approximate reasoning, Artificial Intelligence 82,
(1996), 273-302.
9. Russ B., Randomized Algorithms: Approximation, Generation, and Counting, Dis-
tingished dissertations Springer, 2001.
10. Vadhan Salil P., The complexity of Counting in Sparse, Regular, and Planar
Graphs, SIAM Journal on Computing, Vol. 31, No.2, (2001), 398-427.