A method for counting models on grid Boolean formulas

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(root t . 1.618(root t+2) + t . 1.6182(root 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.