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 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.
F. Massacci acknowledges the support of a STM CNR grant.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
BCC+99._A. Biere, A. Cimatti, E. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using SAT procedures instead of BDDs. In Proc. of ACM/IEEE DAC-99, pages 317–320. ACM Press, 1999.
B. Becker, R. Drechsler, and R. Werchner. On the relation between BDDs and FDDs. Inf. and Comp., 123(2):185–197, 1995.
K. Brace, R. Rudell, and R. Bryant. Efficient implementation of a BDD package. In Proc. of ACM/IEEE DAC-90, pages 40–45. IEEE Press, 1990.
R. Bayardo and R. Schrag. Using CSP look-back techniques to solve real-world SAT instances. In Proc. of AAAI-97, pages 203–208. AAAI Press/TheMIT Press, 1997.
J. Crawford and L. Auton. Experimental results on the crossover point in random 3SAT. AIJ, 81(1–2):31–57, 1996.
C. Chang and R. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973.
L. Claesen, ed. Formal VLSI Correctness Verification: VLSI Design Methods, volume II. Elsevier, 1990.
R. Drechsler, B. Becker, and S. Ruppertz. Manipulation algorithms for K*BMDs. In Proc. of TACAS-97, LNCS 1217, pages 4–18. Springer-Verlag, 1997.
M. Davis, G. Logeman, and D. Loveland. A machine program for theorem proving. CACM, 5(7), 1962.
E. Giunchiglia, A. Massarotto, and R. Sebastiani. Act and the rest will follow: Expliting nondeterminismin planning as satisfiability. In Proc. of AAAI-98, pages 948–952. The MIT Press, 1998.
J. Groote and J. Warners. The propositional formula checker HeerHugo. JAR, 2000. To appear.
U. Hustadt and R. Schmidt. Simplification and backjumping in modal tableau. In Proc. of TABLEAUX-98, LNAI 1397, pages 187–201. Springer-Verlag, 1998.
D. Johnson and M. Trick, eds. Cliques, Coloring, satisfiability: the second DIMACS implementation challenge, volume 26 of AMS Series in Discr. Math. and TCS. AMS, 1996.
H. Kautz and B. Selman. Pushing the envelope: Planning, propositional logic and stocastic search. In Proc. of AAAI-96, pages 1194–1201. The MIT Press, 1996.
Chu-Min Li. A constraint-based approach to narrow search trees for satisfiability. IPL, 71(2):75–80, 1999.
Chun-Min Li. Integrating equivalency reasoning into Davis-Putnam procedure. To appear in Proc. of AAAI-00.
Fabio Massacci. Simplification: A general constraint propagation technique for propositional and modal tableaux. In Proc. of TABLEAUX-98, LNAI 1397, pages 217–231. Springer-Verlag, 1998.
Fabio Massacci. Using Walk-SAT and Rel-sat for cryptographic key search. In Proc. of IJCAI-99, pages 290–295.Morgan Kaufmann, 1999.
Fabio Massacci and Laura Marraro. Logical cryptanalysis as a SAT-problem: Encoding and analysis of the u.s. Data Encryption Standard. JAR, 2000. To appear.
T. Schaefer. The complexity of satisfiability problems. In Proc. of STOC-78, pages 216–226. ACM Press, 1978.
Bart Selman, Henry Kautz, and David McAllester. Ten challenges in propositional resoning and search. In Proc. of IJCAI-97, pages 50–54. Morgan Kaufmann, 1997.
J. Wilson. Compact normal forms in propositional logics and integer programming formulations. Comp. and Op. Res., 17(3):309–314, 1990.
J. Warners and H. van Maaren. A two phase algorithm for solving a class of hard satisfiability problems. Op. Res. Lett., 23(3–5):81–88, 1999.
J. Warners and H. van Maaren. Recognition of tractable satisfiability problems through balanced polynomial representations. Discr. Appl. Math., 2000.
H. Zhang. SATO: An Efficient Propositional Theorem Prover. In Proc. of CADE 97, LNAI 1249, pages 272–275, 1997. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baumgartner, P., Massacci, F. (2000). The Taming of the (X)OR. In: Lloyd, J., et al. Computational Logic — CL 2000. CL 2000. Lecture Notes in Computer Science(), vol 1861. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44957-4_34
Download citation
DOI: https://doi.org/10.1007/3-540-44957-4_34
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67797-0
Online ISBN: 978-3-540-44957-7
eBook Packages: Springer Book Archive