=Paper=
{{Paper
|id=Vol-451/paper-8
|storemode=property
|title=Computing #2-SAT of Grids, Grid-Cylinders and Grid-Tori Boolean Formulas
|pdfUrl=https://ceur-ws.org/Vol-451/paper10guillen.pdf
|volume=Vol-451
|dblpUrl=https://dblp.org/rec/conf/rcra/GuillenLI08
}}
==Computing #2-SAT of Grids, Grid-Cylinders and Grid-Tori Boolean Formulas==
https://ceur-ws.org/Vol-451/paper10guillen.pdf
Computing #2-SAT of Grids, Grid-Cylinders and
Grid-Tori Boolean Formulas
C. Guillén1,2 , A. López López1 , and G. De Ita2
1
Coordinación de Ciencias Computacionales
Inst. Nac. de Astrofı́sica Óptica y Electrónica
Tonantzintla Pue. 72840, México
cguillen@inaoep.mx
2
Facultad de Ciencias de la Computación
Benemérita Universidad Autónoma de Puebla
14 Sur y Av. Sn. Claudio Edif 135 Puebla, México
allopez,deita@inaoep.mx
Abstract
We present an adaptation of transfer matrix method for signed
grids, grid-cylinders and grid-tori. We use this adaptation to count
the number of satisfying assignments of Boolean Formulas in 2-CNF
whose corresponding associated graph has such grid topologies.
1 Introduction
The transfer matrix method is a general technique which has been used
to find exact solutions for a great variety of problems. In particular, have
been developed techniques, based on this method, to count structures in a
grid graph Gn,m , e.g., spanning trees, Hamiltonian cycles, independent sets,
acyclic orientations, k-coloring, and so on [1, 2, 7, 9]. In the case of others
grid topologies, as grid-cylinders and grid-tori, there exists little work done
on counting structures. In [9] the transfer matrix technique is used, with
some modifications, to count structures in fixed height grid-cylinders and
tori. In the case of counting satisfying assignments of Boolean formulas
with this type of grid topologies, the work is null as far as we know.
In almost all cases of counting structures in grid graphs, the technique
used follows a transfer matrix formulation. For example, Calkin and Wilf
[2] used this method for computing the number I(Gn,m ) of independent sets
of a grid graph Gn,m and Golin in [9] count the same number (and others
structures) but in grid-cylinders and grid-tori.
The number of independent sets in a grid graph, problem denoted as
I(Gm,n ), is closely related to the “hard-square model” used in statistical
physics and, of particular interest is the so-called “hard-square entropy con-
stant” defined as limm,n→∞ I(Gm,n )1/m·n [1]. Applications also include for
instance tiling and efficient coding schemes in data storage [12].
It is well known that the number of satisfying assignments (models)
of a monotone formula F in two conjunctive normal form 2-CNF, which
Proceedings of the 15th International RCRA workshop (RCRA 2008):
Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion
Udine, Italy, 12–13 December 2008
is a propositional formula formed by a conjunction of disjunctions of two
nonnegative literals, is related with the number of independent sets of the
constrained undirected graph of the formula [11, 9]. The number of mod-
els of a Boolean formula F is denoted as #SAT(F ) and the computation
of #SAT(F ) for formulas in 2-CNF, denoted as #2-SAT, is a classic #P-
complete problem.
There is a significant amount of works on the design of algorithms for
solving #SAT, #2-SAT and #3-SAT [6, 16, 10, 3, 4, 8, 5, 15]. Most of
them are based on branch-and-bound techniques, for example, applying the
recursive decomposition of the input formula based on the classical Davis
and Putnam division rule [8, 4].
Regarding to #2-SAT problem, considering formulas with n variables,
the better time bounds than the trivial O(2n ) have been achieved in the
works of Dahllöf et al. [4], Fürer [8] and Wahlströn [15]. Wahlströn uses
a refinement of the method of analysis, where is extended the concept of
compound measures to multivariate measures in which a leading running
time of O(1.2377n ) has obtained, for weighted formulas in 2-CNF.
An important line of research is related to the determination of the
constraints on the 2-CF formulas which allow us to compute #2-SAT in
polynomial time. In this address, there are few general results, one of them
is due to Vadhan [14] who showed that #2-SAT is solved in polynomial
time for monotone 2-CNF where all variables appear twice at the most.
Roth [11] generalizes the previous results for non only the monotone case,
but continuing to consider two ocurrence per variable at the most. In this
paper, we extend the class of formulas in 2-CNF in which, counting the
number of satisfying assignments can be done in polynomial time.
On the other hand, Bubbley has shown that #2µ-SAT (conjunction of
clauses without bound in its length and where each variable may appear at
most twice) is a #P-Complete problem [13].
In order to extend the transfer matrix method for considering any kind
of 2-CNF’s we have to deal with grid graphs with signed edges. In the case
of counting models of Boolean formulas with this type of grid topologies,
the work is null as far as we know. In this article, we adapt the transfer
matrix method considering three classes of grid topologies: grid graphs,
grid-cylinders and grid-tori obtained from 2-CNF’s not restricted to the
monotone case, and we show how to compute the number of models for
these classes of formulas. The complexity of our method when counting
models in structures of fixed height is polynomial.
2 Preliminaries
For k and l integers such that k < l, we denote the set {k, k + 1, ..., l} by
[k, l]. The Euclidean distance between points u and v in Euclidean 2-space
2
a) b) c) d)
Figure 1: a) Grid, b), c) grid-cylinders and d) grid-tori.
is denoted by d(u, v).
A grid graph of size m × n is a graph Gn,m with vertex set V (n, m) =
[0, n] × [0, m] and edge set E(n, m) = {(u, v) ∈ V 2 (n, m) : d(u, v) = 1}. Let
E1 (n, m) = ({0} × [0, m]) × ({n} × [0, m]) and E2 (n, m) = ([0, n] × {0}) ×
([0, n] × {m}) be two sets of edges.
A grid-cylinder of size m × n is a graph C(n, m) with vertex set V (n, m)
and edge set EC(n, m) = E(n, m) ∪ E 0 (n, m), where E 0 (n, m) ∈ {E1 (n, m),
E2 (n, m)} (see figures 1b and 1c). A grid-tori of size m × n is a graph
T (n, m) with the same vertex set V (n, m) but its edge set is ET (n, m) =
E(n, m) ∪ E1 (n, m) ∪ E2 (n, m) (see figure 1d).
A set I ⊆ V is called an independent set if no two of its elements are
joined by an edge. We describe the method used by Calkin as follows.
Let I(Gn,m ) be the number of independent sets of Gn,m , and let Cm be
the set of all (m + 1)-vectors v of 00 s and 10 s without two consecutive 10 s
(the number of these vectors is F ibm+2 , the (m + 2)-th Fibonacci number).
Let Tm be an F ibm+2 × F ibm+2 symmetric matrix of 00 s and 10 s whose rows
and columns are indexed by the vectors of Cm . The entry of Tm in position
(u, v) is 1 if the vectors u, v are orthogonal, and is 0 otherwise, Tm is called
the transfer matrix for Gn,m . Then, I(Gn,m ) is the sum of all entries of
the n-th power matrix Tm n , i.e., I(G t n
n,m ) = 1 Tm 1, where 1 is the (F ibm+2 )-
0
vector whose entries are all 1 s. For example, if m = 2 and n = 3 we have
that C2 = {(0, 0, 0), (1, 0, 0), (0, 1, 0), (0, 0, 1), (1, 0, 1)},
1 1 1 1 1 17 12 13 12 9
1 0 1 1 0 12 7 10 8 5
T2 = 1 1 0 1 1 and T23 = 13 10 9 10 8 ,
1 1 1 0 0 12 8 10 7 5
1 0 1 0 0 9 5 8 5 3
therefore I(G(2, 3)) = 1T23 1 = 227.
A Boolean formula F is called monotone when each literal appearing in
F occurs with just one of its signs. Given a monotone Boolean formula F in
2-conjunctive normal form (2-CN F ), we can associate an undirected graph
GF = (V, E), called its constrained graph, where V is the set of variables of
F and two vertices of V are connected by an edge in E if they belong to the
same clause of F . Conversely, given an undirected graph G = (V, E), we
3
can associate
V a monotone 2-CN F formula FG with variables V , and where
FG = (u,v)∈E (u ∨ v). We say that a 2-CN F F is a cycle, path, tree, grid,
grid-cylinder or a grid-tori formula if its constrained graph is a cycle, path,
tree, grid, grid-cylinder or a grid-tori, respectively.
3 Extending the Transfer Matrix Method
In order to extend the transfer matrix method for considering any kind of
2-CNF’s we have to deal with grid graphs with signed edges. In this case,
the associated graph of a formula F is a graph GF = (V, E) with labels on
the edges, where V is the set of variables appearing in F , and a clause (l ∨ l0 )
of F determines an ordered pair (s1 , s2 ) of signs assigned as the labels of
the edge connecting the variables appearing in l and l0 . The signs s1 and s2
are related to the signs of the literals l and l0 respectively. For example, the
clause (¬x ∨ y) determines the labelled edge: “x − + y” which is equivalent
to the edge “y + − x”.
Some authors had considered the signs of the literals in the clauses of
a 2-CN F F by using orientation of the edge corresponding to the clause
[12, 13], and then the problem of counting models of F is seen as counting
the number of orientations in its respective constrained graph, which has no
sink.
A graph with labelled edges on a set A is a triplet G = (V, E, ψ), where
(V, E) is a graph, and ψ is a function with domain E and range A. The
valuation ψ(e) is called the label of the edge e ∈ E.
We denote S = {+, −}, S̄ = {±, ∓} and Ŝ = S ∪ S̄. Let Gn,m = (V, E, ψ)
be a grid graph with labelled edges on S 2 . Let x and y be nodes in V . If
e = {x, y} is an edge and ψ(e) = (s, s0 ), then s (s0 ) is called the adjacent
sign to x (y), see figure 2.
s’o s’o
j x
so so
s s’ s
j=j’ x y s’ x x
j’ y
s1
i i’ s’1
a) b) i=i’ a) b)
Fig. 2: Adjacent sign to x(y) Fig. 3: Incident edges on the node x
Let e = ((i, j), (i0 , j 0 )) be an edge of a grid graph Gn,m , if i = i0 and j 6= j 0 ,
e is called a column-edge (see figure 2b), and if i 6= i0 and j = j 0 , e is called
a row-edge (see figure 2a).
If x is a node of Gn,m , then either x has one incident column-edge, or x
has two incident column-edges. If x has one incident column-edge e0 whose
label is (s0 , s00 ), then we define sgnc (x) = s0 , where s0 is the adjacent sign
to x (see figure 3a).
4
If x has two incident column-edges e0 and e1 with labels (s0 , s00 ) and
(s1 , s01 ) respectively ( see figure 3b ), we define sgncc : V → Ŝ as follows
+ if (s0 , s1 ) = (+, +),
− if (s0 , s1 ) = (−, −),
sgncc (x) =
± if (s0 , s1 ) = (+, −),
∓ if (s0 , s1 ) = (−, +).
In general, we can consider the function sgn : V → Ŝ as sgn(x) =
sgnc (x) if x has one incident column-edge or sgn(x) = sgncc (x) if x has two
incident column-edges.
+ + - - + + - -
y0 z0 x0 y0 y0 z0
x0
- + + - - +
+
- + - - - +
- - +
+ + + + - +
x1 y1 z1 x1 y1 y1 z1
+ + + + + + +
+ + + + + + +
z2 x2 y2 y2 z2
x2 y2
+ + + +
+ + + +
G 2,0,1 G
2,1,2
a) b)
Fig. 4: a) Grid G2,2 , b) Subgrids G2,0,1 , G2,1,2
Given Gn,m = (V, E, ψ) a grid graph with labelled edges on S 2 , we
consider for k = 0, ..., n−1 the sub-grid graph with labelled edges Gm,k,k+1 =
(Vk , Ek , ψk ), where Vk = V ∩([k, k+1]×[0, m]), Ek = {(u, v) ∈ Vk2 : d(u, v) =
1} and ψk = ψ |Ek the restriction of ψ to Ek .
Notice that Gm,k,k+1 specifies a grid of two columns and m+1 rows.
If x is a node in Gm,k,k+1 , then x has only one incident row-edge e. For
k = 0, . . . , n − 1 we define sgnk : Vk → S as sgnk (x) = s, where s is the
adjacent sign of x on the incident row-edge e.
For example, let G2,2 be the grid graph illustrated in figure 4a. Then
sgn(x) = +, for x ∈ {x0 , x2 , y2 , z0 , z1 , z2 }, sgn(y0 ) = − and sgn(y1 ) =
sgn(x1 ) = ∓. In G2,0,1 , we have sgn0 (x) = + for all x ∈ V0 . In G2,1,2 ,
sgn1 (x) = + for x ∈ {y2 , z1 , z2 } and sgn1 (x) = − for x ∈ {y0 , y1 , z0 } (see
figure 4b).
Given a vector v = (v0 , v1 , . . . , vm ) ∈ {0, 1}m+1 and a string s = s0 . . . sm
of signs in Ŝ, for m ≥ 0, we define the family of operators ϕs : {0, 1}m+1 →
{0, 1}p , (m + 1 ≤ p ≤ 2m + 2) as ϕs (v) = (s0 v0 , . . . , sm vm ), where
vj if sj = +,
v¯j if sj = −,
sj vj = (1)
(v , v¯ ) if sj = ±,
j j
(v¯j , vj ) if sj = ∓.
for j = 0, . . . , m. For v ∈ {0, 1}, v̄ denotes 1 − v and v̄ denotes (v̄0 , ..., v̄m ).
For instance,
ϕ+,−,±,∓,− (1, 0, 1, 1, 0) = (+1, −0, ±1, ∓1, −0) = (1, 1, (1, 0), (0, 1), 1).
5
In general, we can omit the internal parenthesis given the associative prop-
erty of the cartesian product. In particular, the vector (1, 1, (1, 0), (0, 1), 1)
can be seen as (1, 1, 1, 0, 0, 1, 1).
Let Fm be the set of all (m+1)-vectors v of 00 s and 10 s, and let Cm ⊂ Fm
be the set of all (m + 1)-vectors v of 00 s and 10 s, such that v does not have
two consecutive 10 s. The cardinality of Cm (denoted by |Cm |) is F ibm+2 (the
(m + 2)-th Fibonacci number), while |Fm | = 2m+1 . Given s = s0 s1 · · · sm
a string of signs in Ŝ, we define Fm s = {e ∈ F
m : ϕs (e) ∈ Cm+` }, where
` = |{s ∈ {s0 , ..., sm } : s ∈ S̄}|.
Remark 1. Notice that Cm ⊆ Fm and that the equality holds when
si = + for all i = 0, ..., m. Furthermore, if there exists i ∈ {0, ..., m} such
s | < |C |.
that si ∈ Ŝ, then |Fm m
Let Gn,m be a grid graph of size m × n with labelled edges on the set S 2 ,
we assume that xk0 , . . . , xkm and xk+1 k+1 are the nodes of the k − th
0 , . . . , xm
and (k + 1) − th columns respectively of Gn,m , 0 ≤ k < n (or columns 0 and
1 of Gm,k,k+1 respectively).
For j = k, k + 1, let sj = sj0 sj1 · · · sjm and τ j = τ0j τ1j · · · τm
j
be two string of
j j j j
signs, such that si = sgn(xi ) and τi = sgnk (xi ) for i = 0, · · · , m. Following
the idea proposed in [2], we define a matrix Tk = Tm,k , the transfer matrix
from column k to the column k + 1 of Gn,m as follows. Tk is an | Fm sk+1 | × |
Fm sk | matrix of 00 s and 10 s whose rows and columns are indexed by vectors
(v, u) of Fm sk+1 × F sk . The entry of T in position (v, u) is 1 if the vectors
m k
ϕτ k (u) and ϕτ k+1 (v) are orthogonal, and is 0 otherwise.
Notice that if sji and τij are positive signs for i = 0, · · · , m, j = k, k + 1,
then Tk is the transfer matrix used in the classic transfer method [2].
For example, if G2,2 is the grid graph with labelled edges as it is illus-
trated in figure 4. For G2,0,1 , we have that s0 = + ∓ +, s1 = − ∓ + and
τ 0 = τ 1 = + + +, then F2+∓+ = {u1 , · · · , u4 } and F2−∓+ = {v1 , v2 , v3 , v4 },
where u1 = (0, 0, 0), u2 = (0, 1, 0), u3 = (0, 0, 1), u4 = (1, 1, 0), v1 =
(1, 0, 0), v2 = (0, 1, 0), v3 = (1, 0, 1) and v4 = (1, 1, 0). The transfer matrix
T0 = (aij )4×4 , is a 4 × 4 matrix determined, for 1 ≤ i, j ≤ 4, as aij = 1, if
ϕτ 1 (vi ) · ϕτ 0 (uj ) = 0 and aij = 0 otherwise. Since τ 0 = τ 1 = + + +, we
have ϕτ 1 (vi ) = vi and ϕτ 0 (uj ) = uj . Then
1 1 1 0
1 0 1 0
T0 = 1 1 0 0
(2)
1 0 1 0
For G2,1,2 that is also depicted in figure 4, we have s1 = − ∓ +, s2 =
+ + +, τ 1 = − − + and τ 2 = − + +, then F2−∓+ = {µ1 ,...,µ4 } and
F2+++ = {ν 1 ,...,ν 5 }, where µ1 =(1,0,0), µ2 =(0,1,0), µ3 =(1,0,1), µ4 =(1,1,0),
6
ν 1 =(0,0,0), ν 2 =(1,0,0), ν 3 =(0,1,0), ν 4 =(0,0,1) and ν 5 =(1,0,1). Then,
ϕ−−+ (F2−∓+ ) = {(0, 1, 0), (1, 0, 0), (0, 1, 1), (0, 0, 0)}
and ϕ−++ (F2−∓+ ) = {(1, 0, 0), (0, 0, 0), (1, 1, 0), (1, 0, 1), (0, 0, 1)}.
The transfer matrix T1 = (bij )5×4 , is such that, for 1 ≤ i ≤ 5 and
1 ≤ j ≤ 4, bij = 1, if ϕ−++ (ν i ) · ϕ−−+ (µj ) = 0 and bij = 0 otherwise. Then
1 0 1 1
1 1 1 1
T1 = 0 0 0 1
(3)
1 0 0 1
1 1 0 1
In the case, not necessarily monotone, of a formula F having a con-
strained grid graph Gn,m with labelled edges on S 2 and transfer matrices
T0 , . . . , Tn−1 , we conclude that the sum of all entries of the product ma-
trix Tn−1 · · · T0 is the number of satisfying assignment of F . This fact is
expressed in the following theorem.
Theorem 1. Let F be a grid formula such that its constrained graph is Gn,m
(1 ≤ n) with labelled edges on S 2 , then #SAT (F ) is given by the sum of all
entries of the product matrix Tn−1 · · · T0 , where Tk is the transfer matrix of
the two consecutive columns: k and k + 1 of Gn,m , k = 0, ..., n − 1.
Before detailing the proof, we consider the following example and obser-
vations.
Example 1. Let F = (x0 ∨ y0 ) ∧ (¬y0 ∨ ¬z0 ) ∧ (z0 ∨ z1 ) ∧ (z1 ∨ z2 ) ∧ (z2 ∨ y2 ) ∧
(y2 ∨x2 )∧(x2 ∨x1 )∧(¬x1 ∨x0 )∧(x1 ∨y1 )∧(¬y1 ∨z1 )∧(¬y1 ∨¬y0 )∧(y1 ∨y2 ).The
constrained graph of F is the grid graph G2,2 with labelled edges depicted in
Figure 3. Then, from last example, T0 and T1 are the transfer matrices given
in (2) and (3) respectively. Now, we have that the product matrix T1 T0 is
the following
3 2 2 0
4 2 3 0
T1 T0 =
1 0 1 0
2 1 2 0
3 1 3 0
therefore, #SAT(F ) = 30.
If Fn,m denotes a grid formula having as constrained graph a grid Gn,m ,
for n > 0, we can write
n
^ n−1
^
Fn,m = ( Ci ) ∧ ( R` ) (4)
i=0 `=0
7
where
m−1
^
i
Ci = (η2k xik ∨ η2k+1
i
xik+1 ) (5)
k=0
ηqi ∈ S for q = 0, ..., 2m − 1,
m
^
R` = (τj2` x`j ∨ τj2`+1 x`+1
j ) (6)
j=0
τjr ∈ S for j = 0, ..., m, r ∈ {2`, 2` + 1}. Here, the formulas Ci and R` are
called column-f ormula and row-f ormula respectively.
Notice that for n, m > 0
Fn,m = Fn,m−1 ∧ Cn ∧ Rn−1 , Fm,0 = C0 , F0,n = R0 . (7)
For i = 0, ..., n − 1, we define
Fm,i,i+1 = Ci ∧ Ci+1 ∧ Ri (8)
Note that
n−1
^
Fn,m = Fm,i,i+1 (9)
i=0
If φ : {xi0 , . . . , xim } → {0, 1} is an assignment of values for the variables
of Ci (partial assignments of the variables of Fn,m ), this is denoted by the
(m + 1)-vector (φ(xi0 ), ..., φ(xim )). That is, an assignment for the variables
of Ci can be seen as a vector in {0, 1}m+1 . Observe that, the assignments
of the variables of Fn,m can be considered as a matrix of n columns formed
by the assignments for the variables of C0 , ..., Cn .
For i = 0, ..., n, let ξ0i = η0i , ξm i = ηi i i
2m−1 and ξq = sgn(xq ) for q =
1, ..., m − 1. Also, notice that for v ∈ {0, 1}
½ i i v if η i i
η2q−1 v = η2q 2q−1 = η2q ,
ξqi v = i i (10)
(η2q−1 v, η2q v) otherwise.
To prove the theorem 1, first, we characterize the partial assignments of
the variables of Fn,m such that satisfies each column-formula Ci (lemma 1).
Second, we characterize the pairs of assignments that satisfies the formula
(8), i.e. satisfies two consecutive column-formulas Ci , Ci+1 and the respec-
tive row-formula Ri (lemma 2). Finally, we prove that all matrix of partial
assignments derived from the lemmas 1 and 2, satisfies the formula Fn,m .
Next, for simplicity we omit the superindex i of vji , xij , ηji , τji and ξji .
Lemma 1. The vector u ∈ {0, 1}m+1 satisfies the formula (5) iff u ∈
ξ0 ···ξm
Fm .
8
Proof. By definition, it is clear that ϕξ0 ,...,ξm (u) ∈ Fm+k . Now, if
u = (u0 , ..., um ) satisfies the formula (5), then (η2` u` ∨ η2`+1 u`+1 ) = 1 for
all ` ∈ {0, ..., m − 1}, that is equivalent to (η2` u` , η2`+1 u`+1 ) 6= (1, 1). From
(10) we obtain
(η2` u` , η2`+1 u`+1 )
if η2`−1 = η2` and η2`+1 = η2`+2 ,
(η2` u` , η2`+1 u`+1 , η2`+2 u`+1 )
if η2`−1 = η2` and η2`+1 6= η2`+2 ,
(ξ` u` , ξ`+1 u`+1 ) =
(η2`−1 u` , η2` u` , η2`+1 u`+1 )
if η 2`−1 6= η2` and η2`+1 = η2`+2 ,
(η2`−1 u` , η2` u` , η2`+1 u`+1 , η2`+2 u`+1 )
if η
2`−1 6= η2` and η2`+1 6= η2`+2 .
for all ` ∈ {0, ..., m − 1}. It is straightforward to verify that (ξ` u` , ξ`+1 u`+1 )
does have no two consecutive 1’s, for example, in the third case, the condi-
tions (η2` u` , η2`+1 u`+1 ) 6= (1, 1) and η2`−1 6= η2` imply that (η2`−1 u` , η2` u` ,
η2`+1 u`+1 ) does not have two consecutive 10 s. Therefore, (ξ0 u0 , ..., ξm um ) =
ϕξ0 ,...,ξm (u) does not have two consecutive 10 s, i.e. ϕξ0 ,...,ξm (u) ∈ Cm+k .
Suppose that ϕξ0 ,...,ξm (u) ∈ Cm+k , for ` = 0, ..., m then (ξ` u` , ξ`+1 u`+1 )
does not have two consecutive 10 s. The vector u satisfies the column-
formula Ci (equation (5)), otherwise, there is ` ∈ {0, ..., m − 1} such that
η2` u` ∨ η2`+1 u`+1 = 0, then η2` u` = 1 and η2`+1 u`+1 = 1, from (10)
we have ξ` u` ∈ {1, (η2`−1 u` , 1)} and ξ`+1 u`+1 ∈ {1, (1, η2`+2 u`+1 )}. Then
(ξ` u` , ξ`+1 u`+1 ) has two consecutive 10 s. ¤
For all i = 0, ..., m, we denote the strings ξ0i , ..., ξm
i and τ i , ..., τ i by ξ i
0 m
i
and τ respectively.
ξ i
Lemma 2. The pair (u, v) ∈ {0, 1}2m+2 satisfies Fm,i,i+1 iff (u, v) ∈ Fm ×
ξ i+1
Fm and ϕτ 2i (u) · ϕτ 2i+1 (v) = 0.
Proof. Suppose that u = (u0 , ..., um ) and v = (v0 , ..., vm ) are such
ξi ξ i+1
that (u, v) satisfies Fm,i,i+1 . From lemma 1, u ∈ Fm and v ∈ Fm , we
must prove that ϕτ 2i (u) · ϕτ 2i+1 (v) = 0. By hypothesis τji uj ∨ τji+1 vj = 1
for all j = 0, ..., m, then τji uj ∧ τji+1 v j = 0 for all j = 0, ..., m, therefore
ϕτ 2i (u) · ϕτ 2i+1 (v) = 0.
ξi ξ i+1
If u ∈ Fm and v ∈ Fm , from lemma 1, u satisfies Ci and v satis-
fies Ci+1 . Now, if ϕτ 2i (u) · ϕτ 2i+1 (v) = 0, then τji uj · τji+1 v j = 0 for all
j = 0, ..., m, hence τji ui ∨ τji+1 vj = 1 for all j = 0, ..., m. Therefore (u, v)
9
satisfies the row-formula Rj (equation (6)) for j = 0, ..., m. ¤
Remark 2. From previous lemma we have 1t Ti 1 = #SAT (Fm,i,i+1 ),
where Ti is the transfer matrix of the column i to the column i + 1 of Gn,m
(the constrained graph of Fn,m ).
Finally, we prove the theorem 1.
Proof (Theorem 1). From equation (9), it is clear that the vector
(u0 , ..., un ) ∈ {0, 1}(n+1)(m+1) satisfies the formula Fn,m iff (ui , ui+1 ) sat-
ξi ξ i+1
isfies Fm,i,i+1 for i = 0, ..., n − 1. By lemma 2, (ūi , ūi+1 ) ∈ Fm × Fm and
ϕτ 2i (u)·ϕτ 2i+1 (v) = 0 for i = 0, ..., n−1. Let aili+1 li be the entry of the trans-
ξ i+1ξ i
fer matrix Ti in the position (ūi+1 , ūi ) ∈ Fm × Fm . Then, by definition of
Ti and previous analysis, (u0 , ..., un ) ∈ {0, 1}(n+1)(m+1) satisfies the formula
ξ0 ξn
Fn,m iff (ū0 , ..., ūn ) ∈ Fm × · · · × Fm and an−1 0
ln ln−1 · · · al1 l0 = 1. Therefore
ξ 0ξ n
#SAT (Fn,m ) is the cardinality of the set {(ū0 , · · · , ūn ) ∈ Fm × · · · × Fm :
n−1 0
aln ln−1 · · · al1 l0 = 1}.
Taking into account all the terms an−1 0
ln ln−1 · · · al1 l0 = 0, we obtain
P n−1 1 0 t
#SAT (Fn,m ) = (l0 ,...,ln )∈I0 ×···×In aln ln−1 · · · al2 l1 · al1 l0 = 1 Tn−1 · · · T0 1,
ξ k
where Ik = {0, ..., rk }, rk =| Fm | for k = 0, ..., n.¤
Remark 3. Note that T = (Tn−1 Tn−2 . . . T0 ) = (αi,j )rn ×r0 is a rn × r0 -
ξ0
matrix, where αi,j is the number of models of Fn,m with ūi ∈ Fm and
ξn
ūj ∈ Fm fixed.
4 Counting Models on Grid-Cylinders and Grid-
Tori
In this section, we consider grid-cylinder or a grid-tori formulas. We are
interested in counting models for formulas with these classes of grid topolo-
gies. For this objective, we introduce the Hadamard product ”¦”, which is
defined for k × l matrices as follows. Let A = (ai,j )k×l and B = (bi,j )k×l be
k × l matrices. The k × l matrix A ¦ B = (ai,j bi,j ) is the Hadamard product.
Notice that a grid-cylinder C(n, m) can be seen as a grid Gn,m = (V (n, m),
E(n, m)) with edges from the column 0 to the column n (row 0 to the row
m) of Gn,m . Then the transfer matrix Tn of the column 0 to the column n
(row 0 to the row m) has sense.
Theorem 2. Let F be a grid-cylinder formula of size m × n with graph
C(n, m) = (V (n, m), EC(n, m)), EC = E ∪ E1 . Then #SAT (F ) = 1t Tn ¦
10
(Tn−1 Tn−2 . . . T0 )1, where Tk is the transfer matrix of the two consecutive
columns: k and k + 1 of Gn,m , k = 0, ..., n − 1 and Tn is the transfer matrix
of the columns 0 and n of Gn,m .
Clearly the previous theorem, also is true for EC = E∪E2 (interchanging
n by m and m by n). In the following example is illustrated.
Example 2. Let F = (x0 ∨ y0 ) ∧ (¬y0 ∨ ¬z0 ) ∧ (z0 ∨ z1 ) ∧ (z1 ∨ z2 ) ∧ (z2 ∨
y2 ) ∧ (y2 ∨ x2 ) ∧ (x2 ∨ x1 ) ∧ (¬x1 ∨ x0 ) ∧ (x1 ∨ y1 ) ∧ (¬y1 ∨ z1 ) ∧ (¬y1 ∨ ¬y0 ) ∧
(y1 ∨ y2 ), (x0 , z0 ), (¬x1 , z1 ), (¬x2 , ¬z2 )) (see figure 5).
xk k+1
+ + 0 x
0
+ + - -
x0 y0 z0 k+1
xk x1 k+1
+ - + 1 x
- + m
- - +
k
+ + - + x
x1 y1 z1 2
+ + +
-
- + +
+
x2 y2 z2 k
x
+ + + + m
Fig. 5: Grid-Cylinder C(2, 2) Fig. 6: Consecutive Cycles
We have that the matrix T1 T0 is given in example 1. The transfer matrix
T2 of columns 0 and 2 is computed as follows.
The strings of signs for edges from the column 0 to column 2 are given by:
s00 s01 s02 = + ∓ +, s20 s21 s22 = + + +, τ00 τ10 τ20 = + − − and τ02 τ12 τ22 = + + −, then
F2+∓+ = {u1 , · · · , u4 } and F2+++ = {v1 , v2 , v3 , v4 , v5 }, where u1 = (0, 0, 0),
u2 = (0, 1, 0), u3 = (0, 0, 1), u4 = (1, 1, 0), v1 = (0, 0, 0), v2 = (1, 0, 0), v3 =
(0, 1, 0), v4 = (0, 0, 1) and v5 = (1, 0, 1). The transfer matrix T2 = (aij )5×4 ,
is a 5 × 4 matrix given by aij = 1 if ϕ++− (vi ) · ϕ+−− (uj ) = 0 and aij = 0
otherwise (1 ≤ i ≤ 5 and 1 ≤ j ≤ 4). Then
0 0 1 0 3 2 2 0 0 0 2 0
0 0 1 0 4 2 3 0 0 0 3 0
T2 ¦ (T1 T0 ) =
0 0 0 0
¦ 1 0 1 0
= 0 0 0 0
1 1 1 1 2 1 2 0 2 1 2 0
1 1 1 0 3 1 3 0 3 1 3 0
Therefore #SAT (F ) = 17.
Proof (Theorem 2). Let F be a grid-cylinder formula of size m×n. We
have that F can beVexpressed as F = Fn,m ∧Rn , where Fn,m is given by equa-
tion (4) and Rn = m 2n 0 2n+1 n
j=0 (τj xj ∨τj xj ), that is, the graph of F is the graph
o Gn,m (the constrained graph of Fn,m ) adding new labelled edges (with signs
τj2n and τj2n+1 ) from the column 0 to column n of Gn,m . Let Tn = (βij )rn ×r0
be the transfer matrix of the column 0 to column n of Gn,m following the arcs
given by Rn . From remark 3, T = (Tn−1 Tn−2 . . . T0 ) = (αij )rn ×r0 , where αi,j
11
ξ0 ξn
is the number of satisfying assignments of Fn,m with ūi ∈ Fm and ūj ∈ Fm
fixed. Also, the formula Rn is satisfied by ui and uj iff βij = 1. Therefore,
ξ0 ξn
there are βij αij satisfying assignments of F with ūi ∈ Fm and ūj ∈ Fm
fixed. We observe that, the product βij αij is the entry ai,j of the Hadamard
product Tn ¦ T .¤
4.1 Transfer Matrix for Cycles
We can adapt our extension for computing the transfer matrix between two
consecutive simple cycles instead of two consecutive columns as follows.
Let Fm be the set of all (m + 1)-vectors v of 00 s and 10 s (as in section
3), and let Cm ⊂ Fm be the set of all (m + 1)-vectors v of 00 s and 10 s,
such that v does not have two consecutive 10 s and does not have 10 s in
the first and last positions. Given s = s0 s1 . . . sm a string in Ŝ, we define
Fms = {e ∈ F
m : ϕs (e) ∈ Cm+` }, ` =| {s ∈ {s0 , s1 , . . . , sm } : s ∈ S̄} |.
Assume that xk0 , . . . , xkm and xk+1 k+1
0 , . . . , xm are the nodes of the k − th and
(k + 1) − th cycles respectively of Cn,m , 0 ≤ k < n.
For j = k, k + 1, let sj = sj0 sj1 · · · sjm and τ j = τ0j τ1j · · · τm
j
, where sji =
sgn(xji ) and τij = sgnk (xji ). We define a matrix Tk = Tm,k , the transfer
matrix from cycle k to the cycle k + 1 as follows. Tk is an | Fm sk+1 | × | F sk |
m
matrix of 00 s and 10 s whose rows and columns are indexed by vectors of
Fmsk+1 × F sk . The entry of T in position (u, v) is 1 if the vectors ϕ (u)
m k τk
and ϕτ k+1 (v) are orthogonal, and is 0 otherwise (see figure 6).
Example 3. We compute the transfer matrices: T0 from cycle x0 y0 z0 to
x1 y1 z1 and T1 from cycle x1 y1 z1 to x2 y2 z2 for F as in example 2 (see figure
5). We have s00 s01 s02 = + ± ∓, s10 s11 s12 = ∓ ± + and s20 s21 s22 = ∓ + ±. On the
other hand, τ 0 = τ00 τ10 τ20 = +−+, τ 1 = τ01 τ11 τ21 = −−+, and τ 2 = τ02 τ12 τ22 =
τ 3 = τ03 τ13 τ23 = + + +. Then F2+±∓ = {u1 , u2 , u3 }, F2∓±+ = {v1 , v2 , v3 } and
F2∓±+ = {w1 , w2 , w3 }, where u1 = (0, 1, 0), u2 = (0, 0, 1), u3 = (0, 1, 1),
v1 = (0, 0, 0), v2 = (1, 0, 0), v3 = (0, 1, 0), w1 = (1, 0, 0), w2 = (0, 0, 1) and
w3 = (1, 0, 1). Computing ϕτ 2k (u) · ϕτ 2k+1 (v) for k = 0, 1 and following the
definition of transfer matrix, we have that T0 and T1 are 3×3 matrices given
by
1 0 1 1 0 1
T0 = 1 0 1 , T1 = 1 1 1 .
1 1 1 1 0 1
Remark 4. For F from example 2,
2 1 2
1T1 T0 1 = 1 3 1 3 1 = 17 = #SAT (F ).
2 1 2
12
The following theorem can also be used for computing #SAT (F ) for F ,
a grid-cylinder.
Theorem 3. Let F be a grid-cylinder of size m × n with graph C(n, m),
then #SAT (F ) = 1t Tn−1 . . . T0 1, where Tk is the transfer matrix of two
consecutive cycles: k and k + 1 of C(n, m), for k = 0, ..., n − 1.
Proof. The proof is similar to the proof of theorem 1, taking Fm , Cm ,
Fms and the transfer matrix for cycles as in section 4.1. We observe that,
in this case the column formulas Ci given by equation (5) are simple cycles.¤
Using theorem 3 and Hadamard product we can compute #SAT (F ) for
F , a grid-tori. The following theorem shows us how to proceed.
Theorem 4. Let F be a grid-tori of size m × n with graph T (n, m) =
(V (n, m), E 0 (n, m)), E 0 = E1 ∪E2 . Then #SAT (F ) = Tn ¦(Tn−1 Tn−2 . . . T0 ),
where Tk is the transfer matrix of the two consecutive cycles of T (n, m): k
and k + 1 of Gn,m , k = 0, ..., n − 1 and Tn is the transfer matrix of the cycle
0 and n.
Example 4. Let F1 = F ∪ {(x0 ∨ x2 ), (¬y0 , y2 ), (¬z0 , ¬z2 )}, where F is like
in example 2 (see figure 7).
+
+ + y0 - - z0
+ x0
- - +
+ -
- + +
- -
+ + - +
x1 y1 z1
+ + - +
-
+ + +
+ + -
x2 y2 z2
+ + + +
Fig. 7: Grid-Tori of example 4
We compute the transfer matrix T2 from the cycle x0 y0 z0 to the cycle
x2 y2 z2 as follows. We have F2+±∓ = {u1 , u2 , u3 } and F2∓±+ = {w1 , w2 , w3 },
where the vectors u0i s and w0j s are as the example 3, only that now τ 0 =
τ00 τ10 τ20 = + − − and τ 3 = τ03 τ13 τ23 = + + −. The transfer matrix T2 is
obtained by the evaluation of ϕτ 3 (wi ) · ϕτ 0 (uj ) for 1 ≤ i ≤ 3 and 1 ≤ j ≤ 3.
Then
0 1 1
T2 = 1 1 1
1 1 1
In example 2, T0 , T1 and T1 T0 are computed, therefore
0 1 1 2 1 2 0 1 2
T2 ¦ (T1 T0 ) = 1 1 1 ¦ 3 1 3 = 3 1 3
1 1 1 2 1 2 2 1 2
and #SAT (F1 ) = 1T2 ¦ (T1 T0 )1 = 15.
13
Proof (Theorem 4). Using the theorem 3, the proof is similar to
the proof of theorem 2 taking Fn,m as a grid cylinder formula and Rn =
C0 ∧ Cn ∧ E, where C0 and Cn corresponding to the first cycle and n-th
cycle of C(n, m) respectively (C(n, m) is the grid cylinder associated to
Fn,m ). The formula E is formed by new clauses corresponding to edges
from the vertices of the first cycle to the vertices of n-th cycle of C(n, m).
¤
5 Conclusion
We have presented an extension of the transfer matrix method that allows
to consider signed edges on grid graphs, grid-cylinders and grid-tori. We
argued about the advantage of this extension in the problem of counting
assignments of Boolean formulas in 2-CN F .
We have designed a procedure for computing #2SAT(F ) where F is a
grid, grid-cylinder or grid-tori Boolean formula, based on the sum of all
entries of the product matrix of the transfer matrix of each two consecutive
columns for the case of a grid. In a grid cylinder we have two result for
computing #2SAT(F ) one uses the sum of the entries of the Hadamard
product between the transfer matrix of the first column (row) and the top
column (row) with the product matrix of the transfer matrix of each two
consecutive columns (row). The second result uses the sum of all entries of
the product matrix of the transfer matrix of each two consecutive cycles.
Finally, if F is a grid tori, we use the sum of the entries of the Hadamard
product between the transfer matrix of the first cycle and the top cycle of
tori with the product matrix of the transfer matrix of each two consecutive
cycles of the tori.
A work in progress is the detailed determination of the complexity of
the proposed extension. However, based on previous works in the transfer
matrix method and our preliminary experiments, the complexity remains
polynomial as long as the starting grid graphs are of fixed height, we consider
the complexity with a fixed-parameter.
References
[1] R. Baxter. Planar lattice gases with nearest neighbour exclusion. An-
nals of Combinatorics, 3:191–203, 1999.
[2] N. J. Calkin and H. S. Wilf. The number of independent sets in a grid
graph. SIAM J. Discrete Math., 11(1):54–60, 1998.
[3] V. Dahllöf, P. Jonsson, and M. Wahlström. Counting satisfying assign-
ments in 2-sat and 3-sat. In COCOON, pages 535–543, 2002.
14
[4] V. Dahllöf, P. Jonsson, and M. Wahlström. Counting models for 2sat
and 3sat formulae. Theor. Comput. Sci., 332(1-3):265–291, 2005.
[5] J. Davies and F. Bacchus. Using more reasoning to improve #sat solv-
ing. In AAAI, pages 185–190, 2007.
[6] O. Dubois. Counting the number of solutions for instances of satisfia-
bility. Theor. Comput. Sci., 81(1):49–64, 1991.
[7] R. Euler. The fibonacci number of a grid graph and a new class of
integer sequences. JIS Journal of Integer Sequences, 8(2):1–16, 2005.
[8] M. Fürer and S. P. Kasiviswanathan. Algorithms for counting 2-sat
solutions and colorings with applications. In AAIM, pages 47–57, 2007.
[9] M. J. Golin, Y.-C. Leung, Y. Wang, and X. Yong. Counting structures
in grid graphs, cylinders and tori using transfer matrices: Survey and
new results. In ALENEX/ANALCO, pages 250–258, 2005.
[10] P. T. Littman M. L. and I. R. On the complexity of counting satisfying
assignments. Notes of LICS, Workshop on Satisfiability, 2001.
[11] D. Roth. On the hardness of approximate reasoning. Artif. Intell.,
82(1-2):273–302, 1996.
[12] R. M. Roth, P. H. Siegel, and J. K. Wolf. Efficient coding schemes
for the hard-square model. IEEE Transactions on Information Theory,
47(3):1166–1176, 2001.
[13] B. Russ. Randomized Algorithms: Approximation, Generation, and
Counting. Distinguished dissertations Springer, 2001.
[14] S. P. Vadhan. The complexity of counting in sparse, regular, and planar
graphs. SIAM J. Comput., 31(2):398–427, 2001.
[15] M. Wahlström. A tighter bound for counting max-weight solutions to
2sat instances. In IWPEC, pages 202–213, 2008.
[16] W. Zhang. Number of models and satisfiability of sets of clauses. Theor.
Comput. Sci., 155(1):277–288, 1996.
15