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 Gm,n. We show that our algorithm is correct and its time complexity is , 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.
WinklerP. and BrifhtwellG., Counting linear extensions, Order8(e) (1991), 225–242.
2.
RothD., On the hardness of approximate reasoning, Artificial Intelligence82 (1996), 273–302.
3.
DarwicheA., 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.
4.
TakamizawaK., NishizekiT. and SaitoN., Lineartime computability of combinatorial problems on series-parallel graphs, Journal of the Association for Computing Machinery29(3) (1982), 623–641.
5.
Marcial-RomeroJ.R., De ItaG., HernándezJ.A. and ValdovinosR.M., A parametric polynomial deterministic algorithm for #2sat, Lecture Notes in Computer Science9413 (2015), 202–213.
6.
SzeiderS., On Fixed-Parameter Tractable Parametrizations of SAT, Springer Berlin Heidelberg (2004), pp. 188–202.
7.
López-MedinaM.A., Marcial-RomeroJ.R., De Ita LunaG., Montes-VenegasH.A. and AlejoR., A linear time algorithm for solving #2SAT on cactus formulas, CoRR, ams/1702.08581, 2017.
8.
López-MedinaM.A., Marcial-RomeroJ.R., De ItaG. and MoyaoY., A Linear Time Algorithm for Computing #2SAT for Outerplanar 2-CNFFormulas, Lecture Notes in Computer Science10880(2018), 72–81.
9.
WahlströmM., A tighter bound for counting maxweight solutions to 2sat instances, Springer Berlin Heidelberg (2008), pp. 202–213.
10.
CalkinN. and WilfH., The number of independent sets in a grid graph, SIAM Journal on Discrete Mathematics11 (1998), 02.
11.
EulerR., The fibonacci number of a grid graph and a new class of integer sequences, Journal of Integer Sequences8 (2005), 05.
12.
GolinM., Cho LeungY., WangY. and YongX., Counting structures in grid graphs, cylinders and tori using transfer matrices: Survey and new results. In ALENEX/ANALCO (2005), pp. 250–258, 01.
13.
GuillenC., Lopez LopezA. and De ItaG., 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.
BaxterR.J., Planar lattice gases with nearestneighbor exclusion,191–203, Jun, Annals of Combinatorics3(2-4) (1999).
15.
RothR.M., SiegelP.H. and WolfJ.K., Efficient coding schemes for the hard-square model, IEEE Trans Inform Theory47 (2001), 1166–1176.
16.
López-MedinaM.A., Marcial-RomeroJ.R., De ItaG. and ValdovinosR.M., A fast and efficient method for #2sat via graph transformations, Advances in Soft Computing (2017), pp. 95–106.
