<!DOCTYPE article PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Archiving and Interchange DTD v1.0 20120330//EN" "JATS-archivearticle1.dtd">
<article xmlns:xlink="http://www.w3.org/1999/xlink">
  <front>
    <journal-meta />
    <article-meta>
      <title-group>
        <article-title>A Minimum Spanning Tree for the #2SAT Problem</article-title>
      </title-group>
      <contrib-group>
        <contrib contrib-type="author">
          <string-name>Guillermo De Ita</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Meliza Contreras</string-name>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <contrib contrib-type="author">
          <string-name>Pedro Bello</string-name>
          <email>pbellog@cs.buap.mx</email>
          <xref ref-type="aff" rid="aff0">0</xref>
        </contrib>
        <aff id="aff0">
          <label>0</label>
          <institution>Faculty of Computer Science, Universidad Aut</institution>
        </aff>
        <aff id="aff1">
          <label>1</label>
          <institution>onoma de Puebla</institution>
        </aff>
      </contrib-group>
      <abstract>
        <p>#2SAT is a classical #P-complete problem. We present here, a novel algorithm for given a 2-CF §, to build a minimum spanning tree for its constraint graph G§ assuming dynamic weights on the edges of the input graph.</p>
      </abstract>
    </article-meta>
  </front>
  <body>
    <sec id="sec-1">
      <title>Introduction</title>
      <p>Counting combinatorial objects over graphs has been an interesting and
important area of research in Mathematics, Physics, and Computer Sciences. Counting
problems, being mathematically interesting by themselves, are closely related to
important practical problems. For instance, reliability issues are often equivalent
to counting problems [2, 3, 5].</p>
      <p>The techniques for building minimum spanning trees have been developed
assuming static weights on the edges of the graph. But for the #2SAT problem [4,
6], instead of static weights we consider dynamic weights determined by the signs
of the edges, as well as the number of partial models associated with the nodes.
We address the construction of the minimum spanning tree of a constraint graph
considering such dynamic weights.
Let § be a 2-CF, the constraint graph of § is the undirected graph G§ =
(V (§); E(§)), with V (§) = À(§) and E(§) = ffÀ(x); À(y)g : fx; yg 2 §g,
i.e. the vertices of G§ are the variables of §, and for each clause fx; yg in §
there is an edge fÀ(x); À(y)g 2 E(§). Each edge has associated an ordered pair
(s1; s2) of signs assigned as labels. For example, the signs s1 and s2 for the clause
fx _ yg are related to the signs of the literals x and y respectively, then s1 = ¡
and s2 = + and the edge is denoted as: x ¡ + y which is equivalent to y + ¡ x.</p>
      <p>A connected component of G is a maximal induced subgraph of G. We say
that the set of connected components of § are the subformulas corresponding to
the connected components of G§ . From now on, when we mention a 2-CF §,
we assume that § is a connected component graph.
3.</p>
      <p>Linear procedures for #2SAT
We present here, some procedures for computing the number of models of a
formula for basic topologies of a graph.</p>
      <p>Procedure A: If § is a path:</p>
      <p>
        The ¯rst pair (®0; ¯0) is (
        <xref ref-type="bibr" rid="ref1 ref1">1,1</xref>
        ) since for any logical value to y0, f0 is satis¯ed.
(®i; ¯i) associated with each variable yi, i = 1; ::; m is computed according to
the signs: ²i; ±i of the literals in the clause ci, by the recurrence (
        <xref ref-type="bibr" rid="ref1">1</xref>
        ). As § = fm
then #SAT (§) = ¹m = ®m + ¯m. We denote with 0 !0 the application of one
of the four rules in the recurrence.
      </p>
      <p>
        (®i; ¯i) =
8(¯i¡1 ;¹i¡1 ) if (²i; ±i) = (0; 0)
&gt;
&gt;&lt;(¹i¡1 ;¯i¡1 ) if (²i; ±i) = (0; 1)
&gt;(®i¡1;¹i¡1 ) if (²i; ±i) = (1; 0)
&gt;:(¹i¡1 ;®i¡1) if (²i; ±i) = (1; 1)
(
        <xref ref-type="bibr" rid="ref1">1</xref>
        )
a) + +
x1
(
        <xref ref-type="bibr" rid="ref1 ref1">1,1</xref>
        )
x2
(
        <xref ref-type="bibr" rid="ref1 ref2">2,1</xref>
        )
+
-
x3
(
        <xref ref-type="bibr" rid="ref2 ref3">2,3</xref>
        )
+ +
x4
(
        <xref ref-type="bibr" rid="ref3 ref5">5,3</xref>
        )
