Clausal Proofs for Pseudo-Boolean Reasoning
Clausal Proofs for Pseudo-Boolean Reasoning
复制标题
伪布尔推理的子句证明
DOI：
10.1007/978-3-030-99524-9_25
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Heule, Marijn J.
中科院分区：
文献类型：
--
作者：
Bryant, Randal E.;Heule, Marijn J.
当使用伪布尔（PB）求解器增强时，布尔可满足性（SAT）求解器可以应用强大的推理方法来确定从输入公式的子句中提取的奇偶性或基数约束的集合何时没有解。通过将PB求解器生成的中间约束转换为有序二元决策图（BDD），基于BDD的证明生成SAT求解器可以生成输入公式不可满足的子句证明。两个求解器一起工作，可以为其他证明生成SAT求解器难以解决的问题生成不可满足性证明。PB求解器有时可以检测到证明可以利用模运算来给出更小的BDD表示，从而缩短证明。
When augmented with a Pseudo-Boolean (PB) solver, a Boolean satisfiability (SAT) solver can apply apply powerful reasoning methods to determine when a set of parity or cardinality constraints, extracted from the clauses of the input formula, has no solution. By converting the intermediate constraints generated by the PB solver into ordered binary decision diagrams (BDDs), a proof-generating, BDD-based SAT solver can then produce a clausal proof that the input formula is unsatisfiable. Working together, the two solvers can generate proofs of unsatisfiability for problems that are intractable for other proof-generating SAT solvers. The PB solver can, at times, detect that the proof can exploit modular arithmetic to give smaller BDD representations and therefore shorter proofs.
登录
查看更多内容
DOI：
10.1007/978-3-030-79876-5_15
发表时间：
2021
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
L. Barnett;Armin Biere;L. Barnett;Armin Biere
通讯作者：
Armin Biere
布尔公式的自动重新编码
DOI：
--
发表时间：
2012
期刊：
Haifa Verification Conference
影响因子：
--
作者：
Norbert Manthey;Marijn J. H. Heule;Armin Biere
通讯作者：
Armin Biere
DOI：
10.1007/978-3-030-51825-7_1
发表时间：
2020-06-26
期刊：
Theory and Applications of Satisfiability Testing – SAT 2020
影响因子：
--
作者：
Chew L;Heule MJ
通讯作者：
Heule MJ
使用基于 BDD 的 SAT 求解器生成扩展分辨率证明
影响因子：
0.5
作者：
Bryant, Randal E.;Heule, Marijn J.
通讯作者：
Heule, Marijn J.
检测 CNF 中的基数约束
DOI：
--
发表时间：
2014
期刊：
International Conference on Theory and Applications of Satisfiability Testing
影响因子：
--
作者：
Armin Biere;Daniel Le Berre;Emmanuel Lonca;Norbert Manthey
通讯作者：
Norbert Manthey