A method for counting models on grid Boolean formulas 1

Abstract

We present a novel algorithm based on combinatorial operations on lists for computing the number of models on two conjunctive normal form Boolean formulas whose restricted graph is represented by a grid graph G_m,n. We show that our algorithm is correct and its time complexity is $O (\sqrt{t} \cdot 1 . 618^{\sqrt{t} + 2} + t \cdot 1 . 618^{2 \sqrt{t} + 4})$ , where t = n · m is the total number of vertices in the graph.

For this class of formulas, we show that our proposal improves the asymptotic behavior of the time-complexity with respect of the current leader algorithm for counting models on two conjunctive form formulas of this kind.

Keywords

#SAT #2SAT models of boolean formulas combinatorial algorithms complexity theory

1 Introduction

The decision problem SAT (F), where F is a Boolean formula, consists in determining whether F has a model, that is, an assignment to the variables of F such that when evaluated with respect to classical Boolean logic it returns true as a result. If F is in two Conjunctive Normal Form (2-CNF) then SAT (F) can be solved in polynomial time, however if F is in k-CNF, k > 2, then SAT (F) is an NP-Complete problem. Its counting version # k-SAT(F) is a classic #P-Complete problem even when F is in 2-CNF, the latter denoted as #2SAT [1].

Counting combinatorial objects is a challenging and relevant area of research in mathematics, computer sciences and physics. Counting problems, being mathematically relevant by themselves, are closely related to practical problems. Several relevant counting problems are hard time complexity problems. For example, #k-SAT (the problem of counting models for a Boolean formula) is of special concern to artificial intelligence (AI), and it has a direct relationship to automated theorem proving, as well as to approximate reasoning [2 –4].

# k-SAT is related to other counting problems, e.g. in approximate reasoning, in the cases of the generation of explanation to propositional queries, repairing inconsistent databases, estimating the degree of belief in propositional theories, in a truth maintenance systems, in Bayesian inference [2 , 6]. The previous problems come from several AI applications such as expert systems, planning, approximate reasoning, etc.

Although the #2SAT problem is #P-Complete, there are instances that can be solved in polynomial time [7, 8]. For example, if the graph representation of the formula is acyclic, then the number of models can be computed in lineal time [7]. Currently, the algorithms that are used to solve the problem for any formula F in 2-CNF, decompose F into sub-formulas until there are base cases in which it can be counted efficiently.

The algorithm with the best time complexity so far was developed by Wahlström [9]. The Wahlström’s algorithm has an upper bound for its time-complexity of order O (1 .2377ⁿ), where n represents the number of variables in the formula. The Wahlström’s algorithm uses the number of times a variable appears in the formula (being it the variable or its negation) as the criterion for choosing it. The two criteria for stopping the algorithm are when F =∅ or when ∅ ∈ F.

In this paper we present an algorithm based on combinatorial operations on lists to compute #2SAT models on the so called grid formulas. We show that for this particular type of formulas our algorithm improves the asymptotic behavior of the time-complexity of the leader algorithm by Wahlström.

2 Preliminaries

2.1 Grid graphs

A grid graph of size m × n is a graph G_m,n with vertex set

V = {(i, j) :1 ≤ i ≤ m, 1 ≤ j ≤ n}

and edge set

E = {((j, i) , (j + 1, i)) ∣1 ≤ j < m, 1 ≤ i ≤ n} ∪ {((j, i) , (j, i + 1)) ∣1 ≤ j ≤ m, 1 ≤ i < n}

There is a large volume of literature devoted to count structures in a grid graph, e.g., spanning trees, Hamiltonian cycles, independent sets, acyclic orientations, k-coloring, and so on [10 –13]. For example, the study of the number of independent sets on grid structures is closely related to the ‘’hard-square model" used in statistical physics and, of particular interest is the so-called hard-square entropy constant [14]. Applications of the counting objects on grids also include for instance tiling and efficient coding schemes in data storage [15].

