Article

SATIRE: a new incremental satisfiability engine

Authors:

Jesse Whittemore,

Karem SakallahAuthors Info & Claims

DAC '01: Proceedings of the 38th annual Design Automation Conference

Pages 542 - 545

https://doi.org/10.1145/378239.379019

Published: 22 June 2001 Publication History

Abstract

We introduce SATIRE, a new satisfiability solver that is particular-ly suited to verification and optimization problems in electronic de-sign automation. SATIRE builds on the most recent advances in satisfiability research, and includes two new features to achieve even higher performance: a facility for incrementally solving sets of related problems, and the ability to handle non-CNF constraints. We provide experimental evidence showing the effectiveness of these additions to classical satisfiability solvers.

References

[1]

P. Barth, "A Davis-Putnam based Enumeration Algorithm for Linear Pseudo-Boolean Optimization," Technical Report MPI-I-95-2-003,Max-Planck-Institut Fur Informatik,1995.

[2]

H. Bennaceur, I. Gouachi and G. Plateau, "An Incremental Branch-and-Bound Method for the Satisfiability Problem," INFORMS Journal on Computing,vol.10,pp.301-308, 1998.

Digital Library

[3]

Biere,. Cimmati, E. Clarke,M.Fujita,and Y.Zhu, "Symbolic Model Checking using S T Procedures instead of BDDs,"Design Automation Confer nc (DAC),pp.317- 320,1999.

Digital Library

[4]

E.Clarke,E.Emerson,and .Sistla,"Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic," ACM Transactions on Programming Languages and Systems,pp.244-263,1986.

Digital Library

[5]

O.Coudert and J.C.Madre,"New Ideas for Solving Covering Problems,"Design Automation Confer nc (DAC),pp. 641-646,1995.

Digital Library

[6]

O.Coudert,"On Solving Covering Problems," Design Automation Confer nc (DAC),pp.197-202,1996.

Digital Library

[7]

M.Davis,G.Logemann,and D.Loveland," A Machine Program for Theorem Proving,"Communications of the ACM,vol.5,pp.394-397,1962.

Digital Library

[8]

J.F.Groote and J.P.Warners,'The Propositional Formula Checker HeerHugo,"Technical Report SEN-R9905 (CWI), 1999.

Digital Library

[9]

J.N.Hooker,"Solving the Incremental Satisfiability Problem," Journal of Logic Programming,vol.15,pp.177-186, 1993.

Digital Library

[10]

J. Kim, J. Whittemore, J. P.M. Silva and K.A. Sakallah, "On Application of Incremental Satisfiability to Delay Fault Testing," Design,Automation and T st in Europe (DATE), pp.380-384,2000.

Digital Library

[11]

J.Kim,J.Whittemore,J.P.M.Silva and K.A.Sakallah, "On Solving Stack-Based Incremental Satisfiability Problems," Int rnational Conf rence on Comput r Design (ICCD),pp.379-382,2000.

Digital Library

[12]

W.Kunz and D.Stoffel,Reasoning in Boolean Networks, Kluwer cademic Publishers,1997.

Digital Library

[13]

PCI Special Interest Group,"PCI Local Bus Specification," Revision 2.2,December 1995.

[14]

I.Pomeranz,S.M.Reddy,"Functional Delay Faults in Macro-based Combinational Circuits," International Conference on Comput r-Aided Design (ICCAD),pp.687-694, 1995.

Digital Library

[15]

M.Sheeran and G.Stalmarck,"A Tutorial on Stalmarck 's Proof Procedure for Propositional Logic," Proceedings of Formal Methods in Computer-Aid d D sign (FMCAD),pp. 82-99,1998.

Digital Library

[16]

K. Shimizu, D. Dill, and A. Hu, Monitor-Based Formal Specification of PCI," Proceedings of Formal Methods in Comput r-Aided Design (FMCAD),pp.335-353,2000.

Digital Library

[17]

J.P. Marques-Silva,and K.A.Sakallah,"GRASP: Search Algorithm for Propositional Satisfiability," IEEE Transactions on Computers,vol.48,no.5,pp.506-521, May 1999.

Digital Library

[18]

G. Stalmarck," System for determining propositional logic theorems by applying values and rules to triplets that are generated from boolean formula," Swedish Patent No. 467,076 (approved 1992),U.S.Patent No.5,276,897 (approved 1994),European Patent No.0403 454 (approved 1995).

[19]

S.Tragoudas and M.Michael,"ATPG tools for Delay Faults at the Functional Level," Design,Automation and Test in Europ (DATE),pp.631-635,1999.

Digital Library

[20]

H. Zhang, "S TO:An Efficient Propositional Prover,"in Proceedings of International Conference on Automated Deductio n,pp.272-275, July 1997.

Digital Library

Cited By

Biere AFaller TFazekas KFleury MFroleyks NPollitt F(2024)CaDiCaL 2.0Computer Aided Verification10.1007/978-3-031-65627-9_7(133-152)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65627-9_7
Reeves JHeule MBryant R(2024)From Clauses to KlausesComputer Aided Verification10.1007/978-3-031-65627-9_6(110-132)Online publication date: 26-Jul-2024
https://doi.org/10.1007/978-3-031-65627-9_6
Young JBittner PWalkingshaw EThüm T(2023)Variational satisfiability solving: efficiently solving lots of related SAT problemsEmpirical Software Engineering10.1007/s10664-022-10217-328:1Online publication date: 1-Jan-2023
https://dl.acm.org/doi/10.1007/s10664-022-10217-3
Show More Cited By

