The satis ability problem for formulas in two conjunctive Normal Form (2SAT) is solved in polynomial time, and ]2SAT which is the count version of 2SAT is ]P-complete. It has been shown that for certain types of formulas, ]2SAT can be computed in polynomial time. In this paper we de ne a new method, based on embedded cycles, to compute ]2SAT on the so-called outerplanar formulas. Our algorithm's time complexity is given by O(n + m) where n is the number of variables and m the number of clauses of the formula. Although the time complexity is similar to other methods, experimental results show that the new method is faster.
Introduction
]SAT (the problem of model counting for a Boolean formula) concerns
especially to arti cial intelligence (AI), and has a direct relationship with the
automated theorem proving, as well as to approximate reasoning [1{3]. ]SAT is
a ]P complete problem, even for formulas in two conjunctive normal form, so
for complete methods, only exponential time algorithms are known. The exact
algorithm with the best bound until now was presented by Wahlstrom [
In practice there are some tools, called SAT solvers to solve ]SAT in e cient time. sharpSAT is a SAT solver reported in literature as the fastest exact and randomized tool, it uses a component cache system that ensures a minimum evaluation on subformulas, generated in the formula decomposition, which are similar.
Besides sharpSAT, in [
In [
In this paper we present a new method to count models in the so called
outerplanar formulas. This method to compute ]2SAT on outerplanar
formulas is based on a transformation in the input formula on its constraint signed
graph. Evidences show that, using outerplanar formulas as a base case is e cient
compared to [
Another special class of graphs contained into outerplanar graphs is the class
of polygonal array graphs that has been widely used in mathematical chemistry,
since they are molecular graphs used to represent the structural formula of
chemical compounds. In particular, hexagonal arrays are the graph representations of
an important subclass of benzenoid molecules, unbranched catacondensed
benzenoid molecules, which play a distinguished role in the theoretical chemistry of
benzenoid hydrocarbons [
In our case, we are more interested in the application of counting models
on conjunctive normal form formulas as a medium to develop methods for
approximate reasoning. For example, for computing the degree of belief on
propositional formulas, or for building Bayesian models. It is relevant to know how
many models are maintained while input conjunctive normal form formulas are
being updating [
This method works using the embedded form of outerplanar graphs, those embedded graphs are then used to compute ]2SAT in linear time.
The paper is organized as follows, in Section 2 the preliminaries are established. In Section 3 an embedded graph representation of outerplanar formulas is presented. In Section 4, our main procedure is presented, in section 5 the results of the paper are shown and nally, the Conclusion. 2
Let X = fx1; : : : ; xng be a set of n Boolean variables. A literal is either a variable xi or a negated variable xi. As usual, for each xi 2 X, we write xi0 = xi and xi1 = xi. A clause is a disjunction of di erent literals (sometimes, we also consider a clause as a set of literals). For k 2 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 2 X appears in a clause c if either the literal x1 or x0 is an element of c.
A Conjunctive Normal Form (CNF) F is a conjunction of clauses (we also call F a Conjunctive Form). A k-CNF is a CNF containing clauses with at most k literals.
We use (Y ) to express the set of variables involved in the object Y , where Y could be a literal, a clause or a Boolean formula. Lit(F ) is the set of literals which appear in a CNF F , i.e. if X = (F ), then Lit(F ) = X[X = fx11; x01; : : : ; x1n; x0ng. We also denote f1; 2; : : : ; ng by [[n]].
An assignment s for F is a Boolean function s : (F ) ! f0; 1g. An assignment can be also considered as a set which does not contain complementary literals. If x 2 s, being s an assignment, then s turns x true and x1 false, 2 f0; 1g. Considering a clause c and assignment s as a set of literals, c is satis ed by s if and only if c \ s 6= ;, and if for all x 2 c, x1 2 s then s falsi es c.
If F1 F is a formula consisting of some clauses of F , then (F1) (F ), and an assignment over (F1) is a partial assignment over (F ).
Let F be a Boolean formula in CNF, F is satis ed by an assignment s if each clause in F is satis ed 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 satis es F . We will denote as SAT (F ) the set of models for the formula F .
Given a CNF F , the SAT problem consists on determining if F has a model. The ]SAT problem consists of counting the number of models of F de ned over (F ). ]2-SAT denotes ]SAT for formulas in 2-CNF. 2.1
There are some graphical representations of a CNF (see e.g. [
Let F be a 2-CNF, its signed primal graph (constraint graph) is denoted by GF = (V (F ); E(F )), with V (F ) = (F ) and E(F ) = ff (x); (y)g : fx; yg 2 F g, that is, the vertices of GF are the variables of F , and for each clause fx; yg in F there is an edge f (x); (y)g 2 E(F ). For x 2 V (F ), (x) denotes its degree, i.e. the number of incident edges to x. Each edge c = f (x); (y)g 2 E is associated with an ordered pair (s1; s2) of signs, assigned as labels of the edge connecting the literals appearing in the clause. The signs s1 and s2 are related to the literals x and y , respectively. For example, the clause fx0; y1g determines the labelled edge: "x + y" which is equivalent to the edge "y + x".
Formally, let S = f+; g 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 2 E. Let G = (V; E; ) be a signed primal graph with labelled edges on SxS. Let x and y be vertices in V , if e = fx; yg is an edge and (e) = (s; s0), then s(resp:s0) is called the adjacent sign to x(resp:y). We say that a 2-CNF F is a path, cycle, a tree, or an outerplanar graph, if its signed constraint graph GF represents a path, cycle, a tree, an outerplanar graph, respectively. We will omit the signs on the graph if all of them are +.
Notice that a signed primal graph of a 2-CNF can be a multigraph since two
xed variables can be involved in more than one clause of the formula forming so
parallel edges. Furthermore, a unitary clause is represented by a loop (an edge
to join a vertex to itself). A polynomial time algorithm to process parallel edges
and loops to solve ]SAT has been shown in [
Let : 2-CNF ! GF be the function whose domain is the space of Boolean formulas in 2-CNF and codomain the set of multi-graphs, is a bijection. So any 2-CNF formula has a unique signed constraint graph associated via and viceversa, any signed constraint graph GF has a unique formula associated. 2.2
We de ne a set of cumulative operations as macro, in this paper a macro must be
constructed using the method shown in [
A new set of equations must be constructed, associated to every pair of signs ( ; ) of an edge fx ; y g, in a graph. ( + ; + 8( > ) = ><>(( >( > >:((
Counting on acyclic graphs, like tree or paths, using a di erent equation
than [
An outerplanar 2-CNF formula is one whose signed primal graph is ourterplanar
e.g the graph has a planar drawing for which all vertices belong to the outer
face of the drawing. Outerplanar graphs may be characterized (analogously to
Wagner's theorem for planar graphs) by the two forbidden minors K4 and K2;3,
or by their Colin de Verdiere graph invariants. They have Hamiltonian cycles if
and only if they are biconnected, in which case the outer face forms the unique
Hamiltonian cycle. Every outerplanar graph is 3-colorable, and has degeneracy
and treewidth at most 2 [
Using the representation of an outerplanar graph as a graph with embedded cycles, there is a method to solve the most internal cycles as simple cycles, and replacing the set of vertices that form the cycle with a macro. In this way it is possible to count models on any outerplanar graph its representation as embedded graph is known. 3.2
One characteristic of the outerplanar graphs is that they do not contain the subgraph K2;3, this subgraph can be obtained with two cycles intersected by two edges, that is, there exists two common edges between a pair of cycles. With this we found that an outerplanar graph has at most one edge between any pair of cycles (Fig. 1).
1 4 2 3 5 6
Identi cation of common edges is done by constructing an expansion tree of the graph, which we can nd a set of back edges or cycles within the graph, this is necessary to identify intersection edges that belongs to the expansion tree or back edges (Fig. 2).
To substitute an edge of the expansion tree for one of the back edges, for a new construction of a embedded graph, an edge of the expansion tree can become in one of the back edges in the embedded graph (Fig. 3), the following considerations allow this exchange to be made between the sets of tree and back edges: { If a pair of the back edges intersect on a tree edge, the back edge that closes at a low level, on the tree, is replaced by the intersecting tree edge. { If two back edges intersect on a tree edge, and they form two sub-partitions, that is, each one belongs to a di erent branch in the tree. The back edge that closes at a low level, on the tree, is replaced by the intersecting tree edge. 3.3
If we identify the common edges between cycles it is possible to nd an expansion tree, which the common edges form the set of back edges, so that the back edges form an embedded graph.
By obtaining the common edges in a graph and eliminating them, it is possible to generate a set of possible paths, obtaining Cn, a simple cycle of n vertices. This way it is possible to generate multiple expansion trees that can be seen as a set of embedded cycles (Fig. 4).
With these graphs it can be shown that no matter which vertex the construction of the new expansion tree begins on, adding the common edges will always result in an embedded graph (Fig. 5).
1 1 5 2 6 3 7 4 8 9 12 11
10 10 11 12 9 8 4 7 3 6 2 5
By constructing an embedded graph it is possible to assign an order in which each embedded cycle must be solved, inner cycles rst. This way all cycles on outerplanar formulas can be handled independently.
If F consists of disconnected sub-formulas then ]2SAT (F ) = Qk
i=1 ]2SAT (Fi)
where Fi; i = 1; : : : ; k, are the disconnected sub-formulas of F [
Due that we can assign an order to solve inner cycles rst, in embedded graphs, and replace that cycle with a macro. We can compute ]2SAT in a outerplanar graph in linear time.
We built a linear equation, macro, that represents the values mi = ( + ; + ) on each cycle in the embedded graph. And a linear equation for each node ( + ; + ).
Giving the rst transformation in Fig. 5, we can handle two cycles at same time and perform two operation sets, M1 and M2, where the vertices f5; 6; 7g 2 M1 and f8; 12; 11; 10; 9; 4g 2 M2.
5 6 7 (1+0 , 0+1) - (0+0 , 0+1) (1+1 , 1+0) - (0+1 , 0+0) (2+1 , 1+1) - (0+0 , 0+1)
The nal operation gives a new macro M1 = (2 + 1; 1 + 0), a second macro analogously can be obtained M2 = (8+5; 5+0). A third macro can be computed, replacing the embedded cycles, we have that the vertices f5; 7; 8; 4g 2 M3 and fM1; M2g 2 M3 (Fig. 7).
As a result we have M3 = (34 + 13; 15 + 0), to obtain a new set of values when we replace an inner cycle by a macro we need to apply another set of equations. If we have that Mi = ( i + i ; i + i ) and a node with values ( 1 + 1 ; 1 + 1 ), to obtain ( + ; + ): { { { { = = = = i i i i
This set of new equations only needs to use when a macro is applied, then we can compute the next macro M4 where f1; 5; 4; 3; 2g 2 M4 and M3 2 M4, then M4 = (109 + 83; 62 + 0). Finally with the initial values of (1 + 0; 0 + 1) we can obtain the total models in this example, ]SAT (M4) = (192; 62) = 254
A relevant property of a macro, as de ned in this paper, is the possibility to
represent cumulative operations via symbolic variables, making macros
indistinguishable from individual operators. If subsequences of operators are repeated,
a hierarchy of macros can represent a more compactly plan than a simple
operator sequence, replacing each occurrence of a repeating subsequence with a
macro [
The correctness of our method is based in the following Theorem from [
Assigning truth values to the variables x1 and x2 to satisfy fx1; x2g in F1 [F2 gives two disconnected formula, by the hypothesis that F1 \ F2 = fx1; x2g, so the conclusion holds. tu
The previous theorem states that if we know the models of F1 where the truth values of the variables x1 and x2 which joint F1 to another formula F2 via a clause fx1; x2g are known, then we can substitute the models where x1 and x2 appears in F1 into those of F2 considering the truth values of x1 and x2 in F2. 5
We implement our proposal and compare its runtime against sharpSAT which to
the best of our knowledge is the leading sequential implementation.Additionally,
in Table 1, we compare our proposal based on embedded cycles against our
previous version of markSAT based on bags [
Table 1 shows instances of polygonal chains, with three sides each polygon, which provides the maximum number of edges in outerplanar graphs.
Table 3 shows results on polygonal trees using a side-randomizer, which generate graphs with polygons from three to eight sides each.
Table 4 shows the running time of our proposal against sharpSAT using outerplanar graphs as base case in a general formula decomposition. We present a new method for model counting in outerplanar graphs, with linear time complexity.
Our procedure requires the construction of the expansion tree of the outerplanar graphs, which in this case it is done in time O(n), the number of vertices of the input formula. Once an expansion tree has been built a common edge identi cation on both the tree and their back edges is done in time complexity O(m), where m is the number of edges in the graph. A new expansion tree is built with non common edges, in time O(n). Embedded edges can be added in time O( n2 1 ), the maximum number of back edges in a outerplanar graph. Model counting is done in O(n + m).