Euler [11] presents a method to calculate the Fibonacci number of a grid graph, calculating a new parameter b (m, n) using the transfer matrix method. Calkin [10] calculates the number of independent sets on grid graphs using the transfer matrix method. Guillen et al. [13] present an extension of the transfer matrix method to count the number of satisfying assignments of Boolean formulas in 2-CNF. Here, we begin considering the transfer matrix method in order to build a list operation method for counting objects on a grid structure and some of its structure variants.

2.2 Conjunctive Normal Form

Let X = {x₁, . . . , x_n} be a set of n Boolean variables (that is, they can only take two possible values 1 or 0). A literal is a variable x_i, denoted in this paper as $x_{i}^{1}$ or the denied variable ¬x_i denoted in this paper as $x_{i}^{0}$ . A clause is a disjunction of different literals. A Boolean formula F in conjunctive normal form (CNF) is a conjunction of clauses. We denote the cardinality of a set S by |S|.

Let V (Y) be the set of variables involved in the object Y, where Y can be a literal, a clause or a Boolean formula. For example, for the clause $c = {x_{1}^{1} \lor x_{2}^{0}}$ , v (c) = {x₁, x₂}. Meanwhile, Lit (Y) denotes the set of literals involved in the object Y. For example, if X = υ (F), then $Lit (F) = X \cup \bar{X} = {x_{1}^{1}, x_{1}^{0}, \dots, x_{n}^{1}, x_{n}^{0}}$ .

An assignment s in F is a Boolean function s : F → {0, 1}. s is defined as: $s (x^{0}) = 1 if s (x^{1}) = 0, otherwise s (x^{0}) = 0 .$

The assignment can be extended to conjunctions and disjunctions as follows:

s (x ∧ y) =1 if s (x) = s (y) =1, otherwise s (x ∧ y) =0

s (xlory) =0 if s (x) = s (y) =0, otherwise s (x ∨ y) =1

Let F be a Boolean formula in CNF, it is said that s satisfies F (denoted as s ⊨ F), if for each clause c in F, it holds s (c) =1. On the other hand, it is said that F is contradicted by s (s $| \neq$ F), if there is at least one clause c of F such that s (c) =0. A model of F is an assignment that satisfies F. s is a partial assignment for the formula F when s has determined a logical value only to variables of a proper subset of F.

Given a CNF F, the SAT problem consists of determining whether F has a model. The # k-SAT(F) problem consists of counting the number of models of F defined over υ (F). #2SAT denotes # k-SAT for formulas in 2-CNF.

2.3 The restricted graph of a 2-CNF

There are some graphical representations of a Conjunctive Normal Form, in this case the signed primary graph (restricted graph) [6] will be used.

Let F be a 2-CNF, its restricted graph is denoted by G_F = (V (F) , E (F)) where the vertices of the graph are the variables V (F) = v (F) and $E (F) = {{x_{i}^{ε}, x_{j}^{γ}} ∣ {x_{i}^{ε} \lor x_{j}^{γ}} \in F}$ , that is, for each clause ${x_{i}^{ε} \lor x_{j}^{γ}} \in F$ there is an edge ${x_{i}^{ε}, x_{j}^{γ}} \in E (F)$ . We say that a 2-CNF F is a path, a cycle, a tree, or a grid, if its restricted graph G_F represents a path, a cycle, a tree, or a grid, respectively.

For x ∈ V (F), δ (x) denotes its degree, that is the number of incident edges in x. Each edge $e = {x_{i}^{ε}, x_{j}^{γ}} \in E (F)$ has associated a pair (ε, γ), which represent whether the variables x_i or x_j appear negated or not. For example, the clause $(x_{1}^{0} \lor x_{2}^{1})$ has associated the pair (0,1) meaning that in the clause, x₁ appears negated and x₂ appears in positive way.

Let S = {+ , -} be a set of signs. A graph with edges labeled S is the pair (G, Ψ), where G = (V, E) is a restricted graph, and Ψ is a function with domain E and range S. Ψ (e) is called the label from the edge e ∈ E. Let G = (V, E, Ψ) be a restricted graph with labeled edges on S × S. Let x and y be two different vertices in V. If e = {x, y} is an edge and ψ (e) = (s, s′), then s (s′) is called the adjacent sign to x (y).

