Abstract
In this paper we present an implementation (markSAT) for computing #2SAT via graph transformations. For that, we transform the input formula into a graph and test whether it is which we call a cactus graph. If it is not the case, the formula is decomposed until cactus sub-formulas are obtained. We compare the efficiency of markSAT against sharpSAT which is the leading sequential algorithm in the literature for computing #SAT obtaining better results with our proposal.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Ita Luna, G.: Polynomial classes of boolean formulas for computing the degree of belief. In: Lemaître, C., Reyes, C.A., González, J.A. (eds.) IBERAMIA 2004. LNCS (LNAI), vol. 3315, pp. 430–440. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30498-2_43
Brightwell, G., Winkler, P.: Counting linear extensions. Order 8(3), 225–242 (1991)
Paulusma, D., Slivovsky, F., Szeider, S.: Model counting for cnf formulas of bounded modular treewidth. Algorithmica 76(1), 168–194 (2016)
Wahlström, M.: A tighter bound for counting max-weight solutions to 2SAT instances. In: Grohe, M., Niedermeier, R. (eds.) IWPEC 2008. LNCS, vol. 5018, pp. 202–213. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-79723-4_19
Schmitt, M., Wanka, R.: Exploiting independent subformulas: a faster approximation scheme for #k-sat. Inf. Process. Lett. 113(9), 337–344 (2013)
Bayardo Jr., R.J., Schrag, R.C.: Using CSP look-back techniques to solve real-world sat instances. In: Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Conference on Innovative Applications of Artificial Intelligence, AAAI 1997/IAAI 1997, pp. 203–208. AAAI Press (1997)
Thurley, M.: sharpSAT – counting models with advanced component caching and implicit BCP. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 424–429. Springer, Heidelberg (2006). https://doi.org/10.1007/11814948_38
Burchard, J., Schubert, T., Becker, B.: Laissez-faire caching for parallel #SAT solving. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 46–61. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24318-4_5
Szeider, S.: On fixed-parameter tractable parameterizations of SAT. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 188–202. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24605-3_15
De Ita, G., Bello López, P., González, M.C.: New polynomial classes for #2SAT established via graph-topological structure. Eng. Lett. 15, 250–258 (2007)
Marcial-Romero, J.R., De Ita Luna, G., Hernández, J.A., Valdovinos, R.M.: A parametric polynomial deterministic algorithm for #2SAT. In: Sidorov, G., Galicia-Haro, S.N. (eds.) MICAI 2015. LNCS (LNAI), vol. 9413, pp. 202–213. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-27060-9_16
Bondy, J.A., Murty, U.S.R.: Graph Theory, 3rd printing edn. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
López, M.A., Marcial-Romero, J.R., De Ita, G., Valdovinos, R.M. (2018). A Fast and Efficient Method for #2SAT via Graph Transformations. In: Castro, F., Miranda-Jiménez, S., González-Mendoza, M. (eds) Advances in Soft Computing. MICAI 2017. Lecture Notes in Computer Science(), vol 10632. Springer, Cham. https://doi.org/10.1007/978-3-030-02837-4_8
Download citation
DOI: https://doi.org/10.1007/978-3-030-02837-4_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-02836-7
Online ISBN: 978-3-030-02837-4
eBook Packages: Computer ScienceComputer Science (R0)