A method for counting models on grid Boolean formulas1.

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 (t · 1. 618 t + 2 + t · 1. 618 2 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. [ABSTRACT FROM AUTHOR]