Solving MaxSAT and #SAT on Structured CNF Formulas
Solving MaxSAT and #SAT on Structured CNF Formulas
复制标题
求解 MaxSAT 和
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
M. Vatshelle
中科院分区：
文献类型：
--
作者：
S. H. Sæther;J. A. Telle;M. Vatshelle
在本文中，我们提出了 CNF 公式的结构参数，并用它来识别可以在多项式时间内求解的加权 MaxSAT 和 #SAT 实例。给定 CNF 公式，如果存在仅满足这些子句的某个完整赋值，则我们说一组子句是投影可满足的。令公式的 ps 值为投影可满足子句集的数量。将分支分解的概念应用于 CNF 公式并使用 ps 值作为剪切函数，我们定义了公式的 ps 宽度。对于通过多项式 ps-width 分解给出的公式，我们展示了在多项式时间内求解加权 MaxSAT 和 #SAT 的动态规划算法。结合贝尔蒙特和 Vatshelle、具有结构化邻域和算法应用的图类、Theor 的结果。计算。科学。 511: 54-65 (2013)’，我们得到了多项式时间算法，可以求解某些类别的结构化 CNF 公式的加权 MaxSAT 和 #SAT。例如，我们得到 ({mathcal O}(m^2(m + n)s)) 公式 F 的 m 个子句和 n 个变量以及总大小 s 的算法，如果 F 具有变量和子句的线性排序，使得对于子句 C 中出现的任何变量 x，如果 x 出现在 C 之前，则它们之间的任何变量也出现在 C 中，如果 C 出现在 x 之前，则 x 也出现在它们之间的任何子句中。请注意，此类公式的关联图类别没有有界的团宽度。
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 ({mathcal O}(m^2(m + n)s)) 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.