A method for counting models on grid Boolean formulas¹

Issue title: Recent Advances in Language & Knowledge Engineering

Guest editors: David Pinto, Beatriz Beltrán and Vivek Singh

Article type: Research Article

Authors: López-Medina, Marco A.^{; *} | Marcial-Romero, J. Raymundo | De Ita Luna, Guillermo | Hernández, José A.

Affiliations: Facultad de Ingeniería, UAEMex and Facultad de Ciencias de la Computación, BUAP

Correspondence: [*] Corresponding author. Marco A. López-Medina. E-mail: mlopezm158@alumno.uaemex.mx.

Note: [1] This paper and the research behind it would not have been possible without the support of CONACYT scholarship CVU:787172.

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 Gm,n. We show that our algorithm is correct and its time complexity is O(t·1.618t+2+t·1.6182t+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

DOI: 10.3233/JIFS-219259

Journal: Journal of Intelligent & Fuzzy Systems, vol. 42, no. 5, pp. 4719-4726, 2022