+
x5
(
        <xref ref-type="bibr" rid="ref5">8,5</xref>
        ) =13 models
b)
x1
(
        <xref ref-type="bibr" rid="ref1 ref1">1,1</xref>
        )
+ +
Example 1 Let § = ffx1; x2g; fx2; x3g; fx3; x4g; fx4; x5gg be a path, the series
(®i; ¯i); i 2 [[5]] is computed according to the signs of the edges, as it is illustrated
in ¯gure (1a). A similar path but with complementary signs on the nodes is
shown in (1b).
      </p>
      <p>Let us consider the class P of Boolean functions where their constraint graphs
are paths. For example, ¯gures (1a) and (1b) represent Boolean path functions.
We denote as Pn+ a monotone path with n nodes and where each variable
appears with the same sign (like in (1a)), while Pn¡+ is the n path where the
occurrences of the variables are with complementary signs (like in (1b)), we
call to this last Boolean formula a changing sign path. Let #+ : IN ! IN
be the function which for a n 2 IN , it considers a monotone path Pn+ 2 P
holding that #+(n) = #SAT (Pn+). We can estimate the rate of growth of
#+ since it corresponds with the growth of #SAT (Pn+) when the number of
variables n growth. As #SAT (Pn+) 2 O(Án) with Á = ³ 1+2p5 ´ ¼ 1:618 [1],
then, #+(n) 2 O ³³ 1+2p5 ´n´. Let #¡+ : IN ! IN be a function which for
a n 2 IN it considers a changing sign path Pn¡+ 2 P, and #¡+ holds that
#¡+(n) = #SAT (Pn¡+). Thus, the rate of growth of the function #¡+ is the
same that the growth of #SAT (Pn¡+) when the number of variables n growth,
and as #SAT (Pn¡+) 2 O(n) [1], then #¡+ 2 O(n). Comparing the rates of
growth for P + and P ¡+, we obtain O(#SAT (Pn+)) &gt; O(#SAT (Pn¡+)).</p>
      <p>Procedure B: If § is a tree:
Let § be a 2-CF where its associated constraint graph G§ is a tree. We
denote with (®v; ¯v) the pair associated with the node v (v 2 G§ ). We compute
#SAT (§) considering the methodology used in [1].</p>
      <p>
        Example 2 Let B7+ a monotone balanced tree, like in (2a). And B+¡ the binary
7
balanced tree where each internal node has complementary signs on its incident
child-edges. Applying Count M odels f or trees to both trees, it starts
assigning the pair (
        <xref ref-type="bibr" rid="ref1 ref1">1,1</xref>
        ) to the leaf nodes. The number of models at each level of the
tree is shown in Figure 2. At the level of the root node, the procedure obtains
#SAT(Bn+) = 25 + 16 = 41. And for the second tree, #SAT(B7+¡) = 8 + 8 = 16.
      </p>
      <p>
        (
        <xref ref-type="bibr" rid="ref4 ref5">5,4</xref>
        ) +
(
        <xref ref-type="bibr" rid="ref1 ref4">4,1</xref>
        ) +
a)
(
        <xref ref-type="bibr" rid="ref1 ref2">2,1</xref>
        )+
      </p>
      <p>
        +
(
        <xref ref-type="bibr" rid="ref1 ref1">1,1</xref>
        )
(25,16) = 41
+ (
        <xref ref-type="bibr" rid="ref4 ref5">5,4</xref>
        )
      </p>
      <p>
        - (
        <xref ref-type="bibr" rid="ref1 ref4">1,4</xref>
        )
(
        <xref ref-type="bibr" rid="ref1 ref2">1,2</xref>
        ) - -(
        <xref ref-type="bibr" rid="ref1 ref2">1,2</xref>
        )
      </p>
      <p>
        (
        <xref ref-type="bibr" rid="ref1 ref2">2,1</xref>
        )
+
+
(
        <xref ref-type="bibr" rid="ref1 ref1">1,1</xref>
        ) (
        <xref ref-type="bibr" rid="ref1 ref1">1,1</xref>
        )
      </p>
      <p>
        +
(
        <xref ref-type="bibr" rid="ref1 ref1">1,1</xref>
        )
      </p>
      <p>(8,8) = 16
b)</p>
      <p>
        (
        <xref ref-type="bibr" rid="ref2 ref4">2,4</xref>
        )
(
        <xref ref-type="bibr" rid="ref2 ref2">2,2</xref>
        ) +
(
        <xref ref-type="bibr" rid="ref1 ref2">1,2</xref>
        )
      </p>
      <p>
        (
        <xref ref-type="bibr" rid="ref1 ref1">1,1</xref>
        )
