ACM Portal
  Subscribe (Full Service)    Register (Limited Service, Free)    Login
  Search:   The ACM Digital Library   The Guide
  
ACM Home Page
Please provide us with feedback. Feedback
Chaff: engineering an efficient SAT solver
Full text PdfPdf (196 KB)
Source Annual ACM IEEE Design Automation Conference archive
Proceedings of the 38th annual Design Automation Conference table of contents
Las Vegas, Nevada, United States
Pages: 530 - 535  
Year of Publication: 2001
ISBN:1-58113-297-2
Authors
Matthew W. Moskewicz  Department of EECS, UC Berkeley
Conor F. Madigan  Department of EECS, MIT
Ying Zhao  Department of Electrical Engineering, Princeton University
Lintao Zhang  Department of Electrical Engineering, Princeton University
Sharad Malik  Department of Electrical Engineering, Princeton University
Sponsors
EDAC : Electronic Design Automation Consortium
IEEE-CAS : Circuits & Systems
SIGDA: ACM Special Interest Group on Design Automation
Publisher
ACM  New York, NY, USA
Bibliometrics
Downloads (6 Weeks): 42,   Downloads (12 Months): 125,   Citation Count: 401
Additional Information:

abstract   references   cited by   index terms   collaborative colleagues  

Tools and Actions: Request Permissions Request Permissions    Review this Article  
DOI Bookmark: Use this link to bookmark this Article: http://doi.acm.org/10.1145/378239.379017
What is a DOI?

ABSTRACT

Boolean Satisfiability is probably the most studied of combinatorial optimization/search problems. Significant effort has been devoted to trying to provide practical solutions to this problem for problem instances encountered in a range of applications in Electronic Design Automation (EDA), as well as in Artificial Intelligence (AI). This study has culminated in the development of several SAT packages, both proprietary and in the public domain (e.g. GRASP, SATO) which find significant use in both research and industry. Most existing complete solvers are variants of the Davis-Putnam (DP) search algorithm. In this paper we describe the development of a new complete solver, Chaff, which achieves significant performance gains through careful engineering of all aspects of the search - especially a particularly efficient implementation of Boolean constraint propagation (BCP) and a novel low overhead decision strategy. Chaff has been able to obtain one to two orders of magnitude performance improvement on difficult SAT benchmarks in comparison with other solvers (DP or otherwise), including GRASP and SATO.


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
Luís Baptista , João P. Marques Silva, Using Randomization and Learning to Solve Hard Real-World Instances of Satisfiability, Proceedings of the 6th International Conference on Principles and Practice of Constraint Programming, p.489-494, September 18-21, 2000
 
2
Bayardo, R. and Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances, in Proc. of the 14th Nat. (US) Conf. on Artificial Intelligence (AAAI-97), AAAI Press/The MIT Press, 1997, pp. 203-208.
 
3
Armin Biere , Alessandro Cimatti , Edmund M. Clarke , Yunshan Zhu, Symbolic Model Checking without BDDs, Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, p.193-207, March 22-28, 1999
 
4
DIMACS benchmarks available at ftp://dimacs.rutgers.edu/pub/challenge/sat/benchmarks
 
5
Jon William Freeman, Improvements to propositional satisfiability search algorithms, University of Pennsylvania, Philadelphia, PA, 1995
 
6
Wolfgang Kunz , Dominik Stoffel , Vishwani D. Agrawal , Randal E. Bryant, Reasoning in Boolean Networks: Logic Synthesis and Verification Using Testing Techniques, Kluwer Academic Publishers, Norwell, MA, 1997
 
7
João P. Marques Silva, The Impact of Branching Heuristics in Propositional Satisfiability Algorithms, Proceedings of the 9th Portuguese Conference on Artificial Intelligence: Progress in Artificial Intelligence, p.62-74, September 21-24, 1999
 
8
João P. Marques-Silva , Karem A. Sakallah, GRASP: A Search Algorithm for Propositional Satisfiability, IEEE Transactions on Computers, v.48 n.5, p.506-521, May 1999  [doi>10.1109/12.769433]
 
9
McAllester, D., Selman, B. and Kautz, H.: Evidence for invariants in local search, in Proceedings of AAAI'97, MIT Press, 1997, pp. 321-326.
 
10
Stephan, P., Brayton, R., and Sangiovanni-Vencentelli, A., "Combinational Test Generation Using Satisfiability," IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 15, 1167-1176, 1996.
 
11
Velev, M., FVP-UNSAT.1.0, FVP-UNSAT.2.0, VLIW- SAT. 1.0, SSS-SAT.1.0, Superscalar Suite 1.0, Superscalar Suite 1.0a, Available from: http://www.ece.cmu.edu/mvelev
12
Miroslav N. Velev , Randal E. Bryant, Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW, Proceedings of the 38th conference on Design automation, p.226-231, June 2001, Las Vegas, Nevada, United States  [doi>10.1145/378239.378469]
 
13
Hantao Zhang, SATO: An Efficient Propositional Prover, Proceedings of the 14th International Conference on Automated Deduction, p.272-275, July 13-17, 1997

