Article

Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications

Authors:

Sharad MalikAuthors Info & Claims

DATE '03: Proceedings of the conference on Design, Automation and Test in Europe - Volume 1

Page 10880

Published: 03 March 2003 Publication History

Abstract

As the use of SAT solvers as core engines in EDA applications grows, it becomes increasingly important to validate their correctness. In this paper, we describe the implementation of an independent resolution-based checking procedure that can check the validity of unsatisfiable claims produced by the SAT solver zchaff. We examine the practical implementation issues of such a checker and describe two implementations with different pros and cons. Experimental results show low overhead for the checking process. Our checker can work with many other modern SAT solvers with minor modifications, and it can provide information for debugging when checking fails. Finally we describe additional results that can be obtained by the validation process and briefly discuss their applications.

References

[1]

{1} M. Velev, and R. Bryant, Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors, Proc. of the Design Automation Conference, 2001.

Digital Library

[2]

{2} A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic Model Checking without BDDs, Tools and Algorithms for the Analysis and Construction of Systems (TACAS), 1999

Digital Library

[3]

{3} G.-J. Nam, K. A. Sakallah, and R. A. Rutenbar, Satisfiability-Based Layout Revisited: Detailed Routing of Complex FPGAs Via Search-Based Boolean SAT, Proc. of Int'l Symposium on Field-Programmable Gate Arrays (FPGA'99), Monterey, California, 1999.

Digital Library

[4]

{4} J. P. Marques-Silva and K. A. Sakallah, GRASP: A Search Algorithm for Propositional Satisfiability, IEEE Transactions on Computers, vol. 48, 506-521, 1999.

Digital Library

[5]

{5} C. P. Gomes, B. Selman, and H. Kautz, Boosting Combinatorial Search Through Randomization, Proc. of AAAI-98, Madison, WI, 1998.

Digital Library

[6]

{6} M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT Solver, Proc. of the Design Automation Conference, July 2001.

Digital Library

[7]

{7} F. Copty, L. Fix, R. Fraer, E. Giunchiglia, G. Kamhi, A. Tacchella and M.Y. Vardi, Benefits of Bounded Model Checking at an Industrial Setting, Proc. 13th Conf. on Computer Aided Verification, 2001

Digital Library

[8]

{8} M. Davis and H. Putnam, A computing procedure for quantification theory, Journal of the ACM, vol. 7, pp. 201- 215, 1960.

Digital Library

[9]

{9} M. Davis, G. Logemann, and D. Loveland, A machine program for theorem proving, Communications of ACM, vol. 5, pp. 394-397, 1962.

Digital Library

[10]

{10} A. Stump and D. Dill, Faster Proof Checking in the Edinburgh Logical Framework, Proc. 18th International Conference on Automated Deduction (CADE-18), 2002

Digital Library

[11]

{11} K. Namjoshi, Certifying Model Checkers, Proc. 13th Conf. on Computer Aided Verification, 2001

Digital Library

[12]

{12} J. Harrison, Stålmarck's algorithm as a HOL Derived Rule, Proc. International Conf. on Theorem Proving in Higher Order Logics, 1996

Digital Library

[13]

{13} A. Van Gelder. Extracting (easily) checkable proofs from a satisfiability solver that employs both preorder and postorder resolution, 7th Int'l Symposium on AI and Mathematics, 2002

[14]

{14} E. Goldberg and Y. Novikov, BerkMin: a Fast and Robust SAT-Solver, Proc. of Design Automation & Test in Europe, 2002

Digital Library

[15]

{15} SAT 2002 Solver Competition results are available at http://www.satlive.org/SATCompetition/index.jsp

[16]

{16} R. Bruni and A. Sassano, Restoring Satisfiability or Maintaining Unsatisfiability by finding small Unsatisfiable Subformulae, Proc. of Theory and Applications of Satisfiability Testing (SAT2001), 2001

[17]

{17} Daniel Jackson, Alloy: A Lightweight Object Modelling Notation, ACM Transactions on Software Engineering and Methodology. April 2002, Vol. 11, No. 2.1

Digital Library

[18]

{18} A. Buchsbaum, M. Goldwasser, S. Venkatasubramanian and J. Westbrook, On External Memory Graph Traversal, 11th ACM-SIAM Symposium on Discrete Algorithms, January 2000

Digital Library

Cited By

Bryant RHeule M(2023)Generating Extended Resolution Proofs with a BDD-Based SAT SolverACM Transactions on Computational Logic10.1145/359529524:4(1-28)Online publication date: 25-Jul-2023
https://dl.acm.org/doi/10.1145/3595295
Borralleras CLarraz DRodríguez-Carbonell EOliveras ARubio A(2019)Incomplete SMT Techniques for Solving Non-Linear Formulas over the IntegersACM Transactions on Computational Logic10.1145/334092320:4(1-36)Online publication date: 17-Aug-2019
https://dl.acm.org/doi/10.1145/3340923
Bonacina MGraham-Lengrand SShankar NAndronick JFelty A(2018)Proofs in conflict-driven theory combinationProceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3167096(186-200)Online publication date: 8-Jan-2018
https://dl.acm.org/doi/10.1145/3167096
Show More Cited By