(
        <xref ref-type="bibr" rid="ref1 ref2">2,1</xref>
        )
+
+
(
        <xref ref-type="bibr" rid="ref1 ref2">2,1</xref>
        )+
      </p>
      <p>
        (
        <xref ref-type="bibr" rid="ref1 ref1">1,1</xref>
        ) (
        <xref ref-type="bibr" rid="ref1 ref1">1,1</xref>
        )
+ (
        <xref ref-type="bibr" rid="ref2 ref4">4,2</xref>
        )
+ (
        <xref ref-type="bibr" rid="ref2 ref2">2,2</xref>
        )
(
        <xref ref-type="bibr" rid="ref1 ref2">1,2</xref>
        )
      </p>
      <p>
        (
        <xref ref-type="bibr" rid="ref1 ref1">1,1</xref>
        )
      </p>
      <p>For monotone Boolean formulas whose constraint graph is a balanced binary
tree, like in example 2, we can express how the number of models changes
according with the number of nodes of the tree. E.g. for a monotone binary tree
with 3 nodes (®3; ¯3) = (22; 12) = (4; 1). The following balanced binary tree
has 7 nodes and (®7; ¯7) = (52; 42) = (25; 16). The following tree has 15 nodes
and (®15; ¯15) = (412; 252) = (1681; 625). In general, we obtain the following
recurrence relation for the balanced monotone binary trees Bn+ with n nodes:
#SAT(Bn+) = Fn2=2 + Fn4=4 being Fi the i-th Fibonacci number. This recurrence
relation has an order of growth of O(2(3=4)n).</p>
      <p>On the other hand, the upper bound for the class of binary formulas where