CITED BY  401
Nikhil Saluja , Kanupriya Gulati , Sunil P Khatri, SAT-based ATPG using multilevel compatible don't-cares, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.13 n.2, p.1-18, April 2008
Fangzhen Lin , Yuting Zhao, ASSAT: computing answer sets of a logic program by SAT solvers, Eighteenth national conference on Artificial intelligence, p.112-117, July 28-August 01, 2002, Edmonton, Alberta, Canada
Slawomir Pilarski , Gracia Hu, SAT with partial clauses and back-leaps, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, ACM SIGPLAN Notices, v.37 n.1, p.58-70, Jan. 2002
Hui Xu , Rob A. Rutenbar , Karem Sakallah, sub-SAT: a formulation for relaxed boolean satisfiability with applications in routing, Proceedings of the 2002 international symposium on Physical design, April 07-10, 2002, San Diego, CA, USA
Fadi A. Aloul , Brian D. Sierawski , Karem A. Sakallah, Satometer:: how much have we searched?, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
Randal E. Bryant , Miroslav N. Velev, Boolean satisfiability with transitivity constraints, ACM Transactions on Computational Logic (TOCL), v.3 n.4, p.604-627, October 2002
Wolfgang Kunz , João Marques-Silva , Sharad Malik, SAT and ATPG: algorithms for Boolean decision problems, Logic Synthesis and Verification, Kluwer Academic Publishers, Norwell, MA, 2001
Edmund Clarke , Daniel Kroening, Hardware verification using ANSI-C programs as a reference, Proceedings of the 2003 conference on Asia South Pacific design automation, January 21-24, 2003, Kitakyushu, Japan
Peter Baumgartner, First-order logic Davis-Putnam-Logemann-Loveland procedure, Exploring artificial intelligence in the new millennium, Morgan Kaufmann Publishers Inc., San Francisco, CA, 2003
Aarti Gupta , Anubhav Gupta , Zijiang Yang , Pranav Ashar, Dynamic detection and removal of inactive clauses in SAT with application in image computation, Proceedings of the 38th conference on Design automation, p.536-541, June 2001, Las Vegas, Nevada, United States
Shuo Sheng , Koichiro Takayama , Michael S. Hsiao, Effective safety property checking using simulation-based sequential ATPG, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
Shin-ichi Minato, Streaming BDD Manipulation, IEEE Transactions on Computers, v.51 n.5, p.474-485, May 2002
Fahiem Bacchus, Enhancing Davis Putnam with extended binary clause reasoning, Eighteenth national conference on Artificial intelligence, p.613-619, July 28-August 01, 2002, Edmonton, Alberta, Canada
Miroslav N. Velev , Randal E. Bryant, Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW, Proceedings of the 38th conference on Design automation, p.226-231, June 2001, Las Vegas, Nevada, United States
Ying Zhao , Sharad Malik , Matthew Moskewicz , Conor Madigan, Accelerating boolean satisfiability through application specific processing, Proceedings of the 14th international symposium on Systems synthesis, September 30-October 03, 2001, Montréal, P.Q., Canada
Alessandro Fin , Franco Fummi , Graziano Pravadelli, Mixing ATPG and property checking for testing HW/SW interfaces, Proceedings of the 13th ACM Great Lakes symposium on VLSI, April 28-29, 2003, Washington, D. C., USA
Malay K. Ganai , Pranav Ashar , Aarti Gupta , Lintao Zhang , Sharad Malik, Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
Henry Kautz , Eric Horvitz , Yongshao Ruan , Carla Gomes , Bart Selman, Dynamic restart policies, Eighteenth national conference on Artificial intelligence, p.674-681, July 28-August 01, 2002, Edmonton, Alberta, Canada
Edmund Clarke , Daniel Kroening , Karen Yorav, Behavioral consistency of C and verilog programs using bounded model checking, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA
Ganapathy Parthasarathy , Madhu K. Iyer , Kwang-Ting (Tim) Cheng , Li-C. Wang, Safety Property Verification Using Sequential SAT and Bounded Model Checking, IEEE Design & Test, v.21 n.2, p.132-143, March 2004
Aarti Gupta , Zijiang Yang , Pranav Ashar , Lintao Zhang , Sharad Malik, Partition-based decision heuristics for image computation using SAT and BDDs, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
Fadi A. Aloul , Igor L. Markov , Karem A. Sakallah, Faster SAT and smaller BDDs via common function structure, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
Wojciech Penczek , Alessio Lomuscio, Verifying epistemic properties of multi-agent systems via bounded model checking, Fundamenta Informaticae, v.55 n.2, p.167-185, May 2003
Alex Fukunaga, Automated discovery of composite SAT variable-selection heuristics, Eighteenth national conference on Artificial intelligence, p.641-648, July 28-August 01, 2002, Edmonton, Alberta, Canada
Sagar Chaki , Edmund Clarke , Alex Groce , Somesh Jha , Helmut Veith, Modular verification of software components in C, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
Wojciech Penczek , Bozena Wozna , Andrzej Zbrzezny, Bounded model checking for the universal fragment of CTL, Fundamenta Informaticae, v.51 n.1, p.135-156, June 2002
Fadi A. Aloul , Igor L. Markov , Karem A. Sakallah, FORCE: a fast and easy-to-implement variable-ordering heuristic, Proceedings of the 13th ACM Great Lakes symposium on VLSI, April 28-29, 2003, Washington, D. C., USA
W. Penczek , A. Lomuscio, Verifying epistemic properties of multi-agent systems via bounded model checking, Proceedings of the second international joint conference on Autonomous agents and multiagent systems, July 14-18, 2003, Melbourne, Australia
Wolfgang Blochinger , Carsten Sinz , Wolfgang Küchlin, Parallel propositional satisfiability checking with distributed dynamic learning, Parallel Computing, v.29 n.7, p.969-994, July 2003
Wolfgang Müller , Wolfgang Rosenstiel , Jürgen Ruf, References, SystemC: methodologies and applications, Kluwer Academic Publishers, Norwell, MA, 2003
Donald Chai , Alex Kondratyev , Yajun Ran , Kenneth H. Tseng , Yosinori Watanabe , Malgorzata Marek-Sadowska, Temporofunctional crosstalk noise analysis, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA
Farzan Fallah, Binary time-frame expansion, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, p.458-464, November 10-14, 2002, San Jose, California
Armin Biere , Wolfgang Kunz, SAT and ATPG: Boolean engines for formal hardware verification, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, p.782-785, November 10-14, 2002, San Jose, California
Heidi E. Dixon , Matthew L. Ginsberg, Inference methods for a pseudo-boolean satisfiability solver, Eighteenth national conference on Artificial intelligence, p.635-640, July 28-August 01, 2002, Edmonton, Alberta, Canada
Aarti Gupta , Malay Ganai , Chao Wang , Zijiang Yang , Pranav Ashar, Learning from BDDs in SAT-based bounded model checking, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA
Donald Chai , Andreas Kuehlmann, A fast pseudo-boolean constraint solver, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA
Hyeong-Ju Kang , In-Cheol Park, SAT-based unbounded symbolic model checking, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA
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
Miroslav N. Velev , Randal E. Bryant, Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors, Journal of Symbolic Computation, v.35 n.2, p.73-106, February 2003
Feng Lu , Li-C. Wang , K.-T. (Tim) Cheng , John Moondanos , Ziyad Hanna, A signal correlation guided ATPG solver and its applications for solving difficult industrial cases, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA
Lintao Zhang , Sharad Malik, Conflict driven learning in a quantified Boolean Satisfiability solver, Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, p.442-449, November 10-14, 2002, San Jose, California
Xiaoyu Song , William N. N. Hung , Alan Mishchenko , Malgorzata Chrzanowska-Jeske , Andrew Kennings , Alan Coppola, Board-level multiterminal net assignment for the partial cross-bar architecture, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, v.11 n.3, p.511-514, June 2003
João Marques-Silva , Luís Guerra e Silva, Solving Satisfiability in Combinational Circuits, IEEE Design & Test, v.20 n.04, p.16-21, January 2003
Edward A. Hirsch, Worst-case study of local search for MAX-k-SAT, Discrete Applied Mathematics, v.130 n.2, p.173-184, 15 August 2003
Steven Prestwich, SAT problems with chains of dependent variables, Discrete Applied Mathematics, v.130 n.2, p.329-350, 15 August 2003
Ilija Hadžić , Jonathan M. Smith, Balancing performance and flexibility with hardware support for network architectures, ACM Transactions on Computer Systems (TOCS), v.21 n.4, p.375-411, November 2003
Chu-Min Li, Equivalent literal propagation in the DLL procedure, Discrete Applied Mathematics, v.130 n.2, p.251-276, 15 August 2003
Thomas Eiter , Wolfgang Faber , Nicola Leone , Gerald Pfeifer , Axel Polleres, A logic programming approach to knowledge-state planning: Semantics and complexity, ACM Transactions on Computational Logic (TOCL), v.5 n.2, p.206-263, April 2004
Iouliia Skliarova , António B. Ferrari, The design and implementation of a reconfigurable processor for problems of combinatorial computation, Journal of Systems Architecture: the EUROMICRO Journal, v.49 n.4-6, p.211-226, September 2003
Enrico Giunchiglia , Massimo Narizzano , Armando Tacchella, Learning for quantified boolean logic satisfiability, Eighteenth national conference on Artificial intelligence, p.649-654, July 28-August 01, 2002, Edmonton, Alberta, Canada
Robert Damiano , James Kukula, Checking satisfiability of a conjunction of BDDs, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA
Fadi A. Aloul , Arathi Ramani , Igor L. Markov , Karem A. Sakallah, ShatterPB: symmetry-breaking for pseudo-Boolean formulas, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.883-886, January 27-30, 2004, Yokohama, Japan
Bozena Woźna , Andrzej Zbrzezny , Wojciech Penczek, Checking reachability properties for timed automata via SAT, Fundamenta Informaticae, v.55 n.2, p.223-241, May 2003
Maher Mneimneh , Karem Sakallah, SAT-based sequential depth computation, Proceedings of the 2003 conference on Asia South Pacific design automation, January 21-24, 2003, Kitakyushu, Japan
Iouliia Skliarova , Antonio de Brito Ferrari, Reconfigurable Hardware SAT Solvers: A Survey of Systems, IEEE Transactions on Computers, v.53 n.11, p.1449-1461, November 2004
G. Parthasarathy , M. K. Iyer , K.-T. Cheng , L.-C. Wang, An efficient finite-domain constraint solver for circuits, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA
Pankaj Chauhan , Edmund M. Clarke , Daniel Kroening, A SAT-based algorithm for reparameterization in symbolic simulation, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA
Ondřej Lhoták , Laurie Hendren, Jedd: a BDD-based relational extension of Java, ACM SIGPLAN Notices, v.39 n.6, May 2004
Tetsuya Iizuka , Makoto Ikeda , Kunihiro Asada, High speed layout synthesis for minimum-width CMOS logic cells via Boolean satisfiability, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.149-154, January 27-30, 2004, Yokohama, Japan
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
Ofer Strichman, Accelerating Bounded Model Checking of Safety Properties, Formal Methods in System Design, v.24 n.1, p.5-24, January 2004
William N. N. Hung , Xiaoyu Song , El Mostapha Aboulhamid , Andrew Kennings , Alan Coppola, Segmented channel routability via satisfiability, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.9 n.4, p.517-528, October 2004
Fadi A. Aloul , Arathi Ramani , Igor L. Markov , Karem A. Sakallah, Dynamic symmetry-breaking for improved Boolean optimization, Proceedings of the 2005 conference on Asia South Pacific design automation, January 18-21, 2005, Shanghai, China
Miroslav N. Velev, Efficient formal verification of pipelined processors with instruction queues, Proceedings of the 14th ACM Great Lakes symposium on VLSI, April 26-28, 2004, Boston, MA, USA
Jonathan Edwards , Daniel Jackson , Emina Torlak , Vincent Yeung, Faster constraint solving with subtypes, ACM SIGSOFT Software Engineering Notes, v.29 n.4, July 2004
Görschwin Fey , Rolf Drechsler, Improving simulation-based verification by means of formal methods, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.640-643, January 27-30, 2004, Yokohama, Japan
Alexander Smith , Andreas Veneris , Anastasios Viglas, Design diagnosis using Boolean satisfiability, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.218-223, January 27-30, 2004, Yokohama, Japan
Ruiming Li , Dian Zhou , Donglei Du, Satisfiability and integer programming as complementary tools, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.879-882, January 27-30, 2004, Yokohama, Japan
Miroslav N. Velev, Efficient translation of boolean formulas to CNF in formal verification of microprocessors, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.310-315, January 27-30, 2004, Yokohama, Japan
Fangzhen Lin , Yuting Zhao, ASSAT: computing answer sets of a logic program by SAT solvers, Artificial Intelligence, v.157 n.1-2, p.115-137, August 2004
G. Parthasarathy , M. K. Iyer , K.-T. Cheng , Li. C. Wang, Efficient reachability checking using sequential SAT, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.418-423, January 27-30, 2004, Yokohama, Japan
Markus Wedler , Dominik Stoffel , Wolfgang Kunz, Exploiting state encoding for invariant generation in induction-based property checking, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.424-429, January 27-30, 2004, Yokohama, Japan
Ilia Polian , Bernd Becker, Scalable Delay Fault BIST for Use with Low-Cost ATE, Journal of Electronic Testing: Theory and Applications, v.20 n.2, p.181-197, April 2004
Lintao Zhang , Conor F. Madigan , Matthew H. Moskewicz , Sharad Malik, Efficient conflict driven learning in a boolean satisfiability solver, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
Sean Safarpour , Görschwin Fey , Andreas Veneris , Rolf Drechsler, Utilizing don't care states in SAT-based bounded sequential problems, Proceedings of the 15th ACM Great Lakes symposium on VLSI, April 17-19, 2005, Chicago, Illinois, USA
Edmund Clarke , Daniel Kroening , Natasha Sharygina , Karen Yorav, Predicate Abstraction of ANSI-C Programs Using SAT, Formal Methods in System Design, v.25 n.2-3, p.105-127, September-November 2004
Iouliia Skliarova , António B. Ferrari, A software/reconfigurable hardware SAT solver, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, v.12 n.4, p.408-419, April 2004
Gi-Joon Nam , Fadi Aloul , Karem A. Sakallah , Rob A. Rutenbar, A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints, IEEE Transactions on Computers, v.53 n.6, p.688-696, June 2004
Yichen Xie , Alex Aiken, Scalable error detection using boolean satisfiability, ACM SIGPLAN Notices, v.40 n.1, p.351-363, January 2005
Shengyu Shen , Ying Qin , SiKun Li, A fast counterexample minimization approach with refutation analysis and incremental SAT, Proceedings of the 2005 conference on Asia South Pacific design automation, January 18-21, 2005, Shanghai, China
Modular Verification of Software Components in C, IEEE Transactions on Software Engineering, v.30 n.6, p.388-402, June 2004
Malay K. Ganai , Aarti Gupta , Pranav Ashar, Beyond safety: customized SAT-based model checking, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, San Diego, California, USA
Vinod Ganapathy , Sanjit A. Seshia , Somesh Jha , Thomas W. Reps , Randal E. Bryant, Automatic discovery of API-level exploits, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA
Marcelo F. Frias , Juan P. Galeotti , Carlos G. López Pombo , Nazareno M. Aguirre, DynAlloy: upgrading alloy with actions, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA
David Detlefs , Greg Nelson , James B. Saxe, Simplify: a theorem prover for program checking, Journal of the ACM (JACM), v.52 n.3, p.365-473, May 2005
Himanshu Jain , Daniel Kroening , Natasha Sharygina , Edmund Clarke, Word level predicate abstraction and refinement for verifying RTL verilog, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, San Diego, California, USA
Ronald P. Lajaunie , Michael S. Hsiao, An effective and efficient ATPG-based combinational equivalence checker, Proceedings of the 15th ACM Great Lakes symposium on VLSI, April 17-19, 2005, Chicago, Illinois, USA
Deborah East , Miroslaw Truszczyński, Predicate-calculus-based logics for modeling and solving search problems, ACM Transactions on Computational Logic (TOCL), v.7 n.1, p.38-83, January 2006
Geoff Sutcliffe , Christian Suttner, The CADE-19 ATP system competition, AI Communications, v.17 n.3, p.103-110, July 2004
Zhao Xing , Weixiong Zhang, MaxSolver: an efficient exact algorithm for (weighted) maximum satisfiability, Artificial Intelligence, v.164 n.1-2, p.47-80, May 2005
Andrew Ling , Deshanand P. Singh , Stephen D. Brown, FPGA technology mapping: a study of optimality, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, San Diego, California, USA
Domagoj Babić , Jesse Bingham , Alan J. Hu, Efficient SAT solving: beyond supercubes, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, San Diego, California, USA
Paul T. Darga , Mark H. Liffiton , Karem A. Sakallah , Igor L. Markov, Exploiting structure in symmetry detection for CNF, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA
Domagoj Babić , Alan J. Hu, Integration of supercubing and learning in a SAT solver, Proceedings of the 2005 conference on Asia South Pacific design automation, January 18-21, 2005, Shanghai, China
Masahiro Fujita, Equivalence checking between behavioral and RTL descriptions with virtual controllers and datapaths, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.10 n.4, p.610-626, October 2005
Shuvendu K. Lahiri , Shaz Qadeer, Verifying properties of well-founded linked lists, ACM SIGPLAN Notices, v.41 n.1, p.115-126, January 2006
Tetsuya Iizuka , Makoto Ikeda , Kunihiro Asada, Exact minimum-width transistor placement without dual constraint for CMOS cells, Proceedings of the 15th ACM Great Lakes symposium on VLSI, April 17-19, 2005, Chicago, Illinois, USA
David Coppit , Jiexin Lian, yagg: an easy-to-use generator for structured test inputs, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA
Zhihong Zeng , Kesava R. Talupuru , Maciej Ciesielski, Functional test generation based on word-level SAT, Journal of Systems Architecture: the EUROMICRO Journal, v.51 n.8, p.488-511, August 2005
K. L. McMillan, An interpolating theorem prover, Theoretical Computer Science, v.345 n.1, p.101-121, 21 November 2005
Yung-Chieh Lin , Feng Lu , Kai Yang , Kwang-Ting Cheng, Constraint extraction for pseudo-functional scan-based delay testing, Proceedings of the 2005 conference on Asia South Pacific design automation, January 18-21, 2005, Shanghai, China
Miroslav N. Velev, Comparison of schemes for encoding unobservability in translation to SAT, Proceedings of the 2005 conference on Asia South Pacific design automation, January 18-21, 2005, Shanghai, China
David Coppit , Jinlin Yang , Sarfraz Khurshid , Wei Le , Kevin Sullivan, Software Assurance by Bounded Exhaustive Testing, IEEE Transactions on Software Engineering, v.31 n.4, p.328-339, April 2005
Sung-Jui (Song-Ra) Pan , Kwang-Ting Cheng , John Moondanos , Ziyad Hanna, Generation of shorter sequences for high resolution error diagnosis using sequential SAT, Proceedings of the 2006 conference on Asia South Pacific design automation, January 24-27, 2006, Yokohama, Japan
Robert K. Brayton, The future of logic synthesis and verification, Logic Synthesis and Verification, Kluwer Academic Publishers, Norwell, MA, 2001
Alexander Nareyek , Eugene C. Freuder , Robert Fourer , Enrico Giunchiglia , Robert P. Goldman , Henry Kautz , Jussi Rintanen , Austin Tate, Constraints and AI Planning, IEEE Intelligent Systems, v.20 n.2, p.62-72, March 2005
Fadi A. Aloul , Igor L. Markov , Karem A. Sakallah, Shatter: efficient symmetry-breaking for boolean satisfiability, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA
Fadi A. Aloul , Arathi Ramani , Igor L. Markov , Karem A. Sakallah, Solving difficult SAT instances in the presence of symmetry, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
Aaron Tomb , Cormac Flanagan, Automatic type inference via partial evaluation, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.106-116, July 11-13, 2005, Lisbon, Portugal
Sebastian Danicic , Mohammed Daoudi , Chris Fox , Mark Harman , Robert M. Hierons , John R. Howroyd , Lahcen Ourabya , Martin Ward, ConSUS: a light-weight program conditioner, Journal of Systems and Software, v.77 n.3, p.241-262, September 2005
Jinbo Huang, MUP: a minimal unsatisfiability prover, Proceedings of the 2005 conference on Asia South Pacific design automation, January 18-21, 2005, Shanghai, China
R. M. Gott , J. R. Baumgartner , P. Roessler , S. I. Joe, Functional formal verification on designs of pSeries microprocessors and communication subsystems, IBM Journal of Research and Development, v.49 n.4/5, p.565-580, July 2005
Kevin Sullivan , Jinlin Yang , David Coppit , Sarfraz Khurshid , Daniel Jackson, Software assurance by bounded exhaustive testing, ACM SIGSOFT Software Engineering Notes, v.29 n.4, July 2004
Michal Kouril , Jerome L. Paul, A parallel backtracking framework (BkFr) for single and multiple clusters, Proceedings of the 1st conference on Computing frontiers, April 14-16, 2004, Ischia, Italy
HoonSang Jin , Fabio Somenzi, Strong conflict analysis for propositional satisfiability, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
Jörg Hoffmann , Ronen I. Brafman, Conformant planning via heuristic forward search: a new approach, Artificial Intelligence, v.170 n.6, p.507-541, May 2006
Vincent Vidal , Héctor Geffner, Branching and pruning: an optimal temporal POCL planner based on constraint programming, Artificial Intelligence, v.170 n.3, p.298-335, March 2006
Daniel Groβe , Ulrich Kühne , Rolf Drechsler, HW/SW co-verification of embedded systems using bounded model checking, Proceedings of the 16th ACM Great Lakes symposium on VLSI, April 30-May 01, 2006, Philadelphia, PA, USA
Piet Engelke , Ilia Polian , Michel Renovell , Bernd Becker, Automatic Test Pattern Generation for Resistive Bridging Faults, Journal of Electronic Testing: Theory and Applications, v.22 n.1, p.61-69, February 2006
Christopher Jefferson , Angela Miguel , Ian Miguel , S. Armagan Tarim, Modelling and solving English Peg Solitaire, Computers and Operations Research, v.33 n.10, p.2935-2959, October 2006
Jin S. Zhang , Alan Mishchenko , Robert Brayton , Malgorzata Chrzanowska-Jeske, Symmetry detection for large Boolean functions using circuit representation, simulation, and satisfiability, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA
Felix Sheng-Ho Chang , Daniel Jackson, Symbolic model checking of declarative relational models, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China
Marco Cadoli , Toni Mancini, Automated reformulation of specifications by safe delay of constraints, Artificial Intelligence, v.170 n.8, p.779-801, June 2006
Gunnar Andersson , Per Bjesse , Byron Cook , Ziyad Hanna, A proof engine approach to solving combinational design automation problems, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
Gianpiero Cabodi , Paolo Camurati , Stefano Quer, Can BDDs compete with SAT solvers on bounded model checking?, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
Victor Khomenko , Maciej Koutny , Alex Yakovlev, Logic synthesis for asynchronous circuits based on STG unfoldings and incremental SAT, Fundamenta Informaticae, v.70 n.1, p.49-73, March 2006
KANGHENG WU , QIANG YANG , YUNFEI JIANG, ARMS: an automatic knowledge engineering tool for learning action models for AI planning, The Knowledge Engineering Review, v.22 n.2, p.135-152, June 2007
Abhijit Jas , Yi-Shing Chang , Sreejit Chakravarty, A Methodology for Handling Complex Functional Constraints for Large Industrial Designs, Journal of Electronic Testing: Theory and Applications, v.24 n.1-3, p.259-269, June 2008
Volker Sorge , Andreas Meier , Roy Mccasland , Simon Colton, Automatic Construction and Verification of Isotopy Invariants, Journal of Automated Reasoning, v.40 n.2-3, p.221-243, March 2008
Blai Bonet , Héctor Geffner, Heuristics for planning with penalties and rewards formulated in logic and computed through circuits, Artificial Intelligence, v.172 n.12-13, p.1579-1604, August, 2008
Inês Lynce , João P. Marques-Silva, An Overview of Backtrack Search Satisfiability Algorithms, Annals of Mathematics and Artificial Intelligence, v.37 n.3, p.307-326, March 2003
Nathan Kitchen , Andreas Kuehlmann, Stimulus generation for constrained random simulation, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
Fadi Zaraket , Adnan Aziz , Sarfraz Khurshid, Sequential circuits for program analysis, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA
Carsten Sinz, Visualizing SAT Instances and Runs of the DPLL Algorithm, Journal of Automated Reasoning, v.39 n.2, p.219-243, August 2007
John D. Davis , Zhangxi Tan , Fang Yu , Lintao Zhang, A practical reconfigurable hardware accelerator for Boolean satisfiability solvers, Proceedings of the 45th annual conference on Design automation, June 08-13, 2008, Anaheim, California
Geoff Sutcliffe , Christian Suttner, The CADE-19 ATP System Competition, AI Communications, v.17 n.3, p.103-110, August 2004
Vishnu C. Vimjam , Michael S. Hsiao, Fast illegal state identification for improving SAT-based induction, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA
Chao Wang , Aarti Gupta , Malay Ganai, Predicate learning and selective theory deduction for a difference logic solver, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA
Sorav Bansal , Alex Aiken, Automatic generation of peephole superoptimizers, ACM SIGPLAN Notices, v.41 n.11, November 2006
Warren A. Hunt, Jr. , Erik Reeber, A SAT-based procedure for verifying finite state machines in ACL2, Proceedings of the sixth international workshop on the ACL2 theorem prover and its applications, August 15-16, 2006, Seattle, Washington
Robert Nieuwenhuis , Albert Oliveras , Cesare Tinelli, Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T), Journal of the ACM (JACM), v.53 n.6, p.937-977, November 2006
Francesco Ricca , Wolfgang Faber , Nicola Leone, A backjumping technique for disjunctive logic programming, AI Communications, v.19 n.2, p.155-172, January 2006
Inês Lynce, Propositional satisfiability: techniques, algorithms and applications, AI Communications, v.19 n.2, p.187-189, January 2006
David Currie , Xiushan Feng , Masahiro Fujita , Alan J. Hu , Mark Kwan , Sreeranga Rajan, Embedded software verification using symbolic execution and uninterpreted functions, International Journal of Parallel Programming, v.34 n.1, p.61-91, Febraury 2006
Marco Bozzano , Roberto Bruttomesso , Alessandro Cimatti , Tommi Junttila , Silvio Ranise , Peter van Rossum , Roberto Sebastiani, Efficient theory combination via boolean search, Information and Computation, v.204 n.10, p.1493-1525, October 2006
Heon-Mo Koo , Prabhat Mishra, Test generation using SAT-based bounded model checking for validation of pipelined processors, Proceedings of the 16th ACM Great Lakes symposium on VLSI, April 30-May 01, 2006, Philadelphia, PA, USA
Weixin Wu , Michael S. Hsiao, Mining global constraints for improving bounded sequential equivalence checking, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA
Namrata Shekhar , Priyank Kalla , Florian Enescu, Equivalence verification of arithmetic datapaths with multiple word-length operands, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
Hana Chockler , Eitan Farchi , Ziv Glazberg , Benny Godlin , Yarden Nir-Buchbinder , Ishai Rabinovitz, Formal verification of concurrent software: two case studies, Proceeding of the 2006 workshop on Parallel and distributed systems: testing and debugging, July 17-17, 2006, Portland, Maine, 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
Andrea F. Lobo , Ganesh R. Baliga, NP-completeness for all computer science undergraduates: a novel project-based curriculum, Journal of Computing Sciences in Colleges, v.21 n.6, p.53-63, June 2006
Sean Safarpour , Andreas Veneris , Gregg Baeckler , Richard Yuan, Efficient SAT-based Boolean matching for FPGA technology mapping, Proceedings of the 43rd annual conference on Design automation, July 24-28, 2006, San Francisco, CA, USA
Qiang Yang , Kangheng Wu , Yunfei Jiang, Learning action models from plan examples using weighted MAX-SAT, Artificial Intelligence, v.171 n.2-3, p.107-143, February, 2007
Katsumi Inoue , Takehide Soh , Seiji Ueda , Yoshito Sasaura , Mutsunori Banbara , Naoyuki Tamura, A competitive and cooperative approach to propositional satisfiability, Discrete Applied Mathematics, v.154 n.16, p.2291-2306, 1 November 2006
Wahid Chrabakh , Rich Wolski, GridSAT: a system for solving satisfiability problems using a computational grid, Parallel Computing, v.32 n.9, p.660-687, October 2006
Jano I. van Hemert, Evolving combinatorial problem instances that are difficult to solve, Evolutionary Computation, v.14 n.4, p.433-462, December 2006
Gang Wu , Jia-Huai You , Guohui Lin, Quartet-Based Phylogeny Reconstruction with Answer Set Programming, IEEE/ACM Transactions on Computational Biology and Bioinformatics (TCBB), v.4 n.1, p.139-152, January 2007
Virendra J. Marathe , Tim Harris , James R. Larus, Featherweight transactions: decoupling threads and atomic blocks, Proceedings of the 12th ACM SIGPLAN symposium on Principles and practice of parallel programming, March 14-17, 2007, San Jose, California, USA
Eugene Goldberg , Yakov Novikov, BerkMin: A fast and robust Sat-solver, Discrete Applied Mathematics, v.155 n.12, p.1549-1561, June, 2007
Hratch Mangassarian , Andreas Veneris , Sean Safarpour , Farid N. Najm , Magdy S. Abadir, Maximum circuit activity estimation using pseudo-boolean satisfiability, Proceedings of the conference on Design, automation and test in Europe, April 16-20, 2007, Nice, France
Sebastian Burckhardt , Rajeev Alur , Milo M. K. Martin, CheckFence: checking consistency of concurrent data types on relaxed memory models, ACM SIGPLAN Notices, v.42 n.6, June 2007
David Eppstein, Quasiconvex analysis of multivariate recurrence equations for backtracking algorithms, ACM Transactions on Algorithms (TALG), v.2 n.4, p.492-509, October 2006
Lucas Bordeaux , Youssef Hamadi , Lintao Zhang, Propositional Satisfiability and Constraint Programming: A comparative survey, ACM Computing Surveys (CSUR), v.38 n.4, p.12-es, 2006
Cormac Flanagan , Stephen N. Freund, Type inference against races, Science of Computer Programming, v.64 n.1, p.140-165, January, 2007
I. Lynce , J. Marques-Silva, Random backtracking in backtrack search algorithms for satisfiability, Discrete Applied Mathematics, v.155 n.12, p.1604-1612, June, 2007
Douglas Cenzer , Jeffrey B. Remmel , Victor W. Marek, Logic programming with infinite sets, Annals of Mathematics and Artificial Intelligence, v.44 n.4, p.309-339, August 2005
Jason Cong , Kirill Minkovich, Improved SAT-based Boolean matching using implicants for LUT-based FPGAs, Proceedings of the 2007 ACM/SIGDA 15th international symposium on Field programmable gate arrays, February 18-20, 2007, Monterey, California, USA
Robert Nieuwenhuis , Albert Oliveras, Fast congruence closure and extensions, Information and Computation, v.205 n.4, p.557-580, April, 2007
Marcelo Arenas, Normalization theory for XML, ACM SIGMOD Record, v.35 n.4, December 2006
Henry Kautz , Bart Selman, The state of SAT, Discrete Applied Mathematics, v.155 n.12, p.1514-1524, June, 2007
Stephanie Kemper , André Platzer, SAT-based Abstraction Refinement for Real-time Systems, Electronic Notes in Theoretical Computer Science (ENTCS), 182, p.107-122, June, 2007
Jen-Chieh Ou , Daniel G. Saab , Qiang Qiang , Jacob A. Abraham, Reducing verification overhead with RTL slicing, Proceedings of the 17th great lakes symposium on Great lakes symposium on VLSI, March 11-13, 2007, Stresa-Lago Maggiore, Italy
Lars-Henrik Eriksson, The GTO Toolset and Method, Electronic Notes in Theoretical Computer Science (ENTCS), 185, p.77-91, July, 2007
David Deharbe , Silvio Ranise , Jorgiano Vidal, Distributing the Workload in a Lazy Theorem-Prover, Electronic Notes in Theoretical Computer Science (ENTCS), 184, p.21-37, July, 2007
Marcelo F. Frias , Carlos G. Lopez Pombo , Juan P. Galeotti , Nazareno M. Aguirre, Efficient Analysis of DynAlloy Specifications, ACM Transactions on Software Engineering and Methodology (TOSEM), v.17 n.1, p.1-34, December 2007
Erika Ábrahám , Marc Herbstritt , Bernd Becker , Martin Steffen, Bounded Model Checking with Parametric Data Structures, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.3, p.3-16, May, 2007
Viorica Sofronie-Stokkermans, On unification for bounded distributive lattices, ACM Transactions on Computational Logic (TOCL), v.8 n.2, p.12-es, April 2007
Edmund Clarke , Himanshu Jain , Daniel Kroening, Verification of SpecC using predicate abstraction, Formal Methods in System Design, v.30 n.1, p.5-28, February 2007
Tobias Schuele , Klaus Schneider, Bounded model checking of infinite state systems, Formal Methods in System Design, v.30 n.1, p.51-81, February 2007
Gianpiero Cabodi , Marco Murciano , Sergio Nocco , Stefano Quer, Boosting interpolation with dynamic localized abstraction and redundancy removal, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.13 n.1, p.1-20, January 2008
Hratch Mangassarian , Andreas Veneris , Sean Safarpour , Marco Benedetti , Duncan Smith, A performance-driven QBF-based iterative logic array representation with applications to verification, debug and test, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
Alexander Taubin , Jordi Cortadella , Luciano Lavagno , Alex Kondratyev , Ad Peeters, Design automation of real-life asynchronous devices and systems, Foundations and Trends® in Electronic Design Automation, v.2 n.1, p.1-133, January 2007
Alan Mishchenko , Satrajit Chatterjee , Robert Brayton , Niklas Een, Improvements to combinational equivalence checking, Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design, November 05-09, 2006, San Jose, California
Yichen Xie , Alex Aiken, Saturn: A scalable framework for error detection using Boolean satisfiability, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.3, p.16-es, May 2007
Ramón Béjar , Felip Manyí , Alba Cabiscol , Cèsar Ferníndez , Carla Gomes, Regular-SAT: A many-valued approach to solving combinatorial problems, Discrete Applied Mathematics, v.155 n.12, p.1613-1626, June, 2007
Andreas Bauer , Markus Pister , Michael Tautschnig, Tool-support for the analysis of hybrid systems and models, Proceedings of the conference on Design, automation and test in Europe, April 16-20, 2007, Nice, France
Stephen M. Majercik, APPSSAT: Approximate probabilistic planning using stochastic satisfiability, International Journal of Approximate Reasoning, v.45 n.2, p.402-419, July, 2007
Chi-An Wu , Ting-Hao Lin , Chih-Chun Lee , Chung-Yang (Ric) Huang, QuteSAT: a robust circuit-based SAT solver for complex circuit structure, Proceedings of the conference on Design, automation and test in Europe, April 16-20, 2007, Nice, France
Sriram Sankaranarayanan , Swarat Chaudhuri , Franjo Ivančić , Aarti Gupta, Dynamic inference of likely data preconditions over predicates by tree learning, Proceedings of the 2008 international symposium on Software testing and analysis, July 20-24, 2008, Seattle, WA, USA
Joao Marques-Silva, Interpolant Learning and Reuse in SAT-Based Model Checking, Electronic Notes in Theoretical Computer Science (ENTCS), v.174 n.3, p.31-43, May, 2007
Zhaohui Fu , Sharad Malik, Solving the minimum-cost satisfiability problem using SAT based branch-and-bound search, Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design, November 05-09, 2006, San Jose, California
Yu-Min Kuo , Yue-Lung Chang , Shih-Chieh Chang, Efficient Boolean characteristic function for fast timed ATPG, Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design, November 05-09, 2006, San Jose, California
Lei Fang , Michael S. Hsiao, A new hybrid solution to boost SAT solver performance, Proceedings of the conference on Design, automation and test in Europe, April 16-20, 2007, Nice, France
Ofer Arieli, Paraconsistent reasoning and preferential entailments by signed quantified Boolean formulae, ACM Transactions on Computational Logic (TOCL), v.8 n.3, p.18-es, July 2007
Martin Fränzle , Christian Herde, HySAT: An efficient proof engine for bounded model checking of hybrid systems, Formal Methods in System Design, v.30 n.3, p.179-198, June 2007
V. Durairaj , P. Kalla, Guiding CNF-SAT search via efficient constraint partitioning, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.498-501, November 07-11, 2004
Liang Zhang , M. R. Prasad , M. S. Hsiao, Incremental deductive & inductive reasoning for SAT-based bounded model checking, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.502-509, November 07-11, 2004
M. K. Ganai , A. Gupta , P. Ashar, Efficient SAT-based unbounded symbolic model checking using circuit cofactoring, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.510-517, November 07-11, 2004
Bing Li , F. Somenzi, Efficient computation of small abstraction refinements, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.518-525, November 07-11, 2004
A. Kuehlmann, Dynamic transition relation simplification for bounded property checking, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.50-57, November 07-11, 2004
D. Kroening , E. Clarke, Checking consistency of C and Verilog using predicate abstraction and induction, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.66-72, November 07-11, 2004
M. Fahim Ali , A. Veneris , A. Smith , S. Safarpour , R. Drechsler , M. Abadir, Debugging sequential circuits using Boolean satisfiability, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.204-209, November 07-11, 2004
Kuo-Hua Wang , Chung-Ming Chan, Incremental learning approach and SAT model for Boolean matching with don't cares, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
Carla P. Gomes , Cèsar Fernández , Bart Selman , Christian Bessière, Statistical Regimes Across Constrainedness Regions, Constraints, v.10 n.4, p.317-337, October 2005
Allen Van Gelder, Another look at graph coloring via propositional satisfiability, Discrete Applied Mathematics, v.156 n.2, p.230-243, January, 2008
Fadi Zaraket , Adnan Aziz , Sarfraz Khurshid, Sequential Circuits for Relational Analysis, Proceedings of the 29th International Conference on Software Engineering, p.13-22, May 20-26, 2007
Sheng Liu , Jian Zhang, Retrieving and Matching RDF Graphs by Solving the Satisfiability Problem, Proceedings of the 2006 IEEE/WIC/ACM International Conference on Web Intelligence, p.510-513, December 18-22, 2006
Engin Uzuncaova , Daniel Garcia , Sarfraz Khurshid , Don Batory, A specification-based approach to testing software product lines, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia
Mana Taghdiri , Daniel Jackson, Inferring specifications to detect errors in code, Automated Software Engineering, v.14 n.1, p.87-121, March 2007
P. Flores , J. Monteiro , E. Costa, An exact algorithm for the maximal sharing of partial terms in multiple constant multiplications, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.13-16, November 06-10, 2005, San Jose, CA
M. F. Ali , S. Safarpour , A. Veneris , M. S. Abadir , R. Drechsler, Post-verification debugging of hierarchical designs, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.871-876, November 06-10, 2005, San Jose, CA
Suchismita Roy , Sayantan Das , Prasenjit Basu , Pallab Dasgupta , P. P. Chakrabarti, SAT based solutions for consistency problems in formal property specifications for open systems, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.885-888, November 06-10, 2005, San Jose, CA
M. D. Nguyen , D. Stoffel , M. Wedler , W. Kunz, Transition-by-transition FSM traversal for reachability analysis in bounded model checking, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.1068-1075, November 06-10, 2005, San Jose, CA
R. Drechsler, Using Word-Level Information in Formal Hardware Verification, Automation and Remote Control, v.65 n.6, p.963-977, June 2004
N. Shekhar , P. Kalla , F. Enescu , S. Gopalakrishnan, Equivalence verification of polynomial datapaths with fixed-size bit-vectors using finite ring algebra, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.291-296, November 06-10, 2005, San Jose, CA
G. Parthasarathy , M. K. Iyer , K.-T. Cheng , F. Brewer, RTL SAT simplification by Boolean and interval arithmetic reasoning, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.297-302, November 06-10, 2005, San Jose, CA
A. Koelbl , Yuan Lu , A. Mathur, Embedded tutorial: formal equivalence checking between system-level models and RTL, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.965-971, November 06-10, 2005, San Jose, CA
Dirk Beyer , Adam J. Chlipala , Rupak Majumdar, Generating Tests from Counterexamples, Proceedings of the 26th International Conference on Software Engineering, p.326-335, May 23-28, 2004
Ofer Arieli , Marc Denecker , Bert Nuffelen , Maurice Bruynooghe, Computational methods for database repair by signed formulae, Annals of Mathematics and Artificial Intelligence, v.46 n.1-2, p.4-37, February 2006
Takeshi Matsumoto , Hiroshi Saito , Masahiro Fujita, Equivalence Checking of C Programs by Locally Performing Symbolic Simulation on Dependence Graphs, Proceedings of the 7th International Symposium on Quality Electronic Design, p.370-375, March 27-29, 2006
Josep Argelich , Felip Manyà, Exact Max-SAT solvers for over-constrained problems, Journal of Heuristics, v.12 n.4-5, p.375-392, September 2006
Miroslav N. Velev, Using Abstraction for Efficient Formal Verification of Pipelined Processors with Value Prediction, Proceedings of the 7th International Symposium on Quality Electronic Design, p.51-56, March 27-29, 2006
Victor Khomenko , Maciej Koutny , Alex Yakovlev, Detecting State Encoding Conflicts in STG Unfoldings Using SAT, Fundamenta Informaticae, v.62 n.2, p.221-241, April 2004
Kaushik Ravindran , Andreas Kuehlmann , Ellen Sentovich, Multi-Domain Clock Skew Scheduling, Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design, p.801, November 09-13, 2003
M. K. Iyer , G. Parthasarathy , K.-T. Cheng, SATORI - A Fast Sequential SAT Engine for Circuits, Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design, p.320, November 09-13, 2003
Cong Liu , Andreas Kuehlmann , Matthew W. Moskewicz, CAMA: A Multi-Valued Satisfiability Solver, Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design, p.326, November 09-13, 2003
Doron B. Motter , Jarrod A. Roy , Igor L. Markov, Resolution cannot polynomially simulate compressed-BFS, Annals of Mathematics and Artificial Intelligence, v.44 n.1-2, p.121-156, May 2005
Chao Wang , Bing Li , HoonSang Jin , Gary D. Hachtel , Fabio Somenzi, Improving Ariadne's Bundle by Following Multiple Threads in Abstraction Refinement, Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design, p.408, November 09-13, 2003
Aarti Gupta , Malay Ganai , Zijiang Yang , Pranav Ashar, Iterative Abstraction using SAT-based BMC with Proof Analysis, Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design, p.416, November 09-13, 2003
Lintao Zhang , Sharad Malik, Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications, Proceedings of the conference on Design, Automation and Test in Europe, p.10880, March 03-07, 2003
Evgueni Goldberg , Yakov Novikov, Verification of Proofs of Unsatisfiability for CNF Formulas, Proceedings of the conference on Design, Automation and Test in Europe, p.10886, March 03-07, 2003
Feng Lu , Li-C. Wang , Kwang-Ting Cheng , Ric C-Y Huang, A Circuit SAT Solver With Signal Correlation Guided Learning, Proceedings of the conference on Design, Automation and Test in Europe, p.10892, March 03-07, 2003
Gianpiero Cabodi , Sergio Nocco , Stefano Quer, Improving SAT-Based Bounded Model Checking by Means of BDD-Based Approximate Traversals, Proceedings of the conference on Design, Automation and Test in Europe, p.10898, March 03-07, 2003
Wahid Chrabakh , Rich Wolski, GridSAT: A Chaff-based Distributed SAT Solver for the Grid, Proceedings of the 2003 ACM/IEEE conference on Supercomputing, p.37, November 15-21, 2003
Yakov Novikov, Local Search for Boolean Relations on the Basis of Unit Propagation, Proceedings of the conference on Design, Automation and Test in Europe, p.10810, March 03-07, 2003
Debasish Das , Kip Killpack , Chandramouli Kashyap , Abhijit Jas , Hai Zhou, Pessimism reduction in coupling-aware static timing analysis using timing and logic filtering, Proceedings of the 2008 conference on Asia and South Pacific design automation, January 21-24, 2008, Seoul, Korea
Inês Lynce , João Marques-Silva, Efficient Data Structures for Backtrack Search SAT Solvers, Annals of Mathematics and Artificial Intelligence, v.43 n.1-4, p.137-152, January 2005
Steven Prestwich , Stéphane Bressan, A SAT Approach to Query Optimization in Mediator Systems, Annals of Mathematics and Artificial Intelligence, v.43 n.1-4, p.195-210, January 2005
Allen Van Gelder, Toward Leaner Binary-Clause Reasoning in a Satisfiability Solver, Annals of Mathematics and Artificial Intelligence, v.43 n.1-4, p.239-253, January 2005
Uwe Egly , Reinhard Pichler , Stefan Woltran, On Deciding Subsumption Problems, Annals of Mathematics and Artificial Intelligence, v.43 n.1-4, p.255-294, January 2005
Paul W. Purdom , Daniel Le Berre , Laurent Simon, A Parsimony Tree for the SAT2002 Competition, Annals of Mathematics and Artificial Intelligence, v.43 n.1-4, p.343-365, January 2005
Satrajit Chatterjee , Alan Mishchenko , Robert Brayton , Andreas Kuehlmann, On resolution proofs for combinational equivalence, Proceedings of the 44th annual conference on Design automation, June 04-08, 2007, San Diego, California
Alfonso Gerevini , Ivan Serina, Planning as Propositional CSP: From Walksat to Local Search Techniques for Action Graphs, Constraints, v.8 n.4, p.389-413, October 2003
Raik Brinkmann , Rolf Drechsler, RTL-Datapath Verification using Integer Linear Programming, Proceedings of the 2002 conference on Asia South Pacific design automation/VLSI Design, p.741, January 07-11, 2002
Carsten Sinz , Andreas Kaiser , Wolfgang Küchlin, Formal methods for the validation of automotive product configuration data, Artificial Intelligence for Engineering Design, Analysis and Manufacturing, v.17 n.1, p.75-97, January 2003
Alan Mishchenko , Robert K. Brayton, SAT-Based Complete Don't-Care Computation for Network Optimization, Proceedings of the conference on Design, Automation and Test in Europe, p.412-417, March 07-11, 2005
Kameshwar Chandrasekar , Michael S. Hsiao, Integration of Learning Techniques into Incremental Satisfiability for Efficient Path-Delay Fault Test Generation, Proceedings of the conference on Design, Automation and Test in Europe, p.1002-1007, March 07-11, 2005
Vasco M. Manquinho , Joao Marques-Silva, Effective Lower Bounding Techniques for Pseudo-Boolean Optimization, Proceedings of the conference on Design, Automation and Test in Europe, p.660-665, March 07-11, 2005
M. K. Iyer , G. Parthasarathy , K.-T. Cheng, Efficient Conflict-Based Learning in an RTL Circuit Constraint Solver, Proceedings of the conference on Design, Automation and Test in Europe, p.666-671, March 07-11, 2005
ShengYu Shen , Ying Qin , SiKun Li, A Faster Counterexample Minimization Algorithm Based on Refutation Analysis, Proceedings of the conference on Design, Automation and Test in Europe, p.672-677, March 07-11, 2005
Hossein M. Sheini , Karem A. Sakallah, Pueblo: A Modern Pseudo-Boolean SAT Solver, Proceedings of the conference on Design, Automation and Test in Europe, p.684-685, March 07-11, 2005
F. Lu , M. K. Iyer , G. Parthasarathy , L.-C. Wang , K.-T. Cheng , K. C. Chen, An Efficient Sequential SAT Solver With Improved Search Strategies, Proceedings of the conference on Design, Automation and Test in Europe, p.1102-1107, March 07-11, 2005
Zhaohui Fu , Yinlei Yu , Sharad Malik, Considering Circuit Observability Don't Cares in CNF Satisfiability, Proceedings of the conference on Design, Automation and Test in Europe, p.1108-1113, March 07-11, 2005
Guoqiang Pan , Moshe Y. Vardi, Symbolic Techniques in Satisfiability Solving, Journal of Automated Reasoning, v.35 n.1-3, p.25-50, October 2005
Jan Johannsen, The Complexity of Pure Literal Elimination, Journal of Automated Reasoning, v.35 n.1-3, p.89-95, October 2005
John Thornton, Clause Weighting Local Search for SAT, Journal of Automated Reasoning, v.35 n.1-3, p.97-142, October 2005
Laurent Simon , Daniel Le Berre , Edward A. Hirsch, The SAT2002 Competition, Annals of Mathematics and Artificial Intelligence, v.43 n.1-4, p.307-342, January 2005
Andreas Meier , Volker Sorge, Applying SAT Solving in Classification of Finite Algebras, Journal of Automated Reasoning, v.35 n.1-3, p.201-235, October 2005
Lengning Liu , Mirosław Truszczyński, Satisfiability Testing of Boolean Combinations of Pseudo-Boolean Constraints using Local-search Techniques, Constraints, v.12 n.3, p.345-369, September 2007
Alessandro Armando , Claudio Castellini , Enrico Giunchiglia , Marco Maratea, The SAT-based Approach to Separation Logic, Journal of Automated Reasoning, v.35 n.1-3, p.237-263, October 2005
Marco Bozzano , Roberto Bruttomesso , Alessandro Cimatti , Tommi Junttila , Peter Rossum , Stephan Schulz , Roberto Sebastiani, MathSAT: Tight Integration of SAT and Mathematical Decision Procedures, Journal of Automated Reasoning, v.35 n.1-3, p.265-293, October 2005
Carlos Ansótegui , Jose Larrubia , Chu---Min Li , Felip Manyà, Exploiting multivalued knowledge in variable selection heuristics for SAT solvers, Annals of Mathematics and Artificial Intelligence, v.49 n.1-4, p.191-205, April 2007
Franc Brglez , Xiao Yu Li , Matthias F. Stallmann, On SAT Instance Classes and a Method for Reliable Performance Experiments with SAT Solvers, Annals of Mathematics and Artificial Intelligence, v.43 n.1-4, p.1-34, January 2005
Enrico Giunchiglia , Yuliya Lierler , Marco Maratea, Answer Set Programming Based on Propositional Satisfiability, Journal of Automated Reasoning, v.36 n.4, p.345-377, April 2006
Eugene Goldberg, Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points, Annals of Mathematics and Artificial Intelligence, v.43 n.1-4, p.65-89, January 2005
Ateet Bhalla , Inês Lynce , José T. Sousa , João Marques-Silva, Heuristic-Based Backtracking Relaxation for Propositional Satisfiability, Journal of Automated Reasoning, v.35 n.1-3, p.3-24, October 2005
Edward A. Hirsch , Arist Kojevnikov, UnitWalk: A New SAT Solver that Uses Local Search Guided by Unit Clause Elimination, Annals of Mathematics and Artificial Intelligence, v.43 n.1-4, p.91-111, January 2005
Keijo Heljanko , Ilkka Niemelä, Bounded LTL model checking with stable models, Theory and Practice of Logic Programming, v.3 n.4, p.519-550, July 2003
Markus Wedler , Dominik Stoffel , Wolfgang Kunz, Using RTL Statespace Information and State Encoding for Induction Based Property Checking, Proceedings of the conference on Design, Automation and Test in Europe, p.11156, March 03-07, 2003
Bin Li , Michael S. Hsiao , Shuo Sheng, A Novel SAT All-Solutions Solver for Efficient Preimage Computation, Proceedings of the conference on Design, automation and test in Europe, p.10272, February 16-20, 2004
Arathi Ramani , Fadi A. Aloul , Igor L. Markov , Karem A. Sakallah, Breaking Instance-Independent Symmetries in Exact Graph Coloring, Proceedings of the conference on Design, automation and test in Europe, p.10324, February 16-20, 2004
Markus Wedler , Dominik Stoffel , Wolfgang Kunz, Arithmetic Reasoning in DPLL-Based SAT Solving, Proceedings of the conference on Design, automation and test in Europe, p.10030, February 16-20, 2004
Panagiotis Manolios , Sudarshan K. Srinivasan, Automatic Verification of Safety and Liveness for XScale-Like Processor Models Using WEB Refinements, Proceedings of the conference on Design, automation and test in Europe, p.10168, February 16-20, 2004
Sean Safarpour , Andreas Veneris , Rolf Drechsler , Joanne Lee, Managing Don't Cares in Boolean Satisfiability, Proceedings of the conference on Design, automation and test in Europe, p.10260, February 16-20, 2004
Miroslav N. Velev, Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of Microprocessors, Proceedings of the conference on Design, automation and test in Europe, p.10266, February 16-20, 2004
Yajun Ran , Alex Kondratyev , Yosinori Watanabe , Malgorzata Marek-Sadowska, Eliminating False Positives in Crosstalk Noise Analysis, Proceedings of the conference on Design, automation and test in Europe, p.21192, February 16-20, 2004
Y. Chevalier , L. Vigneron, Strategy for Verifying Security Protocols with Unbounded Message Size, Automated Software Engineering, v.11 n.2, p.141-166, April 2004
G. Sutcliffe , C. B. Suttner, The CADE-18 ATP System Competition, Journal of Automated Reasoning, v.31 n.1, p.23-32, 2003
Christian Schulte , Peter J. Stuckey, Efficient constraint propagation engines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.31 n.1, p.1-43, December 2008
Isabelle Fagnot , Gaëlle Lelandais , Stéphane Vialette, Bounded list injective homomorphism for comparative analysis of protein-protein interaction graphs, Journal of Discrete Algorithms, v.6 n.2, p.178-191, June, 2008
Martin Lukasiewycz , Michael Glaß , Christian Haubelt , Jürgen Teich, Efficient symbolic multi-objective design space exploration, Proceedings of the 2008 conference on Asia and South Pacific design automation, January 21-24, 2008, Seoul, Korea
Shujun Deng , Jinian Bian , Weimin Wu , Xiaoqing Yang , Yanni Zhao, EHSAT: an efficient RTL satisfiability solver using an extended DPLL procedure, Proceedings of the 44th annual conference on Design automation, June 04-08, 2007, San Diego, California
Stephen M. Plaza , Igor L. Markov , Valeria Bertacco, Optimizing non-monotonic interconnect using functional simulation and logic restructuring, Proceedings of the 2008 international symposium on Physical design, April 13-16, 2008, Portland, Oregon, USA
Robert Wille , Daniel Große, Fast exact Toffoli network synthesis of reversible logic, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
Yiqiao Wang , Sheila A. McIlraith , Yijun Yu , John Mylopoulos, An automated approach to monitoring and diagnosing requirements, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA
Engin Uzuncaova , Daniel Garcia , Sarfraz Khurshid , Don Batory, A specification-based approach to testing software product lines, The 6th Joint Meeting on European software engineering conference and the ACM SIGSOFT symposium on the foundations of software engineering: companion papers, September 03-07, 2007, Dubrovnik, Croatia
Tobias Nopper , Christoph Scholl , Bernd Becker, Computation of minimal counterexamples by using black box techniques and symbolic methods, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
Chih-Chun Lee , Jie-Hong R. Jiang , Chung-Yang (Ric) Huang , Alan Mishchenko, Scalable exploration of functional dependency by interpolation and incremental SAT solving, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
Ohad Shacham , Karen Yorav, On-the-fly resolve trace minimization, Proceedings of the 44th annual conference on Design automation, June 04-08, 2007, San Diego, California
Yexin Zheng , Michael S. Hsiao , Chao Huang, SAT-based equivalence checking of threshold logic designs for nanotechnologies, Proceedings of the 18th ACM Great Lakes symposium on VLSI, May 04-06, 2008, Orlando, Florida, USA
Matteo Pradella , Angelo Morzenti , Pierluigi San Pietro, The symmetry of the past and of the future: bi-infinite time in the verification of temporal properties, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia
Peter Baumgartner , Cesare Tinelli, The model evolution calculus as a first-order DPLL method, Artificial Intelligence, v.172 n.4-5, p.591-632, March, 2008
Hyojung Han , Fabio Somenzi, Alembic: an efficient algorithm for CNF preprocessing, Proceedings of the 44th annual conference on Design automation, June 04-08, 2007, San Diego, California
Assim Sagahyroon , Fadi A. Aloul, Using SAT-based techniques in power estimation, Microelectronics Journal, v.38 n.6-7, p.706-715, June, 2007
Josep Carmona , Jordi Cortadella , Yousuke Takada , Ferdinand Peper, Formal methods for the analysis and synthesis of nanometer-scale cellular arrays, ACM Journal on Emerging Technologies in Computing Systems (JETC), v.4 n.2, p.1-27, April 2008
Wolfgang Faber , Nicola Leone , Gerald Pfeifer , Francesco Ricca, On look-ahead heuristics in disjunctive logic programming, Annals of Mathematics and Artificial Intelligence, v.51 n.2-4, p.229-266, December 2007
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
Miroslav N. Velev, Exploiting hierarchy and structure to efficiently solve graph coloring as SAT, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
Franjo Ivani , Zijiang Yang , Malay K. Ganai , Aarti Gupta , Pranav Ashar, Efficient SAT-based bounded model checking for software verification, Theoretical Computer Science, v.404 n.3, p.256-274, September, 2008
Calvin Kai Fan Tang , Eugenia Ternovska, Model Checking Abstract State Machines with Answer Set Programming, Fundamenta Informaticae, v.77 n.1-2, p.105-141, January 2007
Chia-Chih Yen , Jing-Yang Jou, An Optimum Algorithm for Compacting Error Traces for Efficient Design Error Debugging, IEEE Transactions on Computers, v.55 n.11, p.1356-1366, November 2006
Ian P. Gent , Chris Jefferson , Tom Kelsey , Inês Lynce , Ian Miguel , Peter Nightingale , Barbara M. Smith , S. Armagan Tarim, Search in the patience game ‘Black Hole’, AI Communications, v.20 n.3, p.211-226, August 2007
Gilles Audemard , Said Jabbour , Lakhdar Sais, SAT graph-based representation: A new perspective, Journal of Algorithms, v.63 n.1-3, p.17-33, January, 2008
Ashesh Rastogi , Kunal P. Ganeshpure , Alodeep Sanyal , Sandip Kundu, On Composite Leakage Current Maximization, Journal of Electronic Testing: Theory and Applications, v.24 n.4, p.405-420, August 2008
Ondřej Lhoták , Laurie Hendren, Relations as an abstraction for BDD-based program analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.4, p.1-63, July 2008
Hidde de Jong , Michel Page, Search for Steady States of Piecewise-Linear Differential Equation Models of Genetic Regulatory Networks, IEEE/ACM Transactions on Computational Biology and Bioinformatics (TCBB), v.5 n.2, p.208-222, April 2008
Duc Nghia Pham , John Thornton , Abdul Sattar, Modelling and solving temporal reasoning as propositional satisfiability, Artificial Intelligence, v.172 n.15, p.1752-1782, October, 2008
Volkan Rodoplu , Amir Aminzadeh Gohari, Challenges: automated design of networking protocols, Proceedings of the 14th ACM international conference on Mobile computing and networking, September 14-19, 2008, San Francisco, California, USA
Fadi A. Aloul , Arathi Ramani , Karem A. Sakallah , Igor L. Markov, Solution and Optimization of Systems of Pseudo-Boolean Constraints, IEEE Transactions on Computers, v.56 n.10, p.1415-1424, October 2007
Richard C. Murphy , Peter M. Kogge, On the Memory Access Patterns of Supercomputer Applications: Benchmark Selection and Its Implications, IEEE Transactions on Computers, v.56 n.7, p.937-945, July 2007
Robert Wille , Hoang M. Le , Gerhard W. Dueck , Daniel Große, Quantified synthesis of reversible logic, Proceedings of the conference on Design, automation and test in Europe, March 10-14, 2008, Munich, Germany
Jens Schönherr , Martin Freibothe , Bernd Straube , Jörg Bormann, Semi-formal verification of the steady state behavior of mixed-signal circuits by SAT-based property checking, Theoretical Computer Science, v.404 n.3, p.293-307, September, 2008
Joao Marques-Silva, Model checking with Boolean Satisfiability, Journal of Algorithms, v.63 n.1-3, p.3-16, January, 2008
Qingwei Wu , Michael S. Hsiao, A New Simulation-Based Property Checking Algorithm Based on Partitioned Alternative Search Space Traversal, IEEE Transactions on Computers, v.55 n.11, p.1325-1334, November 2006
Marco Maratea , Francesco Ricca , Wolfgang Faber , Nicola Leone, Look-back techniques and heuristics in DLV: Implementation, evaluation, and comparison to QBF solvers, Journal of Algorithms, v.63 n.1-3, p.70-89, January, 2008
Domagoj Babic , Jesse Bingham , Alan J. Hu, B-Cubing: New Possibilities for Efficient SAT-Solving, IEEE Transactions on Computers, v.55 n.11, p.1315-1324, November 2006
Matti Järvisalo , Ilkka Niemelä, The effect of structural branching on the efficiency of clause learning SAT solving: An experimental study, Journal of Algorithms, v.63 n.1-3, p.90-113, January, 2008
Miroslav N. Velev , Ping Gao, Comparison of Boolean satisfiability encodings on FPGA detailed routing problems, Proceedings of the conference on Design, automation and test in Europe, March 10-14, 2008, Munich, Germany
Matti JÄrvisalo , Emilia Oikarinen, Extended asp tableaux and rule redundancy in normal logic programs1, Theory and Practice of Logic Programming, v.8 n.5-6, p.691-716, November 2008
Hasan Amjad, Data Compression for Proof Replay, Journal of Automated Reasoning, v.41 n.3-4, p.193-218, November 2008
John Backes , Brian Fett , Marc D. Riedel, The analysis of cyclic circuits with Boolean satisfiability, Proceedings of the 2008 IEEE/ACM International Conference on Computer-Aided Design, November 10-13, 2008, San Jose, California
Yiqiao Wang , Sheila A. Mcilraith , Yijun Yu , John Mylopoulos, Monitoring and diagnosing software requirements, Automated Software Engineering, v.16 n.1, p.3-35, March 2009
Chen-Hsuan Lin , Chun-Yao Wang, Dependent latch identification in the reachable state space, Proceedings of the 2009 Conference on Asia and South Pacific Design Automation, January 19-22, 2009, Yokohama, Japan
Andrew C. Ling , Stephen D. Brown , Jianwen Zhu , Sean Safarpour, Towards automated ECOs in FPGAs, Proceeding of the ACM/SIGDA international symposium on Field programmable gate arrays, February 22-24, 2009, Monterey, California, USA
Alda Carvalho , Nuno Crato , Carla Gomes, A generative power-law search tree model, Computers and Operations Research, v.36 n.8, p.2376-2386, August, 2009
Alessandro Armando , Maria Paola Bonacina , Silvio Ranise , Stephan Schulz, New results on rewrite-based satisfiability procedures, ACM Transactions on Computational Logic (TOCL), v.10 n.1, p.1-51, January 2009
Henry Kautz, Deconstructing planning as satisfiability, proceedings of the 21st national conference on Artificial intelligence, p.1524-1526, July 16-20, 2006, Boston, Massachusetts
Lukas Kroc , Ashish Sabharwal , Bart Selman, Message-passing and local heuristics as decimation strategies for satisfiability, Proceedings of the 2009 ACM symposium on Applied Computing, March 08-12, 2009, Honolulu, Hawaii
Jessica Davies , Fahiem Bacchus, Using more reasoning to improve #SAT solving, Proceedings of the 22nd national conference on Artificial intelligence, p.185-190, July 22-26, 2007, Vancouver, British Columbia, Canada
Horst Samulowitz , Roland Memisevic, Learning to solve QBF, Proceedings of the 22nd national conference on Artificial intelligence, p.255-260, July 22-26, 2007, Vancouver, British Columbia, Canada
George Katsirelos , Fahiem Bacchus, Generalized nogoods in CSPs, Proceedings of the 20th national conference on Artificial intelligence, p.390-396, July 09-13, 2005, Pittsburgh, Pennsylvania
Juan A. Navarro , Andrei Voronkov, Generation of hard non-clausal random satisfiability problems, Proceedings of the 20th national conference on Artificial intelligence, p.436-442, July 09-13, 2005, Pittsburgh, Pennsylvania
Ashish Sabharwal, SymChaff: a structure-aware satisfiability solver, Proceedings of the 20th national conference on Artificial intelligence, p.467-474, July 09-13, 2005, Pittsburgh, Pennsylvania
Andrzej Zbrzezny , Bożena Woźna, Towards Verification of Java Programs in perICS, Fundamenta Informaticae, v.85 n.1-4, p.533-548, September 2008
Kanupriya Gulati , Suganth Paul , Sunil P. Khatri , Srinivas Patil , Abhijit Jas, FPGA-based hardware acceleration for Boolean satisfiability, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.14 n.2, p.1-11, March 2009
Naoyuki Tamura , Akiko Taga , Satoshi Kitagawa , Mutsunori Banbara, Compiling finite linear CSP into SAT, Constraints, v.14 n.2, p.254-272, June 2009
Armin Biere , Robert Brummayer, Consistency checking of all different constraints over bit-vectors within a SAT solver, Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, p.1-4, November 17-20, 2008, Portland, Oregon
Brian Keng , Hratch Mangassarian , Andreas Veneris, A succinct memory model for automated design debugging, Proceedings of the 2008 IEEE/ACM International Conference on Computer-Aided Design, November 10-13, 2008, San Jose, California
Shujun Deng , Zhiqiu Kong , Jinian Bian , Yanni Zhao, Self-adjusting constrained random stimulus generation using splitting evenness evaluation and XOR constraints, Proceedings of the 2009 Conference on Asia and South Pacific Design Automation, January 19-22, 2009, Yokohama, Japan
Emilia Katz , Shmuel Katz, Modular verification of strongly invasive aspects: summary, Proceedings of the 2009 workshop on Foundations of aspect-oriented languages, March 02-02, 2009, Charlottesville, Virginia, USA
Dan Goldwasser , Ofer Strichman , Shai Fine, A theory-based decision heuristic for DPLL(T), Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, p.1-8, November 17-20, 2008, Portland, Oregon
Enrico Giunchiglia , Nicola Leone , Marco Maratea, On the relation among answer set solvers, Annals of Mathematics and Artificial Intelligence, v.53 n.1-4, p.169-204, August 2008
Agostino Dovier , Andrea Formisano , Enrico Pontelli, An empirical study of constraint logic programming and answer set programming solutions of combinatorial problems, Journal of Experimental & Theoretical Artificial Intelligence, v.21 n.2, p.79-121, June 2009
Enrico Giunchiglia , Yuliya Lierler , Marco Maratea, SAT-based answer set programming, Proceedings of the 19th national conference on Artifical intelligence, p.61-66, July 25-29, 2004, San Jose, California
Hai Fang , Wheeler Ruml, Complete local search for propositional satisfiability, Proceedings of the 19th national conference on Artifical intelligence, p.161-166, July 25-29, 2004, San Jose, California
Carlos Ansótegui , Alvaro del Val , Iván Dotú , Cèsar Fernández , Felip Manyà, Modeling choices in quasigroup completion: SAT vs. CSP, Proceedings of the 19th national conference on Artifical intelligence, p.137-142, July 25-29, 2004, San Jose, California
Yongshao Ruan , Henry Kautz , Eric Horvitz, The backdoor key: a path to understanding problem hardness, Proceedings of the 19th national conference on Artifical intelligence, p.118-123, July 25-29, 2004, San Jose, California
Lin Yuan , Pushkin R. Pari , Gang Qu, Finding redundant constraints in FSM minimization, Proceedings of the 19th national conference on Artifical intelligence, p.976-977, July 25-29, 2004, San Jose, California
Filip Marić, Formalization and Implementation of Modern SAT Solvers, Journal of Automated Reasoning, v.43 n.1, p.81-119, June 2009
Pingzhong Tang , Fangzhen Lin, Computer-aided proofs of Arrow's and other impossibility theorems, Artificial Intelligence, v.173 n.11, p.1041-1053, July, 2009
Dafna Shahaf , Allen Chang , Eyal Amir, Learning partially observable action models: efficient algorithms, Proceedings of the 21st national conference on Artificial intelligence, p.920-926, July 16-20, 2006, Boston, Massachusetts
Adam Kiezun , Vijay Ganesh , Philip J. Guo , Pieter Hooimeijer , Michael D. Ernst, HAMPI: a solver for string constraints, Proceedings of the eighteenth international symposium on Software testing and analysis, July 19-23, 2009, Chicago, IL, USA
Parag Singla , Pedro Domingos, Memory-efficient inference in relational domains, Proceedings of the 21st national conference on Artificial intelligence, p.488-493, July 16-20, 2006, Boston, Massachusetts
Carlos Ansótegui , Ramón Béjar , César Fernàndez , Carla Gomes , Carles Mateu, The impact of balancing on problem hardness in a highly structured domain, Proceedings of the 21st national conference on Artificial intelligence, p.10-15, July 16-20, 2006, Boston, Massachusetts
Michael D. Moffitt , Martha E. Pollack, Temporal preference optimization as weighted constraint satisfaction, Proceedings of the 21st national conference on Artificial intelligence, p.110-116, July 16-20, 2006, Boston, Massachusetts
Lintao Zhang, Solving QBF with combined conjunctive and disjunctive normal form, Proceedings of the 21st national conference on Artificial intelligence, p.143-149, July 16-20, 2006, Boston, Massachusetts
Zhijun Lin , Yuanlin Zhang , Hector Hernandez, Fast SAT-based answer set solver, Proceedings of the 21st national conference on Artificial intelligence, p.92-97, July 16-20, 2006, Boston, Massachusetts
Robert Mateescu , Rina Dechter, Mixed deterministic and probabilistic networks, Annals of Mathematics and Artificial Intelligence, v.54 n.1-3, p.3-51, November 2008
Heon-Mo Koo , Prabhat Mishra, Functional test generation using design and property decomposition techniques, ACM Transactions on Embedded Computing Systems (TECS), v.8 n.4, p.1-33, July 2009
Sharad Malik , Lintao Zhang, Boolean satisfiability from theoretical hardness to practical success, Communications of the ACM, v.52 n.8, August 2009
Enrico Giunchiglia , Marco Maratea, Solving Optimization Problems with DLL, Proceeding of the 2006 conference on ECAI 2006: 17th European Conference on Artificial Intelligence August 29 -- September 1, 2006, Riva del Garda, Italy, p.377-381, May 22, 2006
Ian P. Gent , Chris Jefferson , Ian Miguel, MINION: A Fast, Scalable, Constraint Solver, Proceeding of the 2006 conference on ECAI 2006: 17th European Conference on Artificial Intelligence August 29 -- September 1, 2006, Riva del Garda, Italy, p.98-102, May 22, 2006
Matti Järvisalo , Tommi Junttila, Limitations of restricted branching in clause learning, Constraints, v.14 n.3, p.325-356, September 2009
Olga Ohrimenko , Peter J. Stuckey , Michael Codish, Propagation via lazy clause generation, Constraints, v.14 n.3, p.357-391, September 2009
Pieter Hooimeijer , Westley Weimer, A decision procedure for subset constraints over regular languages, ACM SIGPLAN Notices, v.44 n.6, June 2009
Arathi Ramani , Igor L. Markov , Karem A. Sakallah , Fadi A. Aloul, Breaking instance-independent symmetries in exact graph coloring, Journal of Artificial Intelligence Research, v.26 n.1, p.289-322, May 2006
Dimitris Achlioptas , Haixia Jia , Cristopher Moore, Hiding satisfying assignments: two are better than one, Journal of Artificial Intelligence Research, v.24 n.1, p.623-639, July 2005
Jinbo Huang , Adnan Darwiche, The language of search, Journal of Artificial Intelligence Research, v.29 n.1, p.191-219, May 2007
Paul Beame , Henry Kautz , Ashish Sabharwal, Towards understanding and harnessing the potential of clause learning, Journal of Artificial Intelligence Research, v.22 n.1, p.319-351, July 2004
Heidi E. Dixon , Matthew L. Ginsberg , David Hofer , Eugene M. Luks , Andrew J. Parkes, Generalizing Boolean satisfiability III: implementation, Journal of Artificial Intelligence Research, v.23 n.1, p.441-531, January 2005
Heidi E. Dixon , Matthew L. Ginsberg , Eugene M. Luks , Andrew J. Parkes, Generalizing Boolean satisfiability II: theory, Journal of Artificial Intelligence Research, v.22 n.1, p.481-534, July 2004
Enrico Giunchiglia , Massimo Narizzano , Armando Tacchella, Clause/term resolution and learning in the evaluation of quantified Boolean formulas, Journal of Artificial Intelligence Research, v.26 n.1, p.371-416, May 2006
Thomas Eiter , Wolfgang Faber , Nicola Leone , Gerald Pfeifer , Axel Polleres, Answer set planning under action costs, Journal of Artificial Intelligence Research, v.19 n.1, p.25-71, July 2003
Heidi E. Dixon , Matthew L. Ginsberg , Andrew J. Parkes, Generalizing Boolean satisfiability I: background and survey of existing work, Journal of Artificial Intelligence Research, v.21 n.1, p.193-243, January 2004
Joxan Jaffar , Andrew E. Santosa , Razvan Voicu, Efficient memoization for dynamic programming with ad-hoc constraints, Proceedings of the 23rd national conference on Artificial intelligence, p.297-303, July 13-17, 2008, Chicago, Illinois
Eyal Amir , Allen Chang, Learning partially observable deterministic action models, Journal of Artificial Intelligence Research, v.33 n.1, p.349-402, September 2008
Federico Heras , Javier Larrosa , Albert Oliveras, MINIMAXSAT: an efficient weighted max-SAT solver, Journal of Artificial Intelligence Research, v.31 n.1, p.1-32, January 2008
Robert Mateescu , Rina Dechter , Radu Marinescu, AND/OR multi-valued decision diagrams (AOMDDs) for graphical models, Journal of Artificial Intelligence Research, v.33 n.1, p.465-519, September 2008
Fahiem Bacchus , Shannon Dalmao , Toniann Pitassi, Solving #SAT and Bayesian inference with backtracking search, Journal of Artificial Intelligence Research, v.34 n.1, p.391-442, January 2009
Knot Pipatsrisawat , Adnan Darwiche, A new clause learning scheme for efficient unsatisfiability proofs, Proceedings of the 23rd national conference on Artificial intelligence, p.1481-1484, July 13-17, 2008, Chicago, Illinois
Gilles Audemard , Laurent Simon, GUNSAT: a greedy local search algorithm for unsatisfiability, Proceedings of the 20th international joint conference on Artifical intelligence, p.2256-2261, January 06-12, 2007, Hyderabad, India
Jinbo Huang, The effect of restarts on the efficiency of clause learning, Proceedings of the 20th international joint conference on Artifical intelligence, p.2318-2323, January 06-12, 2007, Hyderabad, India
Matthew Kitching , Fahiem Bacchus, Symmetric component caching, Proceedings of the 20th international joint conference on Artifical intelligence, p.118-124, January 06-12, 2007, Hyderabad, India
Christophe Lecoutre , Fred Hemery, A study of residual supports in arc consistency, Proceedings of the 20th international joint conference on Artifical intelligence, p.125-130, January 06-12, 2007, Hyderabad, India
Christophe Lecoutre , Lakhdar Sais , Sébastien Tabary , Vincent Vidal, Nogood recording from restarts, Proceedings of the 20th international joint conference on Artifical intelligence, p.131-136, January 06-12, 2007, Hyderabad, India
Martin Gebser , Benjamin Kaufmann , André Neumann , Torsten Schaub, Conflict-driven answer set solving, Proceedings of the 20th international joint conference on Artifical intelligence, p.386-392, January 06-12, 2007, Hyderabad, India
Elena Kelareva , Olivier Buffet , Jinbo Huang , Sylvie Thiébaux, Factored planning using decomposition trees, Proceedings of the 20th international joint conference on Artifical intelligence, p.1942-1947, January 06-12, 2007, Hyderabad, India
Tian Sang , Paul Beame , Henry Kautz, A dynamic approach to MPE and weighted MAX-SAT, Proceedings of the 20th international joint conference on Artifical intelligence, p.173-179, January 06-12, 2007, Hyderabad, India
Fangzhen Lin , Pingzhong Tang, Computer-aided proofs of arrow's and other impossibility theorems, Proceedings of the 23rd national conference on Artificial intelligence, p.114-119, July 13-17, 2008, Chicago, Illinois
Agostino Dovier , Andrea Formisano , Enrico Pontelli, An experimental comparison of constraint logic programming and answer set programming, Proceedings of the 22nd national conference on Artificial intelligence, p.1622-1625, July 22-26, 2007, Vancouver, British Columbia, Canada
Paul Beanie , Henry Kautz , Ashish Sabharwal, Understanding the power of clause learning, Proceedings of the 18th international joint conference on Artificial intelligence, p.1194-1201, August 09-15, 2003, Acapulco, Mexico
Adriana Lopez , Fahiem Bacchus, Generalizing GraphPlan by formulating planning as a CSP, Proceedings of the 18th international joint conference on Artificial intelligence, p.954-960, August 09-15, 2003, Acapulco, Mexico
Fadi A. Aloul , Karem A. Sakallah , Igor L. Markov, Efficient symmetry breaking for boolean satisfiability, Proceedings of the 18th international joint conference on Artificial intelligence, p.271-276, August 09-15, 2003, Acapulco, Mexico
Alessandro Cimatti , Charles Pecheur , Roberto Cavada, Formal verification of diagnosability via symbolic model checking, Proceedings of the 18th international joint conference on Artificial intelligence, p.363-369, August 09-15, 2003, Acapulco, Mexico
Jinbo Huang , Adnan Darwiche, A structure-based variable ordering heuristic for SAT, Proceedings of the 18th international joint conference on Artificial intelligence, p.1167-1172, August 09-15, 2003, Acapulco, Mexico
Ryan Williams , Carla P. Gomes , Bart Selman, Backdoors to typical case complexity, Proceedings of the 18th international joint conference on Artificial intelligence, p.1173-1178, August 09-15, 2003, Acapulco, Mexico
Jinbo Huang , Adnan Darwiche, DPLL with a trace: from SAT to knowledge compilation, Proceedings of the 19th international joint conference on Artificial intelligence, p.156-162, July 30-August 05, 2005, Edinburgh, Scotland
Jörg Hoffmann , Sebastian Kupferschmid, A covering problem for hypercubes, Proceedings of the 19th international joint conference on Artificial intelligence, p.1523-1524, July 30-August 05, 2005, Edinburgh, Scotland
Deepak Ramachandran , Eyal Amir, Compact propositional encodings of first-order theories, Proceedings of the 19th international joint conference on Artificial intelligence, p.1579-1580, July 30-August 05, 2005, Edinburgh, Scotland
Roberto Sebastiani , Michele Vescovi, Automated reasoning in modal and description logics via SAT encoding: the case study of KmALC-satisfiability, Journal of Artificial Intelligence Research, v.35 n.1, p.343-389, May 2009

INDEX TERMS

Primary Classification:
  J. Computer Applications

Additional Classification:
  B. Hardware
  B.8 Performance and Reliability

  C. Computer Systems Organization

  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Complexity of proof procedures


General Terms:
Algorithms, Experimentation, Measurement, Performance, Theory, Verification


Keywords:
boolean satisfiability, design verification

Collaborative Colleagues:
Matthew W. Moskewicz: colleagues
Conor F. Madigan: colleagues
Ying Zhao: colleagues
Lintao Zhang: colleagues
Sharad Malik: colleagues

The ACM Portal is published by the Association for Computing Machinery. Copyright © 2009 ACM, Inc.
Terms of Usage   Privacy Policy   Code of Ethics   Contact Us

Useful downloads: Adobe Acrobat    QuickTime    Windows Media Player    Real Player