<?xml version="1.0" encoding="UTF-8"?>
<TEI xml:space="preserve" xmlns="http://www.tei-c.org/ns/1.0" 
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" 
xsi:schemaLocation="http://www.tei-c.org/ns/1.0 https://raw.githubusercontent.com/kermitt2/grobid/master/grobid-home/schemas/xsd/Grobid.xsd"
 xmlns:xlink="http://www.w3.org/1999/xlink">
	<teiHeader xml:lang="en">
		<fileDesc>
			<titleStmt>
				<title level="a" type="main">A Minimum Spanning Tree for the #2SAT Problem</title>
			</titleStmt>
			<publicationStmt>
				<publisher/>
				<availability status="unknown"><licence/></availability>
			</publicationStmt>
			<sourceDesc>
				<biblStruct>
					<analytic>
						<author>
							<persName><forename type="first">Guillermo</forename><surname>De Ita</surname></persName>
							<email>deita@cs.buap.mx</email>
							<affiliation key="aff0">
								<orgName type="department">Faculty of Computer Science</orgName>
								<orgName type="institution">Universidad Autónoma de Puebla</orgName>
							</affiliation>
						</author>
						<author>
							<persName><forename type="first">Meliza</forename><surname>Contreras</surname></persName>
							<email>mcontreras@cs.buap.mx</email>
							<affiliation key="aff0">
								<orgName type="department">Faculty of Computer Science</orgName>
								<orgName type="institution">Universidad Autónoma de Puebla</orgName>
							</affiliation>
						</author>
						<author>
							<persName><forename type="first">Pedro</forename><surname>Bello</surname></persName>
							<email>pbello@cs.buap.mx</email>
							<affiliation key="aff0">
								<orgName type="department">Faculty of Computer Science</orgName>
								<orgName type="institution">Universidad Autónoma de Puebla</orgName>
							</affiliation>
						</author>
						<title level="a" type="main">A Minimum Spanning Tree for the #2SAT Problem</title>
					</analytic>
					<monogr>
						<imprint>
							<date/>
						</imprint>
					</monogr>
					<idno type="MD5">050AD03576097D25A454414863A2B208</idno>
				</biblStruct>
			</sourceDesc>
		</fileDesc>
		<encodingDesc>
			<appInfo>
				<application version="0.7.2" ident="GROBID" when="2023-03-25T07:13+0000">
					<desc>GROBID - A machine learning software for extracting information from scholarly documents</desc>
					<ref target="https://github.com/kermitt2/grobid"/>
				</application>
			</appInfo>
		</encodingDesc>
		<profileDesc>
			<textClass>
				<keywords>Counting the Number of Models, Minimum Spanning Tree</keywords>
			</textClass>
			<abstract>