Index Terms

SATIRE: a new incremental satisfiability engine

Recommendations

On stateless multihead automata: Hierarchies and the emptiness problem

We look at stateless multihead finite automata in their two-way and one-way, deterministic and nondeterministic variations. The transition of a k-head automaton depends solely on the symbols currently scanned by its k heads, and every such transition ...
Pebble alternating tree-walking automata and their recognizing power

Pebble tree-walking automata with alternation were first investigated by Milo, Suciu and Vianu (2003), who showed that tree languages recognized by these devices are exactly the regular tree languages. We strengthen this by proving the same result for ...
Lower Bounds on Witnesses for Nonemptiness of Universal Co-Büchi Automata
Proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures - Volume 5504

The nonemptiness problem for nondeterministic automata on infinite words can be reduced to a sequence of reachability queries. The length of a shortest witness to the nonemptiness is then polynomial in the automaton. Nonemptiness algorithms for ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

DAC '01: Proceedings of the 38th annual Design Automation Conference

June 2001

863 pages

ISBN:1581132972

DOI:10.1145/378239

Chairman:
Jan Rabaey
Univ. of California

Copyright © 2001 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

EDAC: Electronic Design Automation Consortium
SIGDA: ACM Special Interest Group on Design Automation
IEEE-CAS: Circuits & Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 22 June 2001

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

DAC01

Sponsor:

EDAC
SIGDA
IEEE-CAS

DAC01: 38th ACM/IEEE-CAS/ EDAC Design Automation Conference

Nevada, Las Vegas, USA

Acceptance Rates

Overall Acceptance Rate 1,770 of 5,499 submissions, 32%

Upcoming Conference

DAC '25

Sponsor:
sigda

62nd ACM/IEEE Design Automation Conference

June 22 - 26, 2025

San Francisco , CA , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

111
Total Citations
View Citations
63
Total Downloads

Downloads (Last 12 months)13
Downloads (Last 6 weeks)2

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Biere AFaller TFazekas KFleury MFroleyks NPollitt F(2024)CaDiCaL 2.0Computer Aided Verification10.1007/978-3-031-65627-9_7(133-152)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65627-9_7
Reeves JHeule MBryant R(2024)From Clauses to KlausesComputer Aided Verification10.1007/978-3-031-65627-9_6(110-132)Online publication date: 26-Jul-2024
https://doi.org/10.1007/978-3-031-65627-9_6
Young JBittner PWalkingshaw EThüm T(2023)Variational satisfiability solving: efficiently solving lots of related SAT problemsEmpirical Software Engineering10.1007/s10664-022-10217-328:1Online publication date: 1-Jan-2023
https://dl.acm.org/doi/10.1007/s10664-022-10217-3
Lyu YMishra P(2021)Scalable Concolic Testing of RTL ModelsIEEE Transactions on Computers10.1109/TC.2020.299764470:7(979-991)Online publication date: 1-Jul-2021
https://doi.org/10.1109/TC.2020.2997644
Le Berre DWallon R(2021)On Dedicated CDCL Strategies for PB SolversTheory and Applications of Satisfiability Testing – SAT 202110.1007/978-3-030-80223-3_22(315-331)Online publication date: 2-Jul-2021
https://doi.org/10.1007/978-3-030-80223-3_22
Karpiński MPiotrów M(2020)Incremental Encoding of Pseudo-Boolean Goal Functions Based on Comparator NetworksTheory and Applications of Satisfiability Testing – SAT 202010.1007/978-3-030-51825-7_36(519-535)Online publication date: 26-Jun-2020
https://doi.org/10.1007/978-3-030-51825-7_36
Le Berre DMarquis PWallon R(2020)On Weakening Strategies for PB SolversTheory and Applications of Satisfiability Testing – SAT 202010.1007/978-3-030-51825-7_23(322-331)Online publication date: 26-Jun-2020
https://doi.org/10.1007/978-3-030-51825-7_23
Sumners R(2018)Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its ApplicationsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.280.7280(95-97)Online publication date: 29-Oct-2018
https://doi.org/10.4204/EPTCS.280.7
Veira NPoulos ZVeneris A(2018)Suspect set prediction in RTL bug hunting2018 Design, Automation & Test in Europe Conference & Exhibition (DATE)10.23919/DATE.2018.8342261(1544-1549)Online publication date: Mar-2018
https://doi.org/10.23919/DATE.2018.8342261
Schrammel PKroening DBrain MMartins RTeige TBienmüller T(2017)Incremental bounded model checking for embedded softwareFormal Aspects of Computing10.1007/s00165-017-0419-129:5(911-931)Online publication date: 1-Sep-2017
https://dl.acm.org/doi/10.1007/s00165-017-0419-1
Show More Cited By

View Options

Get Access

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.

Media

Figures

Other

Tables

View Table of Contents