there are complementary signs on the child-edges on each internal node, tree
denoted as Bn+¡ is given by #SAT (Bn+¡) 2 O(2 n2 ). The previous upper bounds
establish a hierarchy for #SAT according to the topology of the constraint
graphs, given as: O(#SAT (Pn¡+)) · O(#SAT (Bn+¡)) · O(#SAT (Pn+)) ·
O(#SAT (Bn+)).
4.</p>
      <p>Building the Minimum Spanning Tree
Let A1; : : : ; An be the sequence of initial charges obtained by the procedures (A)
or (B) for computing #SAT(§). Now, we build a new sequence of pairs which
represent the ¯nal charges (or just the charges) Bn; : : : ; B1, being Bi the charge
of the variable xi 2 À(§), computed as:</p>
      <p>
        Bn = An
Bn¡i = balance(An¡i; Bn¡i+1); i = 1; :::; n ¡ 1
(
        <xref ref-type="bibr" rid="ref2">2</xref>
        )
balance(A; B) is a binary operator between two pairs, e.g. if x s1ys2 is an edge
of the constraint graph G§, and assuming A = (®x; ¯x) be the initial charge of
the variable x, B = (ay; by) be the ¯nal charge of the variable y, then balance
produces a new pair (ax; bx) which will be the ¯nal charge for x, i.e. #SAT(§) =
ax + bx. Let ¹x = ®x + ¯x and ¹y = ay + by. Let P1 = ®¹xx and P0 = ¹¯xx be the
proportion of the number of 1's and 0's in the initial charge of the variable x.
The ¯nal charge (ax; bx) is computed, as:
ax = ay ¢ P1 + by; bx = ¹y ¡ ax if(s1; s2) = (+; +)
bx = by ¢ P0 + ay ; ax = ¹y ¡ bx if(s1; s2) = (¡; ¡)
bx = by ¢ P0 + ay ; ax = ¹y ¡ bx if(s1; s2) = (+; ¡)
ax = ay ¢ P1 + by; bx = ¹y ¡ ax if(s1; s2) = (¡; +)
      </p>
      <p>In the case that the coe±cients P0 or P1 are not integer numbers, the
following formulas are applied for computing the charge of x.</p>
      <p>ax = (by ¡ ay); bx = (¹y ¡ ax) if(s1; s2) = (¡; ¡)
ax = (ay ¡ by); bx = (¹y ¡ ax) if(s1; s2) = (¡; +)
bx = (by ¡ ay) ; ax = (¹y ¡ bx) if(s1; s2) = (+; ¡)
bx = (ay ¡ by) ; ax = (¹y ¡ bx) if(s1; s2) = (+; +)</p>
      <p>
        Note that the essence of the rules in balance consists in applying the inverse
operation utilized via recurrence (
        <xref ref-type="bibr" rid="ref1">1</xref>
        ) during the computation of #SAT(§).
Furthermore, in the case of bifurcations from a father node to a list of child nodes,
the application of recurrence (
        <xref ref-type="bibr" rid="ref3">3</xref>
        ) or (
        <xref ref-type="bibr" rid="ref4">4</xref>
        ) remains valid since each branch edge has
its respective pair of signs.
4.1.
      </p>
      <p>A Procedure for Building Spanning Trees for #2SAT
Given a 2-CF § and its constraint graph G§, a minimum spanning tree, denoted
by T§, is a tree containing all vertices of G§ and such that #SAT (A§) ¸
#SAT (§) and #SAT (A§) is minimum into the set of all spanning trees of G§.</p>
      <p>
        When G§ contains cycles, our proposal works like the well known Kruskal's
algorithm. An initial spanning tree A§ = (V (G§); P Edges) is formed by all
vertices of G§ because all vertices are connected components by themselves, and
all pendant edge of G are edges of the spanning tree (if there are not pendant
edges then an empty set is initially assigned to P Edges).
(
        <xref ref-type="bibr" rid="ref3">3</xref>
        )
(
        <xref ref-type="bibr" rid="ref4">4</xref>
        )
- X1 +
+
+
- X2
+ +
X3 - + X4
      </p>
      <p>
        X1
X2 (
        <xref ref-type="bibr" rid="ref1 ref1">1,1</xref>
        )
(
        <xref ref-type="bibr" rid="ref1 ref2">2,1</xref>
        )
(
        <xref ref-type="bibr" rid="ref2 ref2">2,2</xref>
        )
X4
+
- X6
+
X6
(
        <xref ref-type="bibr" rid="ref1 ref2">2,1</xref>
        )
(
        <xref ref-type="bibr" rid="ref1 ref3">3,1</xref>
        )
X6
(
        <xref ref-type="bibr" rid="ref1 ref1">1,1</xref>
        )
(
        <xref ref-type="bibr" rid="ref1 ref2">2,1</xref>
        )
(
        <xref ref-type="bibr" rid="ref2 ref2">2,2</xref>
        )
(
        <xref ref-type="bibr" rid="ref2 ref3">3,2</xref>
        )
X4 - ((44,,23))
+
- X6
(
        <xref ref-type="bibr" rid="ref1 ref2">2,1</xref>
        )
(
        <xref ref-type="bibr" rid="ref1 ref3">3,1</xref>
        )
(
        <xref ref-type="bibr" rid="ref1 ref4">4,1</xref>
        )
(
        <xref ref-type="bibr" rid="ref1 ref5">5,1</xref>
        )
(
        <xref ref-type="bibr" rid="ref1 ref6">6,1</xref>
        )
      </p>
      <p>The ¯rst step of our procedure consists in detecting the potential edges which
could generate change of signs when a node will be visited,(see ¯g. 3b). In each
step, each edge with one of its end-points in a node of A§ and the other
endpoint in a node not included in A§ . While the procedure detects an edge e 2 E
which generate change of signs on the incident edges of a same node, such edge
e is added to A§ . When there are more than one edge E generating change of
signs or there are not such edges the procedure reviews how increase the number
of models when an edge e 2 E would be added to A§ , for this in each node an
inverse counting is calculated ,(see ¯g. 3c). The resulting spanning tree (see ¯g.
3d) with a total number of models of 7=6+1.</p>
      <p>The edge e 2 E which infers a minimal increment on #SAT(A§ ) with respect
to any other edge in E, is selected to be added to A§ . Notice that the increment
on the number of models depends mainly of the signs of e as well as the charge
of the two-endpoints of e. There are a set of strategies used for detecting the
edges in (E(G§ ) ¡ E(A§ )) which infer minimal increment on #SAT(A§ ). Such
strategies are: In general if two edges e1 and e2 generate the same increment on
the number of models of A§ e1 is preferred over e2 if e1 could bring about a
change of signs, in the following steps, on its incident node, if the edge e connects
A§ with one extra-node and generates complementary signs on one of its
endpoints, then e is an optimal selection, and it is preferable to obtain a path than
a tree when the signs on the edges are the same.
Let P Edges = fe 2 E(G§) : e is a pendant edge g;
All Edges := E(G) ¡ P Edges; Cs := ;; fSet of potential edgesg
A§ := (V (G); P Edges); fall pendant edges are part of the Treeg
CandEdge = SelectC andidateEdges(All Edges) fSet of candidate semi-edges g
F irstEdge = U nionC andidateEdges(CandEdge) flooking for a complete edgeg
if F irstEdge &lt;&gt; ; then</p>
      <p>E(A§) := E(A§) [ fF irstEdgeg; Initialize(V ect M odels; 1; 1) ;</p>
      <p>Count M odels(A§; V ect M odels); InverseOrderCount(A§; V ect M odels);
end if
while (All Edges &lt;&gt; ;) do</p>
      <p>Count M odels(All Edges; V ect M odels); fcount models by each potential edgeg
Sel Edge = minfV ect M odelsg; fselect the edge which minimum incrementalg
if jSel Edgej &gt; 1 then</p>
      <p>Cs = F ind(T est; A§); flooking for edges which could generate change of signsg
T est = complete(Cs); fchoose edges generating change of sign on the nodesg
Sel Edge = F irst(T est); fSelect an edge keeping potential change of signg
end if
All Edges := All Edges ¡ fSel Edgeg; E(A§) := E(A§) [ fSel Edgeg;
All Edges := All Edges ¡ Edges Cycles(A§; All Edges); fdelete cyclesg
end while
5.</p>
    </sec>
    <sec id="sec-2">
      <title>Conclusions</title>
      <p>We consider a new line of researching of building spanning trees with dynamic
weights determined by the signs of the edges and the partial number of models
associated with the endpoints of the edges. This consideration allows us, given
a 2-CF §, to build its minimum spanning tree A§ such that #SAT(A§ ) is a
minimum upper bound for #SAT(§). To build e±ciently the minimum spanning
tree of a 2-CF is very helpful in the research for determining frontiers between
e±cient and exponential counting procedures for the #2SAT problem.</p>
    </sec>
  </body>
  <back>
    <ref-list>
      <ref id="ref1">
        <mixed-citation>
          1.
          <string-name>
            <surname>De Ita</surname>
            <given-names>G</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Bello</surname>
            <given-names>P</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Contreras</surname>
            <given-names>M</given-names>
          </string-name>
          ,
          <article-title>New Polynomial Classes for #2SAT Established Via Graph-Topological Structure, Jour</article-title>
          .
          <source>Engineering Letters</source>
          , Vol.
          <volume>15</volume>
          (
          <issue>2</issue>
          ), (
          <year>2007</year>
          ), pp.
          <fpage>250</fpage>
          -
          <lpage>258</lpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref2">
        <mixed-citation>
          2.
          <string-name>
            <surname>Dyer</surname>
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Greenhill</surname>
            <given-names>C.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Some</surname>
          </string-name>
          #
          <article-title>P-completeness Proofs for Colourings and</article-title>
          Independent Sets, Research Report Series, University of Leeds,
          <year>1997</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref3">
        <mixed-citation>
          3.
          <string-name>
            <surname>Greenhill</surname>
            <given-names>Catherine</given-names>
          </string-name>
          ,
          <article-title>The complexity of counting colourings and independent sets in sparse graphs and hypergraphs"</article-title>
          ,
          <source>Computational Complexity</source>
          ,
          <volume>9</volume>
          (
          <issue>1</issue>
          ):
          <fpage>52</fpage>
          -
          <lpage>72</lpage>
          ,
          <year>2000</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref4">
        <mixed-citation>
          4.
          <string-name>
            <surname>Russ</surname>
            <given-names>B.</given-names>
          </string-name>
          ,
          <string-name>
            <surname>Randomized</surname>
            <given-names>Algorithms</given-names>
          </string-name>
          : Approximation, Generation, and
          <string-name>
            <surname>Counting</surname>
          </string-name>
          , Distinguished dissertations Springer,
          <year>2001</year>
          .
        </mixed-citation>
      </ref>
      <ref id="ref5">
        <mixed-citation>
          5.
          <string-name>
            <surname>Roth</surname>
            <given-names>D.</given-names>
          </string-name>
          ,
          <article-title>On the hardness of approximate reasoning</article-title>
          ,
          <source>Arti¯cial Intelligence</source>
          <volume>82</volume>
          , (
          <year>1996</year>
          ), pp.
          <fpage>273</fpage>
          -
          <lpage>302</lpage>
          .
        </mixed-citation>
      </ref>
      <ref id="ref6">
        <mixed-citation>
          6.
          <string-name>
            <surname>WahlstroÄm</surname>
            <given-names>M.</given-names>
          </string-name>
          ,
          <string-name>
            <given-names>A Tighter</given-names>
            <surname>Bound for Counting</surname>
          </string-name>
          Max-Weight Solutions to 2SAT
          <source>Instances, LNCS 5018</source>
          , Springer-Verlag (
          <year>2008</year>
          ), pp.
          <fpage>202</fpage>
          -
          <lpage>213</lpage>
          .
        </mixed-citation>
      </ref>
    </ref-list>
  </back>
</article>