论文标题
生成CNF公式的子句序列
Generating clause sequences of a CNF formula
论文作者
论文摘要
给定一个带有条款$ C_1，\ ldots，c_m $和变量的CNF公式$φ$ $ $σ_φ（a）=（c_1（a），\ ldots，c_m（a））\ in \ {0,1 \}^m $其中$ c_i（a）= 1 $如果条款$ c_i $评估为$ 1 $ $ 1 $ $ 1 $ $ 1 $ $ $ a $ a $ a $，否则$ c_i（a $ a $）= 0 $。所有可能的子句序列的集合都带有有关公式的大量信息，例如SAT，Max-SAT和Min-SAT可以通过查找具有极端特性的子句序列进行编码。 我们考虑在19211年Dagstuhl研讨会上提出的问题“数据管理中的枚举”（2019年），内容涉及具有有界维度的给定CNF的所有可能子句序列的生成。我们证明问题可以在增量多项式时间内解决。我们进一步给出了具有多项式延迟的算法。我们还考虑了最大和最小从句序列的产生，并表明生成最大从句序列是NP-固定，而最小的子句序列可以用多项式延迟生成。
Given a CNF formula $Φ$ with clauses $C_1,\ldots,C_m$ and variables $V=\{x_1,\ldots,x_n\}$, a truth assignment $a:V\rightarrow\{0,1\}$ of $Φ$ leads to a clause sequence $σ_Φ(a)=(C_1(a),\ldots,C_m(a))\in\{0,1\}^m$ where $C_i(a) = 1$ if clause $C_i$ evaluates to $1$ under assignment $a$, otherwise $C_i(a) = 0$. The set of all possible clause sequences carries a lot of information on the formula, e.g. SAT, MAX-SAT and MIN-SAT can be encoded in terms of finding a clause sequence with extremal properties. We consider a problem posed at Dagstuhl Seminar 19211 "Enumeration in Data Management" (2019) about the generation of all possible clause sequences of a given CNF with bounded dimension. We prove that the problem can be solved in incremental polynomial time. We further give an algorithm with polynomial delay for the class of tractable CNF formulas. We also consider the generation of maximal and minimal clause sequences, and show that generating maximal clause sequences is NP-hard, while minimal clause sequences can be generated with polynomial delay.
