Solving MaxSAT and #SAT on structured CNF formulas

10Citations
Citations of this article
7Readers
Mendeley users who have this article in their library.
Get full text

Abstract

In this paper we propose a structural parameter of CNF formulas and use it to identify instances of weighted MaxSAT and #SAT that can be solved in polynomial time. Given a CNF formula we say that a set of clauses is projection satisfiable if there is some complete assignment satisfying these clauses only. Let the ps-value of the formula be the number of projection satisfiable sets of clauses. Applying the notion of branch decompositions to CNF formulas and using ps-value as cut function, we define the ps-width of a formula. For a formula given with a decomposition of polynomial ps-width we show dynamic programming algorithms solving weighted MaxSAT and #SAT in polynomial time. Combining with results of 'Belmonte and Vatshelle, Graph classes with structured neighborhoods and algorithmic applications, Theor. Comput. Sci. 511: 54-65 (2013)' we get polynomial-time algorithms solving weighted MaxSAT and #SAT for some classes of structured CNF formulas. For example, we get algorithms for formulas F of m clauses and n variables and total size s, if F has a linear ordering of the variables and clauses such that for any variable x occurring in clause C, if x appears before C then any variable between them also occurs in C, and if C appears before x then x occurs also in any clause between them. Note that the class of incidence graphs of such formulas do not have bounded clique-width. © 2014 Springer International Publishing Switzerland.

Cite

CITATION STYLE

APA

Sæther, S. H., Telle, J. A., & Vatshelle, M. (2014). Solving MaxSAT and #SAT on structured CNF formulas. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8561 LNCS, pp. 16–31). Springer Verlag. https://doi.org/10.1007/978-3-319-09284-3_3

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free