The Taming of the (X)OR
The Taming of the (X)OR
复制标题
(X)OR 的驯服
DOI：
10.1007/3-540-44957-4_34
复制
发表时间：
2000
期刊：
影响因子：
--
通讯作者：
F. Massacci
中科院分区：
文献类型：
--
作者：
Peter Baumgartner;F. Massacci
有界模型检验、电路验证和逻辑密码分析等关键验证问题通常采用子句和仿射逻辑相结合的形式化方法（即以异或为连接词的子句）来形式化，而仅使用CNF证明器无法有效地解决这些问题。Gauss-DPLL过程是在Gauss-Elimination过程的统一框架中的紧密集成（仿射逻辑）和Davis-Putnam-Logeman-Loveland过程（用于通常的子句逻辑）。将我们的方法与其他方法区分开来的关键思想是，是两个部分之间的充分互动，（确定性的）简化规则，通过传递新创建的单位或二进制子句，我们证明了Gauss-DPLL在非常自由的假设下的正确性和终止性。
Many key verification problems such as boundedmodel-checking, circuit verification and logical cryptanalysis are formalized with combined clausal and affine logic (i.e. clauses with xor as the connective) and cannot be efficiently (if at all) solved by using CNF-only provers.We present a decision procedure toefficientlydecide such problems. The Gauss-DPLL procedure is a tight integration in a unifying framework of a Gauss-Elimination procedure (for affine logic) and a Davis-Putnam-Logeman-Loveland procedure (for usual clause logic).The key idea, which distinguishes our approach from others, is the full interaction bewteen the two parts which makes it possible to maximize (deterministic) simplification rules by passing around newly created unit or binary clauses in either of these parts.We show the correcteness and the termination of Gauss-DPLL under very liberal assumptions.