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 embedded 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.
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 appears 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 Automated Theorem Proving as well as in Approximate Reasoning. For example, #SAT has applications in estimating the degree of reliability in a communication 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(Σ ≡ ) = #SA2nT (Σ) , 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 ) ≡ |Σ ≡ ) = ##SASAT(TΣ(Σ∧F) ) .
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.
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 noncontradictory 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.
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)
(
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.
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 developed until chapter 4.
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 and its literals, if it were necessary), as: Σ = {c1, ..., cm} =
{x11, xδ21 }, {x22, xδ32 }, . . . , {xmm−1, 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, βi) =
(βi−1 ,αi−1 + βi−1) if ( i, δi) = (0, 0)
(αi−1 + βi−1,βi−1 ) if ( i, δi) = (
Notice that, as Σ = fm then µ(Σ) = µm = αm + βm. We denote with →
the application of one of the four rules of the recurrence (
If Σ is a path, we apply (
µ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) : (
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 =m ci2 whenever i1 ≡ i2 mod m, hence x1 = xm, then Σ = ci = {xi−i1, xiδi } i=1 , where δi, i ∈ {0, 1}. Decomposing Σ as Σ = Σ ∪ cm, where Σ = {c1, ..., cm−1} is a path and cm = (xmm−1, 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 (x1m−−1m ∈/ s and x1m−δm ∈/ s), that is, SAT (Σ ∪ cm) ⊆ SAT (Σ ),
and SAT (Σ ∪ cm) = SAT (Σ ) − {s ∈ SAT (Σ ) : s falsifies cm}. Let X =
Σ ∪ {(x1m−−1m ) ∧ (x1m−δm )}, then µ(X) can be computed as a path with two unary
clauses, that is:
#SAT (Σ) = µ(Σ) = µ(Σ ) − µ(X)
= µ(Σ ) − µ(Σ ∧ (x1m−−1m ) ∧ (x1m−δm ))
(
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}i6=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
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 associated 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) = (
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.
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 embedded 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 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. 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
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) =
(
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 (
If a current cycle Ci is embedded into other Cj , the pairs (αf2 , βf2) and (αf3 , βf3) corresponding to the threads for processing Ci are used for processing the external 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 (
αix+1 = αf2 ∗ αix + αf3 ∗ βxi βx+1 = βf2 ∗ αix + βf ∗ βxi, for i = 1, 2, 3.
i 3
(
Obtaining then the new pairs (αix+1, βxi+1), for i = 1, 2, 3. We will denote the
application of the recurrence (
How it exists an implicit back edge into the contracted node Crsf then we have to update only the pair (α1x+1, βx1+1) as (α1x+1, βx1+1) = (α1x+1, βx1+1 − β1
x ∗ βf3). 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 (αf1 , βf1),(αf2 , βf2),(αf3 , β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 Nodes : Node1 Node2 Node3 Node4
Lp : (
⇒ (
N ode11 (120, 84) = (α111, β111) (76, 52) = (α121, β121) (44, 32) = (α131, β131)
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.
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 5
C2 3 6 4 1
2
G2 Node3 Node6 Node5
Lp : (
Node4
(
2
(
3
Node1
(
Node2
(
2
(
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 translated the maximum number of intersected cycles as embedded cycles before to apply the algorithm for counting models over embedded cycles. 5.
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 counting problems and then, to incide directly over the complexity time of those problems.