<div xmlns="http://www.tei-c.org/ns/1.0"><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></div>
			</abstract>
		</profileDesc>
	</teiHeader>
	<text xml:lang="en">
		<body>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="1.">Introduction</head><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 <ref type="bibr" target="#b1">[2,</ref><ref type="bibr" target="#b2">3,</ref><ref type="bibr" target="#b4">5]</ref>.</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 <ref type="bibr" target="#b3">[4,</ref><ref type="bibr" target="#b5">6]</ref>, 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.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="2.">Preliminaries</head><p>Let Σ be a 2-CF, the constraint graph of Σ is the undirected graph G Σ = (V (Σ), E(Σ)), with V (Σ) = υ(Σ) and E(Σ) = {{υ(x), υ(y)} : {x, y} ∈ Σ}, i.e. the vertices of G Σ are the variables of Σ, and for each clause {x, y} in Σ there is an edge {υ(x), υ(y)} ∈ E(Σ). Each edge has associated an ordered pair (s 1 , s 2 ) of signs assigned as labels. For example, the signs s 1 and s 2 for the clause {x ∨ y} are related to the signs of the literals x and y respectively, then s 1 = − and s 2 = + 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.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="3.">Linear procedures for #2SAT</head><p>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 first pair (α 0 , β 0 ) is (1,1) since for any logical value to y 0 , f 0 is satisfied. (α i , β i ) associated with each variable y i , i = 1, .., m is computed according to the signs: i , δ i of the literals in the clause c i , by the recurrence <ref type="bibr" target="#b0">(1)</ref>. As Σ = f m then #SAT (Σ) = µ m = α m + β m . We denote with → the application of one of the four rules in the recurrence. </p><formula xml:id="formula_0">(α i , β i ) =        (β i−1 ,µ i−1 ) if ( i , δ i ) = (0, 0) (µ i−1 ,β i−1 ) if ( i , δ i ) = (0, 1) (α i−1 ,µ i−1 ) if ( i , δ i ) = (1, 0) (µ i−1 ,α i−1 ) if ( i , δ i ) = (1, 1) (1) a) x2 x1 x3 x4 x5 + + + + + + - -<label>(1,1) (2,3) (2,1) (5,3) (8,5) =13 models b</label></formula><formula xml:id="formula_1">) x2 x1 x3 x4 x5 + + - + + - - +<label>(1,1) (1,3) (2,1) (4,1) (5,1) =6 models</label></formula><formula xml:id="formula_2">(α i , β i ), i ∈ [[5]] is computed</formula></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head>according to the signs of the edges, as it is illustrated in figure (1a). A similar path but with complementary signs on the nodes is shown in (1b).</head><p>Let us consider the class P of Boolean functions where their constraint graphs are paths. For example, figures (1a) and (1b) represent Boolean path functions. We denote as P + n a monotone path with n nodes and where each variable appears with the same sign (like in (1a)), while P −+ n 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.</p><formula xml:id="formula_3">Let # + : IN → IN be the function which for a n ∈ IN , it considers a monotone path P + n ∈ P holding that # + (n) = #SAT (P + n ).</formula><p>We can estimate the rate of growth of # + since it corresponds with the growth of #SAT (P + n ) when the number of variables n growth. As #SAT (P </p><formula xml:id="formula_4">+ n ) ∈ O(φ n ) with φ = 1+ √ 5 2 ≈ 1.618 [1], then, # + (n) ∈ O</formula><formula xml:id="formula_5"># −+ (n) = #SAT (P −+ n ).</formula><p>Thus, the rate of growth of the function # −+ is the same that the growth of #SAT (P −+ n ) when the number of variables n growth, and as #SAT (</p><formula xml:id="formula_6">P −+ n ) ∈ O(n) [1], then # −+ ∈ O(n).</formula><p>Comparing the rates of growth for P + and P −+ , we obtain O(#SAT</p><formula xml:id="formula_7">(P + n )) &gt; O(#SAT (P −+ n )). Procedure B: If Σ is a tree:</formula><p>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 ∈ G Σ ). We compute #SAT (Σ) considering the methodology used in <ref type="bibr" target="#b0">[1]</ref>.</p><p>Example 2 Let B + 7 a monotone balanced tree, like in (2a). And B +− 7 the binary 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 <ref type="bibr" target="#b0">(1,</ref><ref type="bibr" target="#b0">1)</ref> to the leaf nodes. The number of models at each level of the tree is shown in Figure <ref type="figure" target="#fig_1">2</ref>. At the level of the root node, the procedure obtains #SAT(B + n ) = 25 + 16 = 41. And for the second tree, #SAT(B +− 7 ) = 8 + 8 = 16.</p><formula xml:id="formula_8">a) b) + - +<label>(1,1) (1,2) (2,2) (2,4) + + + + - - - (1,1) (1,1) (1,1) (2,1) (2,1) (1,2) (2,2) (4,2)</label></formula><p>(8,8) = 16 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 ) = (2 2 , 1 2 ) = (4, 1). The following balanced binary tree has 7 nodes and (α 7 , β 7 ) = (5 2 , 4 2 ) = (25, 16). The following tree has 15 nodes and (α 15 , β 15 ) = (41 2 , 25 2 ) = (1681, 625). In general, we obtain the following recurrence relation for the balanced monotone binary trees B + n with n nodes:</p><formula xml:id="formula_9">+ - +<label>(1,1) (2,1) (4,1) (5,4) + +</label></formula><formula xml:id="formula_10">+ + + + - - -<label>(1,1) (1,1) (1,1) (2,1) (1,2) (1,2) (1,4) (5,4)</label></formula><formula xml:id="formula_11">#SAT(B + n ) = F 2 n/2 + F 4 n/4</formula><p>being F i 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</p><formula xml:id="formula_12">B +− n is given by #SAT (B +− n ) ∈ O(2 n 2</formula><p>). The previous upper bounds establish a hierarchy for #SAT according to the topology of the constraint graphs, given as:</p><formula xml:id="formula_13">O(#SAT (P −+ n )) ≤ O(#SAT (B +− n )) ≤ O(#SAT (P + n )) ≤ O(#SAT (B + n )).</formula></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="4.">Building the Minimum Spanning Tree</head><p>Let A 1 , . . . , A n 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 final charges (or just the charges) B n , . . . , B 1 , being B i the charge of the variable x i ∈ υ(Σ), computed as:</p><formula xml:id="formula_14">B n = A n B n−i = balance(A n−i , B n−i+1 ), i = 1, ..., n − 1 (2)</formula><p>balance(A, B) is a binary operator between two pairs, e.g. if x s 1 s 2 y is an edge of the constraint graph G Σ , and assuming A = (α x , β x ) be the initial charge of the variable x, B = (a y , b y ) be the final charge of the variable y, then balance produces a new pair (a x , b x ) which will be the final charge for x, i.e. #SAT(Σ) = a x + b x . Let µ x = α x + β x and µ y = a y + b y . Let P 1 = αx µ x and P 0 = βx µ x be the proportion of the number of 1's and 0's in the initial charge of the variable x. The final charge (a x , b x ) is computed, as:</p><formula xml:id="formula_15">a x = a y • P 1 + b y ; b x = µ y − a x if(s 1 , s 2 ) = (+, +) b x = b y • P 0 + a y ; a x = µ y − b x if(s 1 , s 2 ) = (−, −) b x = b y • P 0 + a y ; a x = µ y − b x if(s 1 , s 2 ) = (+, −) a x = a y • P 1 + b y ; b x = µ y − a x if(s 1 , s 2 ) = (−, +)<label>(3)</label></formula><p>In the case that the coefficients P 0 or P 1 are not integer numbers, the following formulas are applied for computing the charge of x.</p><formula xml:id="formula_16">a x = (b y − a y ); b x = (µ y − a x ) if(s 1 , s 2 ) = (−, −) a x = (a y − b y ); b x = (µ y − a x ) if(s 1 , s 2 ) = (−, +) b x = (b y − a y ); a x = (µ y − b x ) if(s 1 , s 2 ) = (+, −) b x = (a y − b y ); a x = (µ y − b x ) if(s 1 , s 2 ) = (+, +)<label>(4)</label></formula><p>Note that the essence of the rules in balance consists in applying the inverse operation utilized via recurrence (1) 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 (3) or (4) remains valid since each branch edge has its respective pair of signs.</p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="4.1.">A Procedure for Building Spanning Trees for #2SAT</head><p>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). The first step of our procedure consists in detecting the potential edges which could generate change of signs when a node will be visited,(see fig. <ref type="figure" target="#fig_3">3b</ref>). 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 ∈ 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 ∈ E would be added to A Σ , for this in each node an inverse counting is calculated ,(see fig. <ref type="figure" target="#fig_3">3c</ref>). The resulting spanning tree (see fig. <ref type="figure" target="#fig_3">3d</ref>) with a total number of models of 7=6+1.</p><p>The edge e ∈ 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 e 1 and e 2 generate the same increment on the number of models of A Σ e 1 is preferred over e 2 if e 1 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.</p></div><figure xmlns="http://www.tei-c.org/ns/1.0" xml:id="fig_0"><head>Fig. 1 .</head><label>1</label><figDesc>Fig. 1. a) Counting models on a monotone paths b)Counting models on a changing sign path</figDesc></figure>
