The Taming of the (X)OR

Abstract. 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 to efficiently decide such problems. The GaussDPLL procedureis 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.

• Type: Conference
• Year: 2000
• Where: CL
• Authors: Peter Baumgartner, Fabio Massacci
• Keywords: Affine Logic, Automated Reasoning, CL 2000, Many Key Verification, Usual Clause Logic