Notice that a restricted graph of a 2-CNF can be a multigraph, since two fixed variables can be involved in more than one clause of the formula, forming so parallel edges. Furthermore, a unitary clause defines a loop in the constraint graph.

Let ρ : 2 - CNF → G_F be the function whose domain is the space of non strict Boolean formulas in 2-CNF and codomain the set of multi-graphs. It is clear that ρ is a bijection. Furthermore, any 2-CNF formula has a unique signed restricted graph (up to isomorphism) associated via ρ and viceversa, any signed constraint graph G_F has a unique formula associated via ρ^-1.

2.4 Methods already reported to compute #2SAT

The basic idea considered in related papers to count models on a restricted graph G consists on computing a tuple (α_i, β_i) over each vertex x_i, where α_i represents the number of times that x_i appears positive in the models of G, and β_i the number of times x_i appears negative in the models of G. For example, a formula with a simple variable {x_i} has associated the tuple (1, 1) to the vertex x_i. Given an edge (clause) $e = {x_{i}^{ε_{i}}, x_{j}^{γ_{i}}}$ , if the counting begins at $x_{i}^{ε_{i}}$ , then the tuples (1, 1) and (2, 1) are associated to $x_{i}^{ε_{i}}$ and $x_{j}^{γ_{i}}$ , respectively. However, if the counting begins at $x_{j}^{γ_{i}}$ , then the tuples are associated inversely. The number of models results of the sum of the last two elements of the tuple.

There are reported methods to count models in some graphical representations of a 2-CNF formula F [5 , 16], here we state the method needed in the paper:

