|
 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
Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked 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
|
|
 |
3
|
A. Biere , A. Cimatti , E. M. Clarke , M. Fujita , Y. Zhu, Symbolic model checking using SAT procedures instead of BDDs, Proceedings of the 36th ACM/IEEE conference on Design automation, p.317-320, June 21-25, 1999, New Orleans, Louisiana, United States
[doi> 10.1145/309847.309942]
|
| |
4
|
|
| |
5
|
|
| |
6
|
|
| |
7
|
|
| |
8
|
|
| |
9
|
|
| |
10
|
Joonyoung Kim , Jesse Whittemore , João P. Marques-Silva , Karem Sakallah, On applying incremental satisfiability to delay fault testing, Proceedings of the conference on Design, automation and test in Europe, p.380-384, March 27-30, 2000, Paris, France
[doi> 10.1145/343647.343801]
|
| |
11
|
|
| |
12
|
W.Kunz and D.Stoffel,Reasoning in Boolean Networks , Kluwer cademic Publishers,1997.
|
| |
13
|
PCI Special Interest Group,"PCI Local Bus Specification," Revision 2.2,December 1995.
|
| |
14
|
|
| |
15
|
|
| |
16
|
|
| |
17
|
|
| |
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
|
|
| |
20
|
|
CITED BY 24
|
|
|
|
|
|
|
|
Fadi A. Aloul , Arathi Ramani , Igor L. Markov , Karem A. Sakallah, Generic ILP versus specialized 0-1 ILP: an update, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, p.450-457, November 10-14, 2002, San Jose, California
|
|
|
|
|
|
Yoonna Oh , Maher N. Mneimneh , Zaher S. Andraus , Karem A. Sakallah , Igor L. Markov, AMUSE: a minimally-unsatisfiable subformula extractor, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA
|
|
|
Chao Wang , HoonSang Jin , Gary D. Hachtel , Fabio Somenzi, Refining the SAT decision ordering for bounded model checking, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA
|
|
|
Afshin Abdollahi , Massoud Pedram , Farzan Fallah, Runtime mechanisms for leakage current reduction in CMOS VLSI circuits1,2, Proceedings of the 2002 international symposium on Low power electronics and design, August 12-14, 2002, Monterey, California, USA
|
|
|
|
|
|
Görschwin Fey , Sean Safarpour , Andreas Veneris , Rolf Drechsler, On the relation between simulation-based and SAT-based diagnosis, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Andre Suelflow , Goerschwin Fey , Roderick Bloem , Rolf Drechsler, Using unsatisfiable cores to debug multiple design errors, Proceedings of the 18th ACM Great Lakes symposium on VLSI, May 04-06, 2008, Orlando, Florida, USA
|
|
|
|
|
|
|
|
|
|
|
Adobe Acrobat
QuickTime
Windows Media Player
Real Player
Pdf
F.2