Solving MaxSAT and \#SAT on structured CNF formulas

DOI10.1007/978-3-319-09284-3_3MaRDI QIDQ3192052zbMATH OpenOpenAlexFDO

Authors Sigve Hortemo Sæther, Jan Arne Telle, Martin Vatshelle

Publication date 26 September 2014

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1402.6485

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

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 precisely satisfiable if there is some complete assignment satisfying these clauses only. Let the ps-value of the formula be the number of precisely 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 $O(m^2(m+n)s)$ algorithms for formulas $F$ of $m$ clauses and $n$ variables and 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.

Recommendations

• Solving #SAT and MAXSAT by Dynamic Programming
• Resolution and linear CNF formulas: improved \((n,3)\)-\textsc{MaxSAT} algorithms
• New width parameters for SAT and \#SAT
• scientific article; zbMATH DE number 1522934
• Counting truth assignments of formulas of bounded tree-width or clique-width

Cited in

(6)

• Complexity and approximability of parameterized MAX-CSPs
• Solving #SAT and MAXSAT by Dynamic Programming
• On compiling CNFs into structured deterministic DNNFs
• Solving SAT for CNF Formulas with a One-Sided Restriction on Variable Occurrences
• Tractable QBF by knowledge compilation
• Direct access for conjunctive queries with negations

This page was built for publication: Solving MaxSAT and \#SAT on structured CNF formulas

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3192052)