Non-clausal Redundancy Properties
Non-clausal Redundancy Properties
复制标题
非子句冗余属性
DOI：
10.1007/978-3-030-79876-5_15
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Armin Biere
中科院分区：
文献类型：
--
作者：
L. Barnett;Armin Biere;L. Barnett;Armin Biere
最先进的SAT反驳系统主要基于满足某些冗余标准的子句的推导，确保它们添加到公式中不会改变其可满足性。然而，有强大的命题推理技术，其推理不容易在这样的系统中表达。本文扩展了冗余框架以外的条款，布尔约束的冗余特征一般。我们表明，这种特征可以实例化，以开发有效的可检查的反驳系统，使用冗余属性的二元决策图（BDDs）。使用BDD的合取上的反向单元传播的形式，这些系统捕获例如在公式中编码的XOR约束上的高斯消除推理，而不需要子句翻译或扩展变量。值得注意的是，这些系统推广了基于强传播冗余（PR）属性的系统，而不会增加复杂性。
State-of-the-art refutation systems for SAT are largely based on the derivation of clauses meeting some redundancy criteria, ensuring their addition to a formula does not alter its satisfiability. However, there are strong propositional reasoning techniques whose inferences are not easily expressed in such systems. This paper extends the redundancy framework beyond clauses to characterize redundancy for Boolean constraints in general. We show this characterization can be instantiated to develop efficiently checkable refutation systems using redundancy properties for Binary Decision Diagrams (BDDs). Using a form of reverse unit propagation over conjunctions of BDDs, these systems capture, for instance, Gaussian elimination reasoning over XOR constraints encoded in a formula, without the need for clausal translations or extension variables. Notably, these systems generalize those based on the strong Propagation Redundancy (PR) property, without an increase in complexity.
使用基于 BDD 的 SAT 求解器生成扩展分辨率证明
影响因子：
0.5
作者：
Bryant, Randal E.;Heule, Marijn J.
通讯作者：
Heule, Marijn J.
DOI：
10.1007/s10817-019-09516-0
发表时间：
2020-03-01
期刊：
JOURNAL OF AUTOMATED REASONING
影响因子：
--
作者：
Heule, Marijn J. H.;Kiesl, Benjamin;Biere, Armin
通讯作者：
Biere, Armin