If the graph represents a path e.g a formula of the form $P_{n} = {{x_{1}^{ε_{1}}, x_{2}^{γ_{1}}}, {x_{2}^{ε_{2}}, x_{3}^{γ_{2}}}, \dots {x_{n - 1}^{ε_{n - 1}}, x_{n}^{γ_{n - 1}}}}$ of n vertices, the number of models is given by the sum of the elements of the pair (α_n, β_n). where (α₁, β₁) = (1, 1) and the tuple for the other vertices is computed according to recurrence 1. $(α_{i}, β_{i}) = {\begin{matrix} (α_{i - 1} + β_{i - 1}, α_{i - 1}) & if (ε_{i - 1}, γ_{i - 1}) = (1, 1) \\ ∥ (α_{i - 1}, α_{i - 1} + β_{i - 1}) & if (ε_{i - 1}, γ_{i - 1}) = (1, 0) \\ ∥ (α_{i - 1} + β_{i - 1}, β_{i - 1}) & if (ε_{i - 1}, γ_{i - 1}) = (0, 1) \\ ∥ (β_{i - 1}, α_{i - 1} + β_{i - 1}) & if (ε_{i - 1}, γ_{i - 1}) = (0, 0) \end{matrix}$ (1)

A known method for counting models on grid formulas comes from an adaptation of the Calkin transfer matrix method [10, 13]. We will present a novel method based on lists that provides a better asymptotic behaviour with respect to other algorithms for computing #2SAT on grid formulas.

3 Construction of the satisfiable assignments of a path formula

Let P_m be the restricted path graph of m vertices representing a 2-CNF F. A satisfiable set S_m over P_m is the set of assignments of F that satisfies the formula represented in the graph. The size of each element in S_m is m representing the assignment of each variable.

The satisfiable set can be divided on two subsets S_{p
_i} and S_{n
_i}, where S_{p
_i} represents the assignments where x_i appears positive, and S_{n
_i} the assignments where x_i appears negated.

The set S_m is inductively constructed where S_{p
₁} = {1} and S_{n
₁} = {0}, and the inductive step consists of a modified version of the equation 1: $(S_{p_{i}}, S_{n_{i}}) = {\begin{matrix} (S_{p_{i - 1}} 1 \cup S_{n_{i - 1}} 1, S_{p_{i - 1}} 0) \\ if (ε_{i - 1}, γ_{i - 1}) = (1, 1) . \\ ∥ (S_{p_{i - 1}} 1, S_{p_{i - 1}} 0 \cup S_{n_{i - 1}} 0) \\ if (ε_{i - 1}, γ_{i - 1}) = (1, 0) . \\ ∥ (S_{p_{i - 1}} 1 \cup S_{n_{i - 1}} 1, S_{n_{i - 1}} 0) \\ if (ε_{i - 1}, γ_{i - 1}) = (0, 1) . \\ ∥ (S_{n_{i - 1}} 1, S_{p_{i - 1}} 0 \cup S_{n_{i - 1}} 0) \\ if (ε_{i - 1}, γ_{i - 1}) = (0, 0) . \end{matrix}$ (2)

For example on the path formed by the edge {x₁, x₂}, signs (1, 1), and the initial sets S_{p
₁} = {1} and S_{n
₁} = {0}, which represents the initial partial assignments on x₁.

The operation S_{p
_i-1}1 represents the concatenation of the elements in S_{p
_i-1} with 1 at the end of the chain.

Then, for the edge {x₁, x₂}, with signs (1, 1), the calculation of the sets S_{p
₂} and S_{n
₂} is as follows:

(S_{p
₂}, S_{n
₂}) = (S_{p
₁}1 ∪ S_{n
₁}1, S_{p
₁}0) that is, S_{p
₂} = {11, 01} and S_{n
₂} = {10}.

Now we can calculate the satisfiable set as the union of both sets, S₂ = S_{p
₂} ∪ S_{n
₂} = {11, 01, 10}.

The calculation of the set S₅ associated to P₅ = {{x₁, x₂} , {x₂, x₃} , {x₃, x₄} , {x₄, x₅}}, with signs {(1, 1) , (1, 1) , (1, 1) , (1, 1)} can be done in a sequential way using the equation 1_sat_set, in the following way.

S₁={1,0}

S₂={01,10,11}

S₃={011,101,111,010,110}

S₄={0111,1011,1111,0101,1101,0110,1010,

1110}

S₅= {01111,10111,11111,01011,11011,01101,

10101,11101,01110,10110,11110,11010}

The size of the set S₅ is the number of models of the formula P₅. Each value represents an assignment to the variables that satisfies the formula. For example the element 10101 means that the assignment s (x₁) = s (x₃) = s (x₅) =1 and s (x₂) = s (x₄) =0 is a model of the formula P₅. The application of Equation 1_sat_set provides us an exponential-time procedure for enumerate all model of a path formula.

4 Counting models on grid formulas

We will consider the grid graph G_m,n as the union of n paths, each path with m vertices. The path $P_{m}^{i}$ (Fig. 1), 1 ≤ i ≤ n have a vertex set $V (P_{m}^{i}) = {(1, i), (2, i), \dots, (m, i)}$ and edge set $E (P_{m}^{i}) = {((j, i), (j + 1, i)) ∣ 1 \leq j < m}$ . The vertices of the grid graph $V (G_{m, n}) = \cup_{i = 1}^{n} V (P_{m}^{i})$ and the edges of the grid graph $E (G_{m, n}) = {((j, i), (j, i + 1)) ∣ 1 \leq i < n, 1 \leq j \leq m} \cup (\cup_{i = 1}^{n} E (P_{m}^{i}))$ .

4.1 List counting method

Let $S_{m}^{i}$ be the satisfiable set associated to the path graph $P_{m}^{i}$ . For each path $P_{m}^{i}$ , we build a list l_i, which has as many elements as the size of $S_{m}^{i}$ . Thus, we can reference l_i [j] as the j-satisfiable set entry of l_i and $S_{m}^{i} [j]$ as the index of l_i [j]. Initially the value of each $l_{i} [j] = 1, 1 \leq j \leq | S_{m}^{i} |$ . Fig. 2.

Fig. 1

Path identification over G_m,n.

Fig. 2

List l_i with initial values.

Lemma 1. Let $P_{m}^{i} = {{x_{1}^{s_{1}}, x_{2}^{s_{1}^{'}}}$ , ${x_{2}^{s_{2}}, x_{3}^{s_{2}^{'}}}, \dots$ , ${x_{m - 1}^{s_{m - 1}}, x_{m}^{s_{m - 1}^{'}}}}$ be the restricted path graph of a 2-CNF F, then $# 2 SAT (F) = \sum_{h = 1}^{| S_{m}^{i} |} l_{i} [h]$

Proof 1. Done by induction comparing the result of the equation 1. The case when there is a simple clause ${x_{1}^{s}, x_{2}^{s^{'}}}$ , s = s′ = 1, the number of models corresponds with that computed with the equation 1 given by the sum of the tuples (Fig. 3). The size of the set S₂ represents the number of models (Fig. 4).

Fig. 3

Counting models on path P₂ using Equation 1.

Fig. 4

Construction of the satisfiable set S₂ for a path P₂.

On a path P₃, with edges ${{x_{1}^{ε_{i}}, x_{2}^{γ_{i}}}, {x_{2}^{ε_{j}}, x_{3}^{γ_{j}}}}$ , the number of models is either 5 if (γ_i = ε_j) or 4 if (γ_i ≠ ε_j).

Fig. 5

Path P₃ with 5 models computed via equation 1.

Fig. 6

Constructing the set S₃ for P₃ computed via equation 1_sat_set.

Fig. 7

Path P₃ with 4 models calculated via equation 1.

Fig. 8

Constructing the set S₃ for P₃ calculated via equation 1_sat_set.

In both figures (Figs. 6 and 8) the size of the set S₃, calculated through the equation 1_sat_set, provides the number of models on each graph, respectively.

A list l_i is built, where $S_{m}^{i}$ contains every model of $P_{m}^{i}$ , and has initial values of 1, which represents the number of times that an index (an assignment over the variables of $P_{m}^{i}$ ) appears on the total models of the path. Clearly, the sum of the elements in l_i is equal to the size of $S_{m}^{i}$ , therefore $# 2 SAT (F) = | S_{m}^{i} | = \sum_{h = 1}^{| S_{m}^{i} |} l_{i} [h]$ .

4.2 Applying the list counting method on grid formulas

Given the grid graph G_m,2, with paths $P_{m}^{1}$ and $P_{m}^{2}$ and the set of edges between them {((j, 1) ^s, (j, 2) ^s′) ∣1 ≤ j ≤ m}. We built the set z₁ = {(s, s′) ₁, (s, s′) ₂, . . . , (s, s′) _m} for each pair of signs between the variables (j, 1) ^s and (j, 2) ^s′, and we call it conditionals of the formula represented by the graph. Let $S_{m}^{1}$ and $S_{m}^{2}$ be the satisfiable sets of $P_{m}^{1}$ and $P_{m}^{2}$ , respectively.

Our method compare the satisfiable assignments over $P_{m}^{i}$ and $P_{m}^{2}$ , and uses the elements of $S_{m}^{1}$ to calculate the size of the list l₁ and $S_{m}^{2}$ for the size of the list l₂.

We call this method as the counting transfer list. It calculates the values on the list l₂ using the values on l₁ and the elements of the set z₁.

The algorithm 1 compares each index of $S_{m}^{2}$ with the indexes of $S_{m}^{1}$ using the conditionals on z₁. The algorithm 2 compares pairwise the elements of the indexes, using π_j (w) as projection function on the j - th element of the tuple w, with their respective conditional using the fact that the size of each index in both $S_{m}^{1}$ and $S_{m}^{2}$ is the same as the set z_i.

Algorithm 1: ListCountingTransfer(l1,l2,Sm1,Sm2,z1)
Require: Lists l₁ and l₂, the sets $S_{m}^{1}$ and $S_{m}^{2}$ , the conditional set z₁
for all element k in l₂, $1 \leq k \leq # SAT (P_{m}^{2})$ do
sum = 0
for all element h in l₁, $1 \leq h \leq # SAT (P_{m}^{1})$ do
${idx}_{1} = S_{m}^{1} [h]$
${idx}_{2} = S_{m}^{2} [k]$
sum = sum + Comp (idx₁, idx₂, z₁) * l₁ [h]
end for
l₂ [k] = sum
end for
return l ₂

Algorithm 2: Comp(idx1,z,idx2)
Require: First index idx₁, second index idx₂ and the set z
val = 1
m = \|idx₁\| = \|idx₂\| = \|z\|
forj = 1, j ≤ mdo
ifπ_j (idx₁) ≠ π₁ (z [j]) andπ_j (idx₂) ≠ π₂ (z [j]) then
val = 0
end if
end for
return val

Lemma 2. Let F be a formula representing the grid graph G_m,2, then $# 2 SAT (F) = \sum_{k = 1}^{| S_{m}^{2} |} l_{2} [k]$

Proof 2. The result of the grid graph G_2,2 (the grid graph with two rows and two columns) is computed as follows:

Fig. 9

Grid graph G_2,2.

Given the grid graph G_2,2 in Fig. 9, V (G_2,2) = {(1, 1) , (2, 1) , (1, 2) , (2, 2)} and E (G_2,2) = {((1, 1) ¹, (2, 1) ¹) , ((1, 2) ¹, (2, 2) ⁰) , ((1, 1) ⁰, (1, 2) ⁰) , ((2, 1) ⁰, (2, 2) ¹)}. The construction of the lists l₁, l₂ and the set z₁ through the satisfiable sets $S_{m}^{1} = {10, 01, 11}$ and $S_{m}^{2} = {00, 10, 11}$ .

l₁ = [1, 1, 1]

l₂ = [1, 1, 1]

z₁ = {(0, 0) ₁, (0, 1) ₂}

The first set of comparisons are computed using the first index of $S_{m}^{2}$ and every index of $S_{m}^{1}$ . In order to ensure consistency on the new model count, we use the set of conditionals z₁.

The first comparison is made using the element $S_{m}^{2} [1] = 00$ and the element $S_{m}^{1} [1] = 10$ , thus, the first conditional z₁ [1] = (0, 0) is satisfied and the second conditional z₁ [2] = (0, 1) is also satisfied. The assignment 1000 is a model of F, this means that we need to satisfy all conditionals from z₁ in order to consider the assignment as a model of F. Table 1 shows the indexes, the new assignment, and if it is a model or not.

Table 1

Comparisons of l₂ [1] versus l₁

$S_{m}^{2} [1]$	$S_{m}^{1} [h]$	Assignment	It’s a model?
00	10	1000	yes
00	01	0100	no
00	11	1100	no

The value of l₂ [1] is the sum of the elements l₁ [h], whose index in $S_{m}^{1}$ forms a model of F with the index of $S_{m}^{2} [1]$ . Therefore, l₂ [1] =2.

The total of comparisons are shown in Table 2.

Table 2

Total of comparisons of l₂ versus l₁

$S_{m}^{2} [k]$	$S_{m}^{1} [h]$	Assignment	It’s a model?
00	10	1000	yes
00	01	0100	no
00	11	1100	no
10	10	1010	no
10	01	0110	no
10	11	1110	no
11	10	1011	no
11	01	0111	yes
11	11	1111	no

Thus, the new values of the list l₂ are:

Fig. 10

List l₂.

The number of models in F is the sum of the elements in the updated list l₂, having $| S_{m}^{2} | = | S_{3}^{2} | = 3$ , then $# SAT (F) = \sum_{k = 1}^{3} l_{2} [k] = 2$ . In general, the comparison method works for any value of m, by constructing the total of assignments between two lists and only counting the ones that are models of F. Furthermore, for any m we have $# SAT (F) = \sum_{k = 1}^{| S_{m}^{2} |} l_{2} [k]$ .

In brief, the list counting method is a combinatorial algorithm that operates on two lists $S_{m}^{1}$ and $S_{m}^{2}$ . Each element of $S_{m}^{2}$ is compared with each element of $S_{m}^{1}$ , which are represented by the lists l₁ and l₂, respectively, in order to obtain the modified list l₂.

ListCountingTransfer(l1,l2,Sm1, Sm2,z) → l2 .

ListCountingTransfer(l2,l1,Sm2, Sm1,z) → l1 .

4.3 An algorithm for counting models on grid formulas

Let us consider the grid graph G_m,n with paths $P_{m}^{1}, P_{m}^{2}, . . ., P_{m}^{n}$ , the lists l₁, l₂, . . . , l_n and the sets of conditionals z₁, z₂, . . . z_n-1.

The general algorithm 3 shows a method for counting the number of models of G_m,n.

Algorithm 3: GeneralCounting(Gm,n)
Require: Grid graph G_m,n
Divide the grid graph in n paths of size m, $P_{m}^{i}$
Construct the list l₁ using the indexes via equation 2
fori = 1, i < ndo
Construct the list l_i+1 using the indexes via equation 2
Construct the set of conditionals z_i
$l_{i + 1} = ListCountingTransfer (l_{i}, l_{i + 1}, S_{m}^{i},$
$S_{m}^{i + 1}, z_{i})$
end for
return l _n

The algorithm 3 works dividing the grid graph G_m,n in n paths $P_{m}^{i}$ . In a iterative process on all path, use the list l_i and the conditionals z_i in order to update the list l_i+1.

Theorem 1. Let F be a formula representing the grid graph G_m,n, then $# 2 SAT (F) = \sum_{k = 1}^{| S_{m}^{n} |} l_{n} [k]$

Proof 3. By induction on the paths $P_{m}^{1}$ and $P_{m}^{2}$ , the Lemma 2 is applied, updating the list l₂. For the paths $P_{m}^{2}$ and $P_{m}^{3}$ the Lemma 2 is applied, updating the list l₃, then by the repeated application of Lemma 2 over the paths P_i and P_i+1, 1 ≤ i < n, we can obtain the updated list l_n after the application of Lemma 2 over $P_{m}^{n - 1}$ and $P_{m}^{n}$ .

Through Lemma 2, the number of models of the grid graph G_m,n is given by the sum of the elements in the list l_n, $# SAT (F) = \sum_{k = 1}^{| S_{m}^{n} |} l_{n} [k]$ .

The flexibility of this combinatorial operations on lists, with respect to the transfer matrix method, allows the possible existence and processing of diagonal edges, which the matrix method does not allow.

5 Complexity analysis

The computation of the satisfiable set S_m is an exponential time method, the max size of a set S_m is related to the (m + 2) - th Fibonacci number. For example, the computation of a monotone positive formula is similar to the calculation of independent sets of its restricted graph. The number of independent sets of a path P_m is given directly by the value of the m + 2 Fibonacci number. The tightest upper bound for the growth of the Fibonacci number function F_n is of order O (1 .618ⁿ).

The general algorithm 3 constructs the n lists $S_{m}^{i}$ and l_i, with complexity at most of order O (F_m+2) = O (1 .618^m+2). Therefore, the final computation of the n pair of lists is O (n · 1 .618^m+2). The sets of conditionals z_i take n · m time to build. For each list l_i, 1 ≤ i < n, the algorithm 1 compares the lists $S_{m}^{i}$ and $S_{m}^{i + 1}$ over all of their elements using the algorithm 2. The algorithm 2 takes O (m) time to compute the comparison of two indexes. The algorithm 1 takes O ((F_m+2) ²) time. Furthermore, the computation of the list l_n takes n · (F_m+2) ² · m time. Then, if the total number of vertices is t = n · m, our algorithm has an upper bound of order $O (\sqrt{t} \cdot 1 . 618^{\sqrt{t} + 2} + t \cdot 1 . 618^{2 \sqrt{t} + 4})$ .

Fig. 11

Complexity comparison of the Wahlström algorithm versus the combinatorial operations on lists for grid graphs.

In consideration of the worst case scenario, when n is equal to m, and the number of vertices in the grid graph is t = n², the total of operations can be simplified by having an upper bound of order $O (t \cdot 1 . 618^{2 \sqrt{t}})$ .

We have compared our proposal versus the Wahlström algorithm, which have a time-complexity of order O (1 .2377^t), and where t = n · m is the total number of vertices in the graph.

The plot in Fig. 11 shows the complexity-time functions for both algorithms: Wahlström’s algorithm and the counting transfer list. The plot shows two intersection intervals: (0.0459, 64.9822) when Wahlström gives a better time complexity; and the interval (64.9822, ∞) when our algorithm has a better asymptotic time behavior with respect to the Wahlström’s algorithm.

6 Conclusions

In this paper we have introduced a novel algorithm to compute the # 2SAT (F), when F is a formula whose restricted graph is represented by a grid graph G_m,n. We show that our algorithm is correct and its time complexity is $O (\sqrt{t} \cdot 1 . 618^{\sqrt{t} + 2} + t \cdot 1 . 618^{2 \sqrt{t} + 2})$ , where t = n · m is the total number of vertices in the graph. This upper bound improves the asymptotic behavior of the time-complexity with respect to other algorithms in the area for counting models for this class of formulas. As future works, we are considering extend our method for considering grid graph topology with optional diagonal edges, as well as to omit some vertices on the base grid.

References

Winkler

and Brifhtwell

, Counting linear extensions, Order8(e) (1991), 225–242.

Roth

, On the hardness of approximate reasoning, Artificial Intelligence82 (1996), 273–302.

Darwiche

, On the tractable counting of theory models and its application to truth maintenance and belief revision, Journal of Applied Non-Classical Logics11 (2012), 11–34.

Takamizawa

, Nishizeki

and Saito

, Lineartime computability of combinatorial problems on series-parallel graphs, Journal of the Association for Computing Machinery29(3) (1982), 623–641.

Marcial-Romero

J.R.

, De Ita

, Hernández

J.A.

and Valdovinos

R.M.

, A parametric polynomial deterministic algorithm for #2sat, Lecture Notes in Computer Science9413 (2015), 202–213.

Szeider

, On Fixed-Parameter Tractable Parametrizations of SAT, Springer Berlin Heidelberg (2004), pp. 188–202.

López-Medina

M.A.

, Marcial-Romero

J.R.

, De Ita Luna

, Montes-Venegas

H.A.

and Alejo

, A linear time algorithm for solving #2SAT on cactus formulas, CoRR, ams/1702.08581, 2017.

López-Medina

M.A.

, Marcial-Romero

J.R.

, De Ita

and Moyao

, A Linear Time Algorithm for Computing #2SAT for Outerplanar 2-CNFFormulas, Lecture Notes in Computer Science10880(2018), 72–81.

Wahlström

, A tighter bound for counting maxweight solutions to 2sat instances, Springer Berlin Heidelberg (2008), pp. 202–213.

10.

Calkin

and Wilf

, The number of independent sets in a grid graph, SIAM Journal on Discrete Mathematics11 (1998), 02.

11.

Euler

, The fibonacci number of a grid graph and a new class of integer sequences, Journal of Integer Sequences8 (2005), 05.

12.

Golin

, Cho Leung

, Wang

and Yong

, Counting structures in grid graphs, cylinders and tori using transfer matrices: Survey and new results. In ALENEX/ANALCO (2005), pp. 250–258, 01.

13.

Guillen

, Lopez Lopez

and De Ita

, Computing #2-sat of grids, grid-cylinders and grid-tori boolean formulas. In Proceedings of the 15th RCRA workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion 451. CEUR-WS.org, 2008.

14.

Baxter

R.J.

, Planar lattice gases with nearestneighbor exclusion,191–203, Jun, Annals of Combinatorics3(2-4) (1999).

15.

Roth

R.M.

, Siegel

P.H.

and Wolf

J.K.

, Efficient coding schemes for the hard-square model, IEEE Trans Inform Theory47 (2001), 1166–1176.

16.

López-Medina

M.A.

, Marcial-Romero

J.R.

, De Ita

and Valdovinos

R.M.

, A fast and efficient method for #2sat via graph transformations, Advances in Soft Computing (2017), pp. 95–106.