Index Terms

Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications
1. Hardware

Recommendations

A decision-making procedure for resolution-based SAT-solvers
SAT'08: Proceedings of the 11th international conference on Theory and applications of satisfiability testing

We describe a new decision-making procedure for resolutionbased SAT-solvers called Decision Making with a Reference Point (DMRP). In DMRP, a complete assignment called a reference point is maintained. DMRP is aimed at finding a change of the reference ...
Bounded model checking of software using SMT solvers instead of SAT solvers
SPIN'06: Proceedings of the 13th international conference on Model Checking Software

C Bounded Model Checking (CBMC) has proven to be a successful approach to automatic software analysis. The key idea is to (i) build a propositional formula whose models correspond to program traces (of bounded length) that violate some given property ...
On the power of clause-learning SAT solvers as resolution engines

In this work, we improve on existing results on the relationship between proof systems obtained from conflict-driven clause-learning SAT solvers and general resolution. Previous contributions such as those by Beame et al. (2004), Hertel et al. (2008), ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

DATE '03: Proceedings of the conference on Design, Automation and Test in Europe - Volume 1

March 2003

1112 pages

ISBN:0769518702

Sponsors

SIGDA: ACM Special Interest Group on Design Automation

Publisher

IEEE Computer Society

United States

Publication History

Published: 03 March 2003

Check for updates

Qualifiers

Article

Conference

DATE03

Sponsor:

SIGDA

DATE03: Design, Automation, and Test in Europe 2003

March 3 - 7, 2003

Acceptance Rates

Overall Acceptance Rate 518 of 1,794 submissions, 29%

Upcoming Conference

DATE '25

Sponsor:
sigda

Design, Automation and Test in Europe

March 31 - April 2, 2025

Lyon , France

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

87
Total Citations
View Citations
261
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Bryant RHeule M(2023)Generating Extended Resolution Proofs with a BDD-Based SAT SolverACM Transactions on Computational Logic10.1145/359529524:4(1-28)Online publication date: 25-Jul-2023
https://dl.acm.org/doi/10.1145/3595295
Borralleras CLarraz DRodríguez-Carbonell EOliveras ARubio A(2019)Incomplete SMT Techniques for Solving Non-Linear Formulas over the IntegersACM Transactions on Computational Logic10.1145/334092320:4(1-36)Online publication date: 17-Aug-2019
https://dl.acm.org/doi/10.1145/3340923
Bonacina MGraham-Lengrand SShankar NAndronick JFelty A(2018)Proofs in conflict-driven theory combinationProceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3167096(186-200)Online publication date: 8-Jan-2018
https://dl.acm.org/doi/10.1145/3167096
Cruz-Filipe LMarques-Silva JSchneider-Kamp P(2017)Efficient Certified Resolution Proof CheckingProceedings, Part I, of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems - Volume 1020510.1007/978-3-662-54577-5_7(118-135)Online publication date: 22-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54577-5_7
Cabodi GCamurati PPalena MPasini PVendraminetto DPiskac RTalupur M(2016)Reducing interpolant circuit size by ad-hoc logic synthesis and SAT-based weakeningProceedings of the 16th Conference on Formal Methods in Computer-Aided Design10.5555/3077629.3077640(25-32)Online publication date: 3-Oct-2016
https://dl.acm.org/doi/10.5555/3077629.3077640
Schuppan V(2016)Enhancing unsatisfiable cores for LTL with information on temporal relevanceTheoretical Computer Science10.1016/j.tcs.2016.01.014655:PB(155-192)Online publication date: 6-Dec-2016
https://dl.acm.org/doi/10.1016/j.tcs.2016.01.014
Janota MMarques-Silva J(2015)Solving QBF by clause selectionProceedings of the 24th International Conference on Artificial Intelligence10.5555/2832249.2832294(325-331)Online publication date: 25-Jul-2015
https://dl.acm.org/doi/10.5555/2832249.2832294
Yi QYang ZLiu JZhao CWang C(2015)Explaining Software Failures by Cascade Fault LocalizationACM Transactions on Design Automation of Electronic Systems10.1145/273803820:3(1-28)Online publication date: 24-Jun-2015
https://dl.acm.org/doi/10.1145/2738038
Heule MBiere A(2015)Compositional Propositional ProofsProceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning - Volume 945010.1007/978-3-662-48899-7_31(444-459)Online publication date: 24-Nov-2015
https://dl.acm.org/doi/10.1007/978-3-662-48899-7_31
Scholl CPigorsch FDisch SAlthaus EFettweis GNebel W(2014)Simple interpolants for linear arithmeticProceedings of the conference on Design, Automation & Test in Europe10.5555/2616606.2616747(1-6)Online publication date: 24-Mar-2014
https://dl.acm.org/doi/10.5555/2616606.2616747
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten