Efficiently checking propositional refutations in HOL theorem provers. (English) Zbl 1171.68041
Summary: This paper describes the integration of zChaff and MiniSat, currently two leading SAT solvers, with Higher Order Logic (HOL) theorem provers. Both SAT solvers generate resolution-style proofs for (instances of) propositional tautologies. These proofs are verified by the theorem provers. The presented approach significantly improves the provers’ performance on propositional problems, and exhibits counterexamples for unprovable conjectures. It is also shown that LCF-style theorem provers can serve as viable proof checkers even for large SAT problems. An efficient representation of the propositional problem in the theorem prover turns out to be crucial; several possible solutions are discussed.
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
Software:
ACL2; PVS; SATLIB; zChaff; Isabelle/HOL; Isabelle; ML; TRAMP; MiniSat; HOL Light; Chaff; Gandalf; LCF; CVC LiteReferences:
| [1] | Audemard, G.; Bertoli, P.; Cimatti, A.; Kornilowicz, A.; Sebastiani, R., A SAT based approach for solving formulas over Boolean and linear mathematical propositions, (Voronkov, A., Proceedings of the 18th International Conference on Automated Deduction (CADE-18). Proceedings of the 18th International Conference on Automated Deduction (CADE-18), Copenhagen, Denmark, July 2002. Proceedings of the 18th International Conference on Automated Deduction (CADE-18). Proceedings of the 18th International Conference on Automated Deduction (CADE-18), Copenhagen, Denmark, July 2002, Lecture Notes in Artificial Intelligence, vol. 2392 (2002), Springer), 195-210 · Zbl 1072.68562 |
| [2] | Amjad, H., Shallow lazy proofs, (Hurd, J.; Melham, T., Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics. Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science, vol. 3603 (2005), Springer), 35-49 · Zbl 1152.68515 |
| [3] | H. Amjad, Compressing propositional refutations, in: S. Merz, T. Nipkow (Eds.), Sixth International Workshop on Automated Verification of Critical Systems (AVOCS ’06)—Preliminary Proceedings, 2006, pp. 7-18; H. Amjad, Compressing propositional refutations, in: S. Merz, T. Nipkow (Eds.), Sixth International Workshop on Automated Verification of Critical Systems (AVOCS ’06)—Preliminary Proceedings, 2006, pp. 7-18 · Zbl 1335.68222 |
| [4] | Anbulagan, J. Slaney, Multiple preprocessing for systematic SAT solvers, in: C. Benzmüller, B. Fischer, G. Sutcliffe (Eds.), Proceedings of the 6th International Workshop on the Implementation of Logics, CEUR Workshop Proceedings, vol. 212, Phnom Penh, Cambodia, 2006, pp. 100-116; Anbulagan, J. Slaney, Multiple preprocessing for systematic SAT solvers, in: C. Benzmüller, B. Fischer, G. Sutcliffe (Eds.), Proceedings of the 6th International Workshop on the Implementation of Logics, CEUR Workshop Proceedings, vol. 212, Phnom Penh, Cambodia, 2006, pp. 100-116 |
| [5] | C.W. Barrett, Checking validity of quantifier-free formulas in combinations of first-order theories, PhD thesis, Stanford University, Stanford, California, January 2003; C.W. Barrett, Checking validity of quantifier-free formulas in combinations of first-order theories, PhD thesis, Stanford University, Stanford, California, January 2003 |
| [6] | C. Barrett, S. Berezin, CVC lite: A new implementation of the cooperating validity checker, in: Proceedings of the 16th International Conference on Computer Aided Verification (CAV 2004), Boston, Massachusetts, USA, July 2004; C. Barrett, S. Berezin, CVC lite: A new implementation of the cooperating validity checker, in: Proceedings of the 16th International Conference on Computer Aided Verification (CAV 2004), Boston, Massachusetts, USA, July 2004 · Zbl 1103.68605 |
| [7] | C. Barrett, S. Berezin, D.L. Dill, A proof-producing Boolean search engine, in: Proceedings of the Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2003), Miami, Florida, USA, July 2003; C. Barrett, S. Berezin, D.L. Dill, A proof-producing Boolean search engine, in: Proceedings of the Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2003), Miami, Florida, USA, July 2003 |
| [8] | DIMACS satisfiability suggested format (1993) |
| [9] | de Nivelle, H.; Meng, J., Geometric resolution: A proof procedure based on finite model search, (Furbach, U.; Shankar, N., Automated Reasoning—Third International Joint Conference, IJCAR 2006, Proceedings. Automated Reasoning—Third International Joint Conference, IJCAR 2006, Proceedings, Seattle, WA, USA, August 2006. Automated Reasoning—Third International Joint Conference, IJCAR 2006, Proceedings. Automated Reasoning—Third International Joint Conference, IJCAR 2006, Proceedings, Seattle, WA, USA, August 2006, Lecture Notes in Artificial Intelligence, vol. 4130 (2006), Springer), 303-317 · Zbl 1222.68378 |
| [10] | Eén, N.; Biere, A., Effective preprocessing in SAT through variable and clause elimination, (Bacchus, F.; Walsh, T., SAT. SAT, Lecture Notes in Computer Science, vol. 3569 (2005), Springer), 61-75 · Zbl 1128.68463 |
| [11] | Eén, N.; Sörensson, N., An extensible SAT-solver, (Giunchiglia, E.; Tacchella, A., Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003, Selected Revised Papers. Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003, Selected Revised Papers, Santa Margherita Ligure, Italy, May 5-8, 2003. Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003, Selected Revised Papers. Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003, Selected Revised Papers, Santa Margherita Ligure, Italy, May 5-8, 2003, Lecture Notes in Computer Science, vol. 2919 (2004), Springer), 502-518 · Zbl 1204.68191 |
| [12] | Eén, N.; Sörensson, N., MiniSat-p-v1.14—A proof-logging version of MiniSat, September 2006 |
| [13] | Fontaine, P.; Marion, J.-Y.; Merz, S.; Prensa Nieto, L.; Tiu, A., Expressiveness + automation + soundness: Towards combining SMT solvers and interactive proof assistants, (Hermanns, H.; Palsberg, J., Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Proceedings. Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Proceedings, Vienna, Austria, March 25-April 2, 2006. Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Proceedings. Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, TACAS 2006 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Proceedings, Vienna, Austria, March 25-April 2, 2006, Lecture Notes in Computer Science, vol. 3920 (2006), Springer), 167-181 · Zbl 1180.68240 |
| [14] | (Gordon, M. J.C.; Melham, T. F., Introduction to HOL: A Theorem Proving Environment for Higher Order Logic (1993), Cambridge University Press) · Zbl 0779.68007 |
| [15] | Gordon, M. J.C., From LCF to HOL: A short history, (Plotkin, G.; Stirling, C. P.; Tofte, M., Proof, Language, and Interaction (2000), MIT Press) |
| [16] | Gordon, M. J.C., HolSatLib 1.0b (June 2001) |
| [17] | Harrison, J., Binary decision diagrams as a HOL derived rule, The Computer Journal, 38, 2, 162-170 (1995) |
| [18] | Harrison, J., HOL light: A tutorial introduction, (Srivas, M. K.; Camilleri, A. J., FMCAD. FMCAD, Lecture Notes in Computer Science, vol. 1166 (1996), Springer), 265-269 |
| [19] | Harrison, J., Stålmarck’s algorithm as a HOL derived rule, (von Wright, J.; Grundy, J.; Harrison, J., Theorem Proving in Higher Order Logics. Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science, vol. 1125 (1996), Springer), 221-234 · Zbl 1543.68403 |
| [20] | Hoos, H. H.; Stützle, T., SATLIB: An online resource for research on SAT, (Gent, I.; van Maaren, H.; Walsh, T., SAT 2000 (2000), IOS Press), 283-292 · Zbl 0979.68128 |
| [21] | Hurd, J., Integrating Gandalf and HOL, (Bertot, Y.; Dowek, G.; Hirschowitz, A.; Paulin, C.; Théry, L., Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs ’99. Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs ’99, Nice, France, September 1999. Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs ’99. Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs ’99, Nice, France, September 1999, Lecture Notes in Computer Science, vol. 1690 (1999), Springer), 311-321 |
| [22] | Hurd, J., An LCF-style interface between HOL and first-order logic, (Voronkov, A., Proceedings of the 18th International Conference on Automated Deduction (CADE-18). Proceedings of the 18th International Conference on Automated Deduction (CADE-18), Copenhagen, Denmark, July 2002. Proceedings of the 18th International Conference on Automated Deduction (CADE-18). Proceedings of the 18th International Conference on Automated Deduction (CADE-18), Copenhagen, Denmark, July 2002, Lecture Notes in Artificial Intelligence, vol. 2392 (2002), Springer), 134-138 · Zbl 1072.68578 |
| [23] | C. Hurlin, Proof reconstruction for first-order logic and set-theoretical constructions, in: S. Merz, T. Nipkow (Eds.), Sixth International Workshop on Automated Verification of Critical Systems (AVOCS ’06)—Preliminary Proceedings, 2006, pp. 157-162; C. Hurlin, Proof reconstruction for first-order logic and set-theoretical constructions, in: S. Merz, T. Nipkow (Eds.), Sixth International Workshop on Automated Verification of Critical Systems (AVOCS ’06)—Preliminary Proceedings, 2006, pp. 157-162 |
| [24] | Kumar, R.; Kropf, T.; Schneider, K., Integrating a first-order automatic prover in the HOL environment, (Archer, M.; Joyce, J. J.; Levitt, K. N.; Windley, P. J., Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications. Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and its Applications, Davis, California, USA, August 1991 (1992), IEEE Computer Society Press), 170-176 |
| [25] | McLaughlin, S.; Barrett, C.; Ge, Y., Cooperating theorem provers: A case study combining CVC Lite and HOL Light, (Armando, A.; Cimatti, A., PDPAR. PDPAR, Electronic Notes in Theoretical Computer Science, vol. 144 (2005), Springer), 43-51 · Zbl 1272.68362 |
| [26] | Meier, A., TRAMP: Transformation of machine-found proofs into natural deduction proofs at the assertion level, (McAllester, D. A., Automated Deduction—CADE-17, 17th International Conference on Automated Deduction, Proceedings. Automated Deduction—CADE-17, 17th International Conference on Automated Deduction, Proceedings, Pittsburgh, PA, USA, June 17-20, 2000. Automated Deduction—CADE-17, 17th International Conference on Automated Deduction, Proceedings. Automated Deduction—CADE-17, 17th International Conference on Automated Deduction, Proceedings, Pittsburgh, PA, USA, June 17-20, 2000, Lecture Notes in Artificial Intelligence, vol. 1831 (2000), Springer), 460-464 · Zbl 0963.68537 |
| [27] | J. Meng, Integration of interactive and automatic provers, in: M. Carro, J. Correas (Eds.), Second CologNet Workshop on Implementation Technology for Computational Logic Systems, FME 2003, September 2003; J. Meng, Integration of interactive and automatic provers, in: M. Carro, J. Correas (Eds.), Second CologNet Workshop on Implementation Technology for Computational Logic Systems, FME 2003, September 2003 |
| [28] | M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, S. Malik, Chaff: Engineering an efficient SAT solver, in: Proceedings of the 38th Design Automation Conference, Las Vegas, June 2001; M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, S. Malik, Chaff: Engineering an efficient SAT solver, in: Proceedings of the 38th Design Automation Conference, Las Vegas, June 2001 |
| [29] | Meng, J.; Paulson, L. C., Experiments on supporting interactive proof using resolution, (Basin, D.; Rusinowitch, M., Automated Reasoning: Second International Joint Conference, IJCAR 2004, Proceedings. Automated Reasoning: Second International Joint Conference, IJCAR 2004, Proceedings, Cork, Ireland, July 4-8, 2004. Automated Reasoning: Second International Joint Conference, IJCAR 2004, Proceedings. Automated Reasoning: Second International Joint Conference, IJCAR 2004, Proceedings, Cork, Ireland, July 4-8, 2004, Lecture Notes in Artificial Intelligence, vol. 3097 (2004), Springer), 372-384 · Zbl 1126.68574 |
| [30] | J. Meng, L.C. Paulson, Translating higher-order problems to first-order clauses, in: G. Sutcliffe, R. Schmidt, S. Schulz (Eds.), ESCoR: Empirically Successful Computerized Reasoning, CEUR Workshop Proceedings, vol. 192, 2006, pp. 70-80; J. Meng, L.C. Paulson, Translating higher-order problems to first-order clauses, in: G. Sutcliffe, R. Schmidt, S. Schulz (Eds.), ESCoR: Empirically Successful Computerized Reasoning, CEUR Workshop Proceedings, vol. 192, 2006, pp. 70-80 |
| [31] | Meier, A.; Sorge, V., Applying SAT solving in classification of finite algebras, Journal of Automated Reasoning, 35, 1-3, 201-235 (2005) · Zbl 1109.68103 |
| [32] | Milner, R.; Tofte, M.; Harper, R.; MacQueen, D., The Definition of Standard ML—Revised (1997), MIT Press: MIT Press May |
| [33] | Nipkow, T.; Paulson, L. C.; Wenzel, M., Isabelle/HOL—A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol. 2283 (2002), Springer · Zbl 0994.68131 |
| [34] | Nonnengart, A.; Rock, G.; Weidenbach, C., On generating small clause normal forms, (Kirchner, C.; Kirchner, H., Automated Deduction—CADE-15, 15th International Conference on Automated Deduction, Proceedings. Automated Deduction—CADE-15, 15th International Conference on Automated Deduction, Proceedings, Lindau, Germany, July 5-10, 1998. Automated Deduction—CADE-15, 15th International Conference on Automated Deduction, Proceedings. Automated Deduction—CADE-15, 15th International Conference on Automated Deduction, Proceedings, Lindau, Germany, July 5-10, 1998, Lecture Notes in Computer Science, vol. 1421 (1998), Springer), 397-411 · Zbl 0924.03023 |
| [35] | Owre, S.; Rushby, J. M.; Shankar, N., PVS: A prototype verification system, (Kapur, D., 11th International Conference on Automated Deduction (CADE). 11th International Conference on Automated Deduction (CADE), Saratoga, NY, June 1992. 11th International Conference on Automated Deduction (CADE). 11th International Conference on Automated Deduction (CADE), Saratoga, NY, June 1992, Lecture Notes in Artificial Intelligence, vol. 607 (1992), Springer), 748-752 |
| [36] | Paulson, L. C., Isabelle: A Generic Theorem Prover, Lecture Notes in Computer Science, vol. 828 (1994), Springer · Zbl 0825.68059 |
| [37] | Reeber, E.; Hunt, W. A., A SAT-based decision procedure for the subclass of unrollable list formulas in ACL2 (SULFA), (Furbach, U.; Shankar, N., Automated Reasoning—Third International Joint Conference, IJCAR 2006, Proceedings. Automated Reasoning—Third International Joint Conference, IJCAR 2006, Proceedings, Seattle, WA, USA, August 2006. Automated Reasoning—Third International Joint Conference, IJCAR 2006, Proceedings. Automated Reasoning—Third International Joint Conference, IJCAR 2006, Proceedings, Seattle, WA, USA, August 2006, Lecture Notes in Artificial Intelligence, vol. 4130 (2006), Springer), 453-467 · Zbl 1222.68372 |
| [38] | Shankar, N., Using decision procedures with a higher-order logic, (Boulton, R. J.; Jackson, P. B., Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Proceedings. Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Proceedings, Edinburgh, Scotland, UK, September 3-6, 2001. Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Proceedings. Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Proceedings, Edinburgh, Scotland, UK, September 3-6, 2001, Lecture Notes in Computer Science, vol. 2152 (2001), Springer), 5-26 · Zbl 1005.68543 |
| [39] | Strichman, O., On solving Presburger and linear arithmetic with SAT, (Aagaard, M. D.; O’Leary, J. W., Formal Methods in Computer-Aided Design: 4th International Conference, FMCAD 2002, Proceedings. Formal Methods in Computer-Aided Design: 4th International Conference, FMCAD 2002, Proceedings, Portland, OR, USA, November 6-8, 2002. Formal Methods in Computer-Aided Design: 4th International Conference, FMCAD 2002, Proceedings. Formal Methods in Computer-Aided Design: 4th International Conference, FMCAD 2002, Proceedings, Portland, OR, USA, November 6-8, 2002, Lecture Notes in Computer Science, vol. 2517 (2002), Springer), 160-169 · Zbl 1019.68592 |
| [40] | Tseitin, G. S., On the complexity of derivation in propositional calculus, (Siekmann, J.; Wrightson, G., Automation of Reasoning: Classical Papers on Computational Logic, vol. II, 1967-1970 (1983), Springer). (Slisenko, A. O., Structures in Constructive Mathematics and Mathematical Logic, Part II (1968)), 115-125, Also · Zbl 0205.00402 |
| [41] | T. Weber, Integrating a SAT solver with an LCF-style theorem prover, in: A. Armando, A. Cimatti (Eds.), Proceedings of PDPAR’05—Third International Workshop on Pragmatical Aspects of Decision Procedures in Automated Reasoning, Edinburgh, UK, July 2005; T. Weber, Integrating a SAT solver with an LCF-style theorem prover, in: A. Armando, A. Cimatti (Eds.), Proceedings of PDPAR’05—Third International Workshop on Pragmatical Aspects of Decision Procedures in Automated Reasoning, Edinburgh, UK, July 2005 · Zbl 1272.68366 |
| [42] | T. Weber, Using a SAT solver as a fast decision procedure for propositional logic in an LCF-style theorem prover, in: J. Hurd, E. Smith, A. Darbari (Eds.), Theorem Proving in Higher Order Logics—18th International Conference, TPHOLs 2005, Oxford, UK, August 2005, Emerging Trends Proceedings, Oxford, UK, August 2005, pp. 180-189; Oxford University Computing Laboratory, Programming Research Group, Research Report PRG-RR-05-02; T. Weber, Using a SAT solver as a fast decision procedure for propositional logic in an LCF-style theorem prover, in: J. Hurd, E. Smith, A. Darbari (Eds.), Theorem Proving in Higher Order Logics—18th International Conference, TPHOLs 2005, Oxford, UK, August 2005, Emerging Trends Proceedings, Oxford, UK, August 2005, pp. 180-189; Oxford University Computing Laboratory, Programming Research Group, Research Report PRG-RR-05-02 |
| [43] | Zhang, L., On subsumption removal and on-the-fly CNF simplification, (Bacchus, F.; Walsh, T., SAT. SAT, Lecture Notes in Computer Science, vol. 3569 (2005), Springer), 482-489 · Zbl 1128.68488 |
| [44] | Zhang, L.; Malik, S., Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications, (Design, Automation and Test in Europe (DATE 2003) (2003), IEEE Computer Society), 10880-10885 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
