Symbolic model checking using SAT procedures instead of BDDs

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Symbolic model checking using SAT procedures instead of BDDs

Full text

Pdf (75 KB)

Source

Annual ACM IEEE Design Automation Conference archive
Proceedings of the 36th annual ACM/IEEE Design Automation Conference table of contents

New Orleans, Louisiana, United States

Pages: 317 - 320

Year of Publication: 1999

ISBN:1-58133-109-7

Authors

A. Biere	Computer Science Department, Carnegie Mellon University, 5000 Forbes Avenue, Pittsburgh, PA and Verysys Design Automation, Inc., 42707 Lawrence Place, Fremont, CA
A. Cimatti	Istituto per la Ricerca Scientifica e Tecnolgica (IRST), via Sommarive 18, 38055 Povo (TN), Italy
E. M. Clarke	Computer Science Department, Carnegie Mellon University, 5000 Forbes Avenue, Pittsburgh, PA and Verysys Design Automation, Inc., 42707 Lawrence Place, Fremont, CA
M. Fujita	Fujitsu Laboratories of America, Inc., 595 Lawrence Expressway, Sunnyvale, CA
Y. Zhu	Computer Science Department, Carnegie Mellon University, 5000 Forbes Avenue, Pittsburgh, PA and Verysys Design Automation, Inc., 42707 Lawrence Place, Fremont, CA

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): 11, Downloads (12 Months): 53, Citation Count: 93

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/309847.309942 What is a DOI?

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	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
	2	Arne Borälv, The Industrial Success of Verification Tools Based on Stålmarck's Method, Proceedings of the 9th International Conference on Computer Aided Verification, p.7-10, June 22-25, 1997
	3	Randal E. Bryant, Graph-based algorithms for Boolean function manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, Aug. 1986 [doi>10.1109/TC.1986.1676819]
	4	J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
	5	Edmund M. Clarke , E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic, Logic of Programs, Workshop, p.52-71, May 01, 1981
	6	Martin Davis , Hilary Putnam, A Computing Procedure for Quantification Theory, Journal of the ACM (JACM), v.7 n.3, p.201-215, July 1960 [doi>10.1145/321033.321034]
	7	David Déharbe , Anamaria Martins Moreira, Using induction and BDDs to model check invariants, Proceedings of the IFIP WG 10.5 International Conference on Correct Hardware Design and Verification Methods: Advances in Hardware Design and Verification, p.203-213, October 16-18, 1997
	8	Wolfgang Kunz, HANNIBAL: an efficient tool for logic verification based on recursive learning, Proceedings of the 1993 IEEE/ACM international conference on Computer-aided design, p.538-543, November 07-11, 1993, Santa Clara, California, United States
	9	MARTIN, A. J. The design of a self-timed circuit for distributed mutual exclusion. In Proceedings of the 1985 Chapel Hill Conference on Very Large Scale Integration (1985), H. Fuchs, Ed.
	10	Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
	11	Kenneth L. McMillan, A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking, Proceedings of the 8th International Conference on Computer Aided Verification, p.13-25, August 03, 1996
	12	MUKHERJEE, R., JAIN, J., TAKAYAMA, K., FUJITA, M., ABRA- HAM, J. A., AND FUSSELL, D. S. FLOVER: Filtering oriented combinational verification approach. In Proc. of International Workshop on Logic Synthesis (1995).
	13	David A. Plaisted , Steven Greenbaum, A structure-preserving clause form translation, Journal of Symbolic Computation, v.2 n.3, p.293-304, Sept. 1986 [doi>10.1016/S0747-7171(86)80028-1]
	14	SENTOVlCH, E. M., SINGH, K. J., LAVAGNO, L., M., C., MUR- GAI, R., SALDANHA, A., SAVOJ, H., STEPHAN, P. R., BRAYTON, R. K., AND SANGIOVANNI-VINCENTELLI, A. SIS: A System for Sequential Circuit Synthesis. Memorandum No. UCB/ERL M92/41, Electronics Research Laboratory, College of Engineering, University of California, Berkeley, 1992.
	15	STALMARCK, G. A system for determining propositional logic theorems by applying values and rules to triplets that are generated from a formula,1989. Swedish patent no. 467 076(1992), U.S. patent no. 5 276 897(1994), European patent no. 0404 454(1995).
	16	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 93

	S. Minato , S. Ishihara, Streaming BDD manipulation for large-scale combinatorial problems, Proceedings of the conference on Design, automation and test in Europe, p.702-707, March 2001, Munich, Germany
	Stephan Merz, Model checking: a tutorial overview, Modeling and verification of parallel processes, Springer-Verlag New York, Inc., New York, NY, 2001
	Scott Hazelhurst , Osnat Weissberg , Gila Kamhi , Limor Fix, A hybrid verification approach: getting deep into the design, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA
	Kazuhiro Nakamura , Shinji Maruoka , Shinji Kimura , Katsumasa Watanabe, Multi-clock path analysis using propositional satisfiability, Proceedings of the 2000 conference on Asia South Pacific design automation, p.81-86, January 2000, Yokohama, Japan
	Chung-Yang Huang , Kwang-Ting Cheng, Assertion checking by combined word-level ATPG and modular arithmetic constraint-solving techniques, Proceedings of the 37th conference on Design automation, p.118-123, June 05-09, 2000, Los Angeles, California, United States
	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
	Richard Raimi , Jacob Abraham, Detecting false timing paths: experiments on PowerPC microprocessors, Proceedings of the 36th ACM/IEEE conference on Design automation, p.737-741, June 21-25, 1999, New Orleans, Louisiana, 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
	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
	Shin-ichi Minato, Streaming BDD Manipulation, IEEE Transactions on Computers, v.51 n.5, p.474-485, May 2002
	Pankaj Chauhan , Edmund M. Clarke , Somesh Jha , Jim Kukula , Tom Shiple , Helmut Veith , Dong Wang, Non-linear quantification scheduling in image computation, Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, November 04-08, 2001, San Jose, California
	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
	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
	Pei Hsin Ho , Thomas Shiple , Kevin Harer , James Kukula , Robert Damiano , Valeria Bertacco , Jerry Taylor , Jiang Long, Smart simulation using collaborative formal and simulation engines, Proceedings of the 2000 IEEE/ACM international conference on Computer-aided design, November 05-09, 2000, San Jose, California
	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
	Edmund M. Clarke , Bernd-Holger Schlingloff, Model checking, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
	Beata Konikowska , Wojciech Penczek, Model checking for multi-valued computation tree logics, Beyond two: theory and applications of multiple-valued logic, Physica-Verlag GmbH, Heidelberg, Germany, 2003
	Jesse Whittemore , Joonyoung Kim , Karem Sakallah, SATIRE: a new incremental satisfiability engine, Proceedings of the 38th conference on Design automation, p.542-545, June 2001, Las Vegas, Nevada, United States
	Prasenjit Basu , Sayantan Das , Pallab Dasgupta , P. P. Chakrabarti, Discovering the input assumptions in specification refinement coverage, Proceedings of the 2006 conference on Asia South Pacific design automation, January 24-27, 2006, Yokohama, Japan
	Bijan Alizadeh, Word level functional coverage computation, Proceedings of the 2006 conference on Asia South Pacific design automation, January 24-27, 2006, Yokohama, Japan
	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
	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
	David Déharbe, A tutorial introduction to symbolic model checking, Logic for concurrency and synchronisation, Kluwer Academic Publishers, Norwell, MA, 2003
	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
	William N. N. Hung , Xiaoyu Song , Guowu Yang , Jin Yang , Marek Perkowski, Quantum logic synthesis by symbolic reachability analysis, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA
	Orna Grumberg , Flavio Lerda , Ofer Strichman , Michael Theobald, Proof-guided underapproximation-widening for multi-process systems, ACM SIGPLAN Notices, v.40 n.1, p.122-131, January 2005
	Edmund Clarke , Armin Biere , Richard Raimi , Yunshan Zhu, Bounded Model Checking Using Satisfiability Solving, Formal Methods in System Design, v.19 n.1, p.7-34, July 2001
	Orna Kupferman , Moshe Y. Vardi, Model Checking of Safety Properties, Formal Methods in System Design, v.19 n.3, p.291-314, November 2001
	Shuo Sheng , Michael S. Hsiao, Success-Driven Learning in ATPG for Preimage Computation, IEEE Design & Test, v.21 n.6, p.504-512, November 2004
	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
	Markus Wedler , Dominik Stoffel , Wolfgang Kunz, Normalization at the arithmetic bit level, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, San Diego, California, USA
	Bozena Woźna , Alessio Lomuscio , Wojciech Penczek, Bounded model checking for knowledge and real time, Proceedings of the fourth international joint conference on Autonomous agents and multiagent systems, July 25-29, 2005, The Netherlands
	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
	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
	Edmund Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , Helmut Veith, Counterexample-guided abstraction refinement for symbolic model checking, Journal of the ACM (JACM), v.50 n.5, p.752-794, September 2003
	Michael S. Hsiao , Shuo Sheng , Rajat Arora , Ankur Jain , Vamsi Boppana, Verification of large scale nano systems with unreliable nano devices, Nano, quantum and molecular computing: implications to high level design and validation, Kluwer Academic Publishers, Norwell, MA, 2004
	Frédéric Lardeux , Frédéric Saubion , Jin-Kao Hao, GASAT: a genetic local search algorithm for the satisfiability problem, Evolutionary Computation, v.14 n.2, p.223-253, June 2006
	Fumiaki Okushi , Allen Van Gelder, Persistent and Quasi-Persistent Lemmas in Propositional Model Elimination, Annals of Mathematics and Artificial Intelligence, v.40 n.3-4, p.373-401, March 2004
	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
	Eugene Goldberg , Yakov Novikov, BerkMin: A fast and robust Sat-solver, Discrete Applied Mathematics, v.155 n.12, p.1549-1561, June, 2007
	D. Tadesse , D. Sheffield , E. Lenge , R. I. Bahar , J. Grodstein, Accurate timing analysis using SAT and pattern-dependent delay models, Proceedings of the conference on Design, automation and test in Europe, April 16-20, 2007, Nice, France
	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
	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
	Malay K Ganai , Aarti Gupta, Accelerating high-level bounded model checking, Proceedings of the 2006 IEEE/ACM international conference on Computer-aided design, November 05-09, 2006, San Jose, California
	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
	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
	R. Armoni , S. Egorov , R. Fraer , D. Korchemny , M. Y. Vardi, Efficient LTL compilation for SAT-based model checking, Proceedings of the 2005 IEEE/ACM International conference on Computer-aided design, p.877-884, 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
	Bożena Woźna, ACTLS properties and Bounded Model Checking, Fundamenta Informaticae, v.63 n.1, p.65-87, January 2004
	Andrzej Zbrzezny, Improvements in SAT-based Reachability Analysis for Timed Automata, Fundamenta Informaticae, v.60 n.1-4, p.417-434, January 2004
	Cristian Coarfa , Demetrios D. Demopoulos , Alfonso San Miguel Aguirre , Devika Subramanian , Moshe Y. Vardi, Random 3-SAT: The Plot Thickens, Constraints, v.8 n.3, p.243-261, July 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
	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
	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
	Malay K. Ganai , Adnan Aziz, Improved SAT-based Bounded Reachability Analysis, Proceedings of the 2002 conference on Asia South Pacific design automation/VLSI Design, p.729, January 07-11, 2002
	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
	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
	Gianpiero Cabodi , Marco Crivellari , Sergio Nocco , Stefano Quer, Circuit Based Quantification: Back to State Set Manipulation within Unbounded Model Checking, Proceedings of the conference on Design, Automation and Test in Europe, p.688-689, 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
	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
	Guoqiang Pan , Moshe Y. Vardi, Symbolic Techniques in Satisfiability Solving, Journal of Automated Reasoning, v.35 n.1-3, p.25-50, October 2005
	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
	Per Bjesse , James Kukula, Using Counter Example Guided Abstraction Refinement to Find Complex Bugs, Proceedings of the conference on Design, automation and test in Europe, p.10156, February 16-20, 2004
	Daniel Kroening , Sanjit A. Seshia, Formal verification at higher levels of abstraction, Proceedings of the 2007 IEEE/ACM international conference on Computer-aided design, November 05-08, 2007, San Jose, California
	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
	Alessio Lomuscio , Wojciech Penczek , Bożena Woźna, Bounded model checking for knowledge and real time, Artificial Intelligence, v.171 n.16-17, p.1011-1038, November, 2007
	Assim Sagahyroon , Fadi A. Aloul, Using SAT-based techniques in power estimation, Microelectronics Journal, v.38 n.6-7, p.706-715, June, 2007
	Bożena Woźna , Andrzej Zbrzezny, Bounded Model Checking for the Existential Fragment of TCTL_{-G} and Diagonal Timed Automata, Fundamenta Informaticae, v.79 n.1-2, p.229-256, January 2007
	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
	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
	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
	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
	G. Cabodi , P. Camurati , M. Murciano, Automated abstraction by incremental refinement in interpolant-based model checking, Proceedings of the 2008 IEEE/ACM International Conference on Computer-Aided Design, November 10-13, 2008, San Jose, California
	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, Improving the Translation from ECTL to SAT, Fundamenta Informaticae, v.85 n.1-4, p.513-531, September 2008
	Zhi-Hong Tao , Hans Kleine Büning , Li-Fu Wang, Direct model checking matrix algorithm, Journal of Computer Science and Technology, v.21 n.6, p.944-949, November 2006
	Yung-Chih Chen , Chun-Yao Wang, Enhancing SAT-based sequential depth computation by pruning search space, Proceedings of the 19th ACM Great Lakes symposium on VLSI, May 10-12, 2009, Boston Area, MA, USA
	G. Cabodi , P. Camurati , L. Garcia , M. Murciano , S. Nocco , S. Quer, Trading-off SAT search and variable quantifications for effective unbounded model checking, Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design, p.1-8, November 17-20, 2008, Portland, Oregon
	J. Julliand , P. -A. Masson , E. Oudot, Partitioned PLTL model-checking for refined transition systems, Information and Computation, v.207 n.6, p.681-698, June, 2009
	Fadi A. Aloul , Karem A. Sakallah , Igor L. Markov, Efficient Symmetry Breaking for Boolean Satisfiability, IEEE Transactions on Computers, v.55 n.5, p.549-558, May 2006
	Emanuele Di Rosa , Enrico Giunchiglia , Marco Maratea, A new Approach for Solving Satisfiability Problems with Qualitative Preferences, Proceeding of the 2008 conference on ECAI 2008: 18th European Conference on Artificial Intelligence, p.510-514, June 27, 2008
	Matti Järvisalo , Tommi Junttila, Limitations of restricted branching in clause learning, Constraints, v.14 n.3, p.325-356, September 2009
	Liang Xu , Wei Chen , Yan-Yan Xu , Wen-Hui Zhang, Improved bounded model checking for the universal fragment of CTL, Journal of Computer Science and Technology, v.24 n.1, p.96-109, January 2009
	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
	Jôme Lang , Paolo Liberatore , Pierre Marquis, Propositional independence: formula-variable independence and forgetting, Journal of Artificial Intelligence Research, v.18 n.1, p.391-443, January 2003
	Lin Xu , Frank Hutter , Holger H. Hoos , Kevin Leyton-Brown, SATzilla: portfolio-based algorithm selection for SAT, Journal of Artificial Intelligence Research, v.32 n.1, p.565-606, May 2008
	Dafna Shahaf , Eyal Amir, Logical circuit filtering, Proceedings of the 20th international joint conference on Artifical intelligence, p.2611-2618, January 06-12, 2007, Hyderabad, India
	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
	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
	Moshe Y. Vardi, Automated verification: graphs, logic, and automata, Proceedings of the 18th international joint conference on Artificial intelligence, p.1603-1606, August 09-15, 2003, Acapulco, Mexico