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. 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
Introduction The transfer matrix method is a general technique which has been used to ¯nd 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 modi¯cations, to count structures in ¯xed 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 constant" de¯ned as limm;n!1 I(Gm;n)1=m¢n [1]. Applications also include for instance tiling and e±cient 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 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 models 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 #Pcomplete problem.
There is a signi¯cant 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Äof et al. [4], FuÄrer [8] and WahlstroÄn [15]. WahlstroÄn uses a re¯nement 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 ¯xed height is polynomial. 2
Preliminaries For k and l integers such that k < l, we denote the set fk; k + 1; :::; lg by [k; l]. The Euclidean distance between points u and v in Euclidean 2-space 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) = f(u; v) 2 V 2(n; m) : d(u; v) = 1g. Let E1(n; m) = ( 0
f g £ [0; m]) £ (fng £ [0; m]) and E2(n; m) = ([0; n] £ f0g) £ ([0; n] £ fmg) 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) [ E0(n; m), where E0(n; m) 2 fE1(n; m); E2(n; m)g (see ¯gures 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 ¯gure 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 00s and 10s without two consecutive 10s (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 00s and 10s 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 Tmn , i.e., I(Gn;m) = 1tTmn 1, where 1 is the (F ibm+2)vector whose entries are all 10s. For example, if m = 2 and n = 3 we have that C2 = f(0; 0; 0); (1; 0; 0); (0; 1; 0); (0; 0; 1); (1; 0; 1)g, can associate a monotone 2-CN F formula FG with variables V , and where FG = V(u;v)2E(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 2 E.
We denote S = f+; ¡g, S¹ = f§; ¨g and S^ = S [S¹. Let Gn;m = (V; E; Ã) be a grid graph with labelled edges on S2. Let x and y be nodes in V . If e = fx; yg is an edge and Ã(e) = (s; s0), then s (s0) is called the adjacent sign to x (y), see ¯gure 2.
j=j’
x s s’ y a) i i’ b) i=i’ j j’ x y s s’ s’o so x a) s’o so
x s1 b) s’1 Let e = ((i; j); (i0; j0)) be an edge of a grid graph Gn;m, if i = i0 and j 6= j0, e is called a column-edge (see ¯gure 2b), and if i 6= i0 and j = j0, e is called a row-edge (see ¯gure 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 de¯ne sgnc(x) = s0, where s0 is the adjacent sign to x (see ¯gure 3a).
If x has two incident column-edges e0 and e1 with labels (s0; s00) and (s1; s01) respectively ( see ¯gure 3b ), we de¯ne sgncc : V ! S^ as follows 8+ if (s0; s1) = (+; +); > sgncc(x) = <>¡ if (s0; s1) = (¡; ¡); >§ if (s0; s1) = (+; ¡); > :¨ if (s0; s1) = (¡; +):
In general, we can consider the function sgn : V ! S^ as sgn(x) = sgnc(x) if x has one incident column-edge or sgn(x) = sgncc(x) if x has two incident column-edges.
x0 + + y0 - - z0 + - +
- - + + - x1 + + y1 z1 + + + + + + x2 y2 z2
+ + + + a) x0 + + y0 y0 - - z0 -+x1 + + -- y1 -- y1 - + z1++ ++ ++ ++ ++ x2 + + y2 y2 + + z2
G2,0,1 G 2,1,2 b)
Given Gn;m = (V; E; Ã) a grid graph with labelled edges on S2, 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 = f(u; v) 2 Vk2 : d(u; v) = 1g and Ãk = à jEk the restriction of à to Ek.
Notice that Gm;k;k+1 speci¯es 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 de¯ne 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 ¯gure 4a. Then sgn(x) = +, for x 2 fx0; x2; y2; z0; z1; z2g, sgn(y0) = ¡ and sgn(y1) = sgn(x1) = ¨. In G2;0;1, we have sgn0(x) = + for all x 2 V0. In G2;1;2, sgn1(x) = + for x 2 fy2; z1; z2g and sgn1(x) = ¡ for x 2 fy0; y1; z0g (see ¯gure 4b).
Given a vector v = (v0; v1; : : : ; vm) 2 f0; 1gm+1 and a string s = s0 : : : sm of signs in S^, for m ¸ 0, we de¯ne the family of operators 's : f0; 1gm+1 ! f0; 1gp; (m + 1 · p · 2m + 2) as 's(v) = (s0v0; : : : ; smvm), where sjvj = ><>8 vv¹jj iiff ssjj == +¡;; >(vj; v¹j) if sj = §; >:(v¹j; vj) if sj = ¨: for j = 0; : : : ; m. For v 2 f0; 1g, 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): In general, we can omit the internal parenthesis given the associative property 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 00s and 10s, and let Cm ½ Fm be the set of all (m + 1)-vectors v of 00s and 10s, such that v does not have two consecutive 10s. The cardinality of Cm (denoted by jCmj) is F ibm+2 (the (m + 2)-th Fibonacci number), while jFmj = 2m+1. Given s = s0s1 ¢ ¢ ¢ sm a string of signs in S^, we de¯ne F ms = fe 2 Fm : 's(e) 2 Cm+`g, where ` = jfs 2 fs0; :::; smg : s 2 S¹gj.
Remark 1. Notice that Cm µ Fm and that the equality holds when si = + for all i = 0; :::; m. Furthermore, if there exists i 2 f0; :::; mg such that si 2 S^, then jFmj < jCmj.
s
Let Gn;m be a grid graph of size m £ n with labelled edges on the set S2, we assume that x0k; : : : ; xkm and xk+1; : : : ; xkm+1 are the nodes of the k ¡ th 0 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 = sj0sj1 ¢ ¢ ¢ sjm and ¿ j = ¿0 ¿1 ¢ ¢ ¢ ¿ mj be two string of j j signs, such that sij = sgn(xij ) and ¿ij = sgnk(xij ) for i = 0; ¢ ¢ ¢ ; m. Following the idea proposed in [2], we de¯ne a matrix Tk = Tm;k, the transfer matrix sk+1 frokm column k to the column k + 1 of Gn;m as follows. Tk is an j Fm j £ j F ms j matrix of 00s and 10s whose rows and columns are indexed by vectors (v; u) of F msk+1 £ F msk . The entry of Tk in position (v; u) is 1 if the vectors '¿k (u) and '¿k+1 (v) are orthogonal, and is 0 otherwise.
Notice that if sij 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 illustrated in ¯gure 4. For G2;0;1, we have that s0 = + ¨ +, s1 = ¡ ¨ + and ¿ 0 = ¿ 1 = + + +, then F2+¨+ = fu1; ¢ ¢ ¢ ; u4g and F2¡¨+ = fv1; v2; v3; v4g, 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
0 1 1 1 0 1
T0 = BB@ 11 01 10 00 CCA
1 0 1 0
(
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
In the case, not necessarily monotone, of a formula F having a constrained grid graph Gn;m with labelled edges on S2 and transfer matrices T0; : : : ; Tn¡1, we conclude that the sum of all entries of the product matrix 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 S2, 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 observations.
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 (
If Fn;m denotes a grid formula having as constrained graph a grid Gn;m, for n > 0, we can write where
i ´q 2 S for q = 0; :::; 2m ¡ 1,
Ci = m¡1 ^ (´2ikxik _ ´2k+1xk+1)
i i k=0
m R` = ^ (¿j2`xj` _ ¿j2`+1x`+1)
j
j=0
¿jr 2 S for j = 0; :::; m, r 2 f2`; 2` + 1g. Here, the formulas Ci and R` are
called column-f ormula and row-f ormula respectively.
(
Fm;i;i+1 = Ci ^ Ci+1 ^ Ri
Fn;m = n¡1 ^ Fm;i;i+1 i=0 Notice that for n; m > 0 For i = 0; :::; n ¡ 1, we de¯ne
If Á : fxi0; : : : ; ximg ! f0; 1g 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 f0; 1gm+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, »mi = ´2im¡1 and »qi = sgn(xiq) for q = 1; :::; m ¡ 1. Also, notice that for v 2 f0; 1g
»qi v = ½´( ´2iq2i¡q¡1v1v=;´´2iq2ivqv) if ´o2itqh¡e1r=wi´s2ieq:;
To prove the theorem 1, ¯rst, we characterize the partial assignments of
the variables of Fn;m such that satis¯es each column-formula Ci (lemma 1).
Second, we characterize the pairs of assignments that satis¯es the formula
(
Next, for simplicity we omit the superindex i of vji ; xij ; ´ji ; ¿ji and »ji .
Lemma 1. The vector u 2 f0; 1gm+1 satis¯es the formula (
Proof. By de¯nition, it is clear that '»0;:::;»m(u) 2 Fm+k. Now, if
u = (u0; :::; um) satis¯es the formula (
Suppose that '»0;:::;»m(u) 2 Cm+k, for ` = 0; :::; m then (»`u`; »`+1u`+1)
does not have two consecutive 10s. The vector u satis¯es the
columnformula Ci (equation (
For all i = 0; :::; m, we denote the strings »0i; :::; »mi and ¿0i; :::; ¿ mi by »i and ¿ i respectively. »i Lemma 2. The pair (u; v) 2 f0; 1g2m+2 satis¯es Fm;i;i+1 i® (u; v) 2 Fm £ »i+1 Fm and '¿2i(u) ¢ '¿2i+1(v) = 0.
Proof. Suppose that u = (u0; :::; um) and v = (v0; :::; vm) are such that (u; v) satis¯es Fm;i;i+1. From lemma 1, u 2 F m»i and v 2 F m»i+1, we must prove that '¿2i(u) ¢ '¿2i+1(v) = 0. By hypothesis ¿jiuj _ ¿ji+1vj = 1 for all j = 0; :::; m, then ¿jiuj ^ ¿ji+1vj = 0 for all j = 0; :::; m, therefore '¿2i(u) ¢ '¿2i+1(v) = 0.
»i »i+1, from lemma 1, u satis¯es Ci and v
satisIf u 2 Fm and v 2 Fm
¯es Ci+1. Now, if '¿2i(u) ¢ '¿2i+1(v) = 0, then ¿jiuj ¢ ¿ji+1vj = 0 for all
j = 0; :::; m, hence ¿jiui _ ¿ji+1vj = 1 for all j = 0; :::; m. Therefore (u; v)
satis¯es the row-formula Rj (equation (
Remark 2. From previous lemma we have 1tTi1 = #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).
Proof (Theorem 1). From equation (
Taking into account all the terms alnn¡ln1¡1 ¢ ¢ ¢ al1l0 = 0, we obtain 0 #SAT (Fn;m) = P(l0;:::;ln)2I0£¢¢¢£In alnn¡ln1¡1 ¢ ¢ ¢ al12l1 ¢ al01l0 = 1tTn¡1 ¢ ¢ ¢ T01, »k where Ik = f0; :::; rkg, rk =j Fm j for k = 0; :::; n.¤
Remark 3. Note that T = (Tn¡1Tn¡2 : : : T0) = (®i;j )rn£r0 is a rn £ r0matrix, where ®i;j is the number of models of Fn;m with u¹i 2 F m»0 and u¹j 2 F m»n ¯xed. 4
Counting Models on Grid-Cylinders and GridTori 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 topologies. For this objective, we introduce the Hadamard product "¦", which is de¯ned 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 ) = 1tTn ¦ (Tn¡1Tn¡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 ¯gure 5).
+ + x0 + + y0 - - z0 -+ - -- + ++ x1 + + y1 - + z1 ++ - ++ - ++ x2 y2 z2 Fig. 6: Consecutive Cycles
We have that the matrix T1T0 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: s00s01s02 = + ¨ +, s20s21s22 = + + +, ¿00¿10¿20 = + ¡ ¡ and ¿02¿12¿22 = + + ¡, then F2+¨+ = fu1; ¢ ¢ ¢ ; u4g and F2+++ = fv1; v2; v3; v4; v5g, 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 Therefore #SAT (F ) = 17.
Proof (Theorem 2). Let F be a grid-cylinder formula of size m£n. We
have that F can be expressed as F = Fn;m ^Rn, where Fn;m is given by
equation (
j=0(¿j2nxj0_¿j2n+1xjn), 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¡1Tn¡2 : : : T0) = (®ij )rn£r0 , where ®i;j is the number of satisfying assignments of Fn;m with u¹i 2 F m»0 and u¹j 2 F m»n ¯xed. Also, the formula Rn is satis¯ed by ui and uj i® ¯ij = 1. Therefore, there are ¯ij ®ij satisfying assignments of F with u¹i 2 F m»0 and u¹j 2 F m»n ¯xed. 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 00s and 10s (as in section 3), and let Cm ½ Fm be the set of all (m + 1)-vectors v of 00s and 10s, such that v does not have two consecutive 10s and does not have 10s in the ¯rst and last positions. Given s = s0s1 : : : sm a string in S^, we de¯ne F ms = fe 2 Fm : 's(e) 2 Cm+`g, ` =j fs 2 fs0; s1; : : : ; smg : s 2 S¹g j. Assume that x0k; : : : ; xkm and x0k+1; : : : ; xkm+1 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 = s0s1 ¢ ¢ ¢ sjm and ¿ j = ¿0 ¿1 ¢ ¢ ¢ ¿m, where sij = j j j j j sgn(xij ) and ¿ij = sgnk(xij ). We de¯ne a matrix Tk = Tm;k, the transfer matrix from cycle k to the cycle k + 1 as follows. Tk is an j F msk+1 j £ j F msk j matrix of 00s and 10s whose rows and columns are indexed by vectors of F msk+1 £ F msk . The entry of Tk in position (u; v) is 1 if the vectors '¿k (u) and '¿k+1 (v) are orthogonal, and is 0 otherwise (see ¯gure 6). Example 3. We compute the transfer matrices: T0 from cycle x0y0z0 to x1y1z1 and T1 from cycle x1y1z1 to x2y2z2 for F as in example 2 (see ¯gure 5). We have s00s01s02 = + § ¨, s10s11s12 = ¨ § + and s20s21s22 = ¨ + §. On the other hand, ¿ 0 = ¿00¿10¿20 = +¡+, ¿ 1 = ¿01¿11¿21 = ¡¡+, and ¿ 2 = ¿02¿12¿22 = ¿ 3 = ¿03¿13¿23 = + + +. Then F2+§¨ = fu1; u2; u3g, F2¨§+ = fv1; v2; v3g and F2¨§+ = fw1; w2; w3g, 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 de¯nition of transfer matrix, we have that T0 and T1 are 3£3 matrices given by
0 1 0 1 1 0 1 0 1 1 T0 = @ 1 0 1 A ; T1 = @ 1 1 1 A : 1 1 1 1 0 1 0 2 1 2 1 1T1T01 = 1 @ 3 1 3 A 1 = 17 = #SAT (F ): 2 1 2
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 ) = 1tTn¡1 : : : T01, 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,
F ms and the transfer matrix for cycles as in section 4.1. We observe that,
in this case the column formulas Ci given by equation (
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); E0(n; m)), E0 = E1[E2. Then #SAT (F ) = Tn¦(Tn¡1Tn¡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 [ f(x0 _ x2); (:y0; y2); (:z0; :z2)g, where F is like in example 2 (see ¯gure 7).
+ + x0 + + y0 - -- z0 -+ - - -- + ++ x1 + + y1 - + z1 + ++ - ++ -- ++ x2 + ++ y2 + + z2
0 0 1 1 1 T2 = @ 1 1 1 A
1 1 1
Fig. 7: Grid-Tori of example 4
We compute the transfer matrix T2 from the cycle x0y0z0 to the cycle x2y2z2 as follows. We have F2+§¨ = fu1; u2; u3g and F2¨§+ = fw1; w2; w3g, where the vectors u0 s and w0 s are as the example 3, only that now ¿ 0 = i j ¿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
In example 2, T0, T1 and T1T0 are computed, therefore
0 0 1 1 1 0 2 1 2 1 0 0 1 2 1 T2 ¦ (T1T0) = @ 1 1 1 A ¦ @ 3 1 3 A = @ 3 1 3 A
1 1 1 2 1 2 2 1 2 and #SAT (F1) = 1T2 ¦ (T1T0)1 = 15:
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 ¯rst 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 ¯rst cycle to the vertices of n-th cycle of C(n; m). ¤
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 ¯rst 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 ¯rst 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 ¯xed height, we consider the complexity with a ¯xed-parameter.