<figure xmlns="http://www.tei-c.org/ns/1.0" xml:id="fig_1"><head>1+ √ 5 2 n.</head><label>2</label><figDesc>Let # −+ : IN → IN be a function which for a n ∈ IN it considers a changing sign path P −+ n ∈ P, and # −+ holds that</figDesc></figure>
<figure xmlns="http://www.tei-c.org/ns/1.0" xml:id="fig_2"><head>Fig. 2 .</head><label>2</label><figDesc>Fig. 2. a) Counting models over a monotone balanced tree, b) Counting models over a non-monotone balanced tree</figDesc></figure>
<figure xmlns="http://www.tei-c.org/ns/1.0" xml:id="fig_3"><head>Fig. 3 .</head><label>3</label><figDesc>Fig.3. Phases on the construction of the minimum spanning tree from an initial constraint graph .</figDesc></figure>
		</body>
		<back>
			<div type="annex">
<div xmlns="http://www.tei-c.org/ns/1.0"><p>(</p><p>(2,1) </p></div>
<div xmlns="http://www.tei-c.org/ns/1.0"><head n="5.">Conclusions</head><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 efficiently the minimum spanning tree of a 2-CF is very helpful in the research for determining frontiers between efficient and exponential counting procedures for the #2SAT problem.</p></div>			</div>
			<div type="references">

				<listBibl>

<biblStruct xml:id="b0">
	<analytic>
		<title level="a" type="main">New Polynomial Classes for #2SAT Established Via Graph-Topological Structure</title>
		<author>
			<persName><forename type="first">De</forename><surname>Ita</surname></persName>
		</author>
		<author>
			<persName><forename type="first">G</forename><surname>Bello</surname></persName>
		</author>
		<author>
			<persName><forename type="first">P</forename><surname>Contreras</surname></persName>
		</author>
		<author>
			<persName><forename type="first">M</forename></persName>
		</author>
	</analytic>
	<monogr>
		<title level="j">Jour. Engineering Letters</title>
		<imprint>
			<biblScope unit="volume">15</biblScope>
			<biblScope unit="issue">2</biblScope>
			<biblScope unit="page" from="250" to="258" />
			<date type="published" when="2007">2007</date>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b1">
	<monogr>
		<title level="m" type="main">Some #P-completeness Proofs for Colourings and Independent Sets</title>
		<author>
			<persName><forename type="first">M</forename><surname>Dyer</surname></persName>
		</author>
		<author>
			<persName><forename type="first">C</forename><surname>Greenhill</surname></persName>
		</author>
		<imprint>
			<date type="published" when="1997">1997</date>
		</imprint>
		<respStmt>
			<orgName>Research Report Series ; University of Leeds</orgName>
		</respStmt>
	</monogr>
</biblStruct>

<biblStruct xml:id="b2">
	<analytic>
		<title level="a" type="main">The complexity of counting colourings and independent sets in sparse graphs and hypergraphs</title>
		<author>
			<persName><forename type="first">Catherine</forename><surname>Greenhill</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="j">Computational Complexity</title>
		<imprint>
			<biblScope unit="volume">9</biblScope>
			<biblScope unit="issue">1</biblScope>
			<biblScope unit="page" from="52" to="72" />
			<date type="published" when="2000">2000</date>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b3">
	<monogr>
		<author>
			<persName><forename type="first">B</forename><surname>Russ</surname></persName>
		</author>
		<title level="m">Randomized Algorithms: Approximation, Generation, and Counting</title>
				<imprint>
			<publisher>Distinguished dissertations Springer</publisher>
			<date type="published" when="2001">2001</date>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b4">
	<analytic>
		<title level="a" type="main">On the hardness of approximate reasoning</title>
		<author>
			<persName><forename type="first">D</forename><surname>Roth</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="j">Artificial Intelligence</title>
		<imprint>
			<biblScope unit="volume">82</biblScope>
			<biblScope unit="page" from="273" to="302" />
			<date type="published" when="1996">1996</date>
		</imprint>
	</monogr>
</biblStruct>

<biblStruct xml:id="b5">
	<analytic>
		<title level="a" type="main">A Tighter Bound for Counting Max-Weight Solutions to 2SAT Instances</title>
		<author>
			<persName><forename type="first">M</forename><surname>Wahlström</surname></persName>
		</author>
	</analytic>
	<monogr>
		<title level="j">LNCS</title>
		<imprint>
			<biblScope unit="volume">5018</biblScope>
			<biblScope unit="page" from="202" to="213" />
			<date type="published" when="2008">2008</date>
			<publisher>Springer-Verlag</publisher>
		</imprint>
	</monogr>
</biblStruct>

				</listBibl>
			</div>
		</back>
	</text>
</TEI>
