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
Digital Library logoTake a look at the new version of this page: [ beta version ]. Tell us what you think.
A machine program for theorem-proving
Full text PdfPdf (420 KB)
Source
Communications of the ACM archive
Volume 5 ,  Issue 7  (July 1962) table of contents
Pages: 394 - 397  
Year of Publication: 1962
ISSN:0001-0782
Authors
Martin Davis  Institute of Mathematical Sciences, New York Univ., New York
George Logemann  Institute of Mathematical Sciences, New York Univ., New York
Donald Loveland  Institute of Mathematical Sciences, New York Univ., New York
Publisher
ACM  New York, NY, USA
Bibliometrics
Downloads (6 Weeks): 49,   Downloads (12 Months): 424,   Citation Count: 327
Additional Information:

abstract   references   cited by   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/368273.368557
What is a DOI?

Warning: The download time has expired please click on the item to try again.


ABSTRACT

The programming of a proof procedure is discussed in connection with trial runs and possible improvements.


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
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]
 
2
GILMORE, P. C. A proof method for quantification theory. IBM J. Res. Dev. 4 (1960), 28-35.
 
3
PRAWITZ, DAG. An improved proof procedure. Theoria 26, 2 (1960), 102-139.

CITED BY  327
Joyce Friedman, A Computer Program for a Solvable Case of the Decision Problem, Journal of the ACM (JACM), v.10 n.3, p.348-356, July 1963
Renato Bruni, Approximating minimal unsatisfiable subformulae by means of adaptive core search, Discrete Applied Mathematics, v.130 n.2, p.85-100, 15 August 2003
Rina Dechter , Daniel Frost, Backjump-based backtracking for constraint satisfaction problems, Artificial Intelligence, v.136 n.2, p.147-188, April 2002
Dimitris Achlioptas, Setting 2 variables at a time yields a new lower bound for random 3-SAT (extended abstract), Proceedings of the thirty-second annual ACM symposium on Theory of computing, p.28-37, May 21-23, 2000, Portland, Oregon, United States
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
E. Goldberg , M. Prasad , R. Brayton, Using SAT for combinational equivalence checking, Proceedings of the conference on Design, automation and test in Europe, p.114-121, March 2001, Munich, Germany
Eli Ben-Sasson , Avi Wigderson, Short proofs are narrow—resolution made simple, Proceedings of the thirty-first annual ACM symposium on Theory of computing, p.517-526, May 01-04, 1999, Atlanta, Georgia, United States
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
Dimitris Achlioptas , Paul Beame , Michael Molloy, A sharp threshold in proof complexity, Proceedings of the thirty-third annual ACM symposium on Theory of computing, p.337-346, July 2001, Hersonissos, Greece
Chris Wilson , David L. Dill, Reliable verification using symbolic simulation with scalar values, Proceedings of the 37th conference on Design automation, p.124-129, June 05-09, 2000, Los Angeles, California, United States
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
Paul Beame , Richard Karp , Toniann Pitassi , Michael Saks, On the complexity of unsatisfiability proofs for random k-CNF formulas, Proceedings of the thirtieth annual ACM symposium on Theory of computing, p.561-571, May 24-26, 1998, Dallas, Texas, United States
Ross A. Overbeek, A New Class of Automated Theorem-Proving Algorithms, Journal of the ACM (JACM), v.21 n.2, p.191-200, April 1974
William F. Atchison , Samuel D. Conte , John W. Hamblen , Thomas E. Hull , Thomas A. Keenan , William B. Kehl , Edward J. McCluskey , Silvio O. Navarro , Werner C. Rheinboldt , Earl J. Schweppe , William Viavant , David M. Young, Jr., Curriculum 68: Recommendations for academic programs in computer science: a report of the ACM curriculum committee on computer science, Communications of the ACM, v.11 n.3, p.151-197, March 1968
João P. Marques-Silva , Karem A. Sakallah, Boolean satisfiability in electronic design automation, Proceedings of the 37th conference on Design automation, p.675-680, June 05-09, 2000, Los Angeles, California, United States
J. A. Robinson, Theorem-Proving on the Computer, Journal of the ACM (JACM), v.10 n.2, p.163-174, April 1963
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
Enrico Giunchiglia , Massimo Narizzano , Armando Tacchella, Backjumping for quantified Boolean logic satisfiability, Artificial Intelligence, v.145 n.1-2, p.99-120, April 2003
Edward A. Hirsch, Two new upper bounds for SAT, Proceedings of the ninth annual ACM-SIAM symposium on Discrete algorithms, p.521-530, January 25-27, 1998, San Francisco, California, United States
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
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
Patrik Simons , Ilkka Niemelá , Timo Soininen, Extending and implementing the stable model semantics, Artificial Intelligence, v.138 n.1-2, p.181-234, 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
Morten Heine Sørensen , Jens Peter Secher, From type inference to configuration, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
Claudio Castellini , Enrico Giunchiglia , Armando Tacchella, SAT-based planning in complex domains: concurrency, constraints and nondeterminism, Artificial Intelligence, v.147 n.1-2, p.85-117, July 2003
Franz Baader , Diego Calvanese , Deborah L. McGuinness , Daniele Nardi , Peter F. Patel-Schneider, Bibliography, The description logic handbook: theory, implementation, and applications, Cambridge University Press, New York, NY, 2003
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
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
Mary Sheeran , Gunnar Stålmarck, A Tutorial on Stålmarck‘s Proof Procedure for PropositionalLogic, Formal Methods in System Design, v.16 n.1, p.23-58, Jan 1,2000
Cynthia A. Brown , Larry Finkelstein , Paul Walton Purdom, Jr., Backtrack searching in the presence of symmetry, Nordic Journal of Computing, v.3 n.3, p.203-219, Fall 1996
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
Lyndon Drake , Alan Frisch , Toby Walsh, Combining inference and search for the propositional satisfiability problem, Eighteenth national conference on Artificial intelligence, p.982-982, July 28-August 01, 2002, Edmonton, Alberta, Canada
Adnan Darwiche, A compiler for deterministic, decomposable negation normal form, Eighteenth national conference on Artificial intelligence, p.627-634, July 28-August 01, 2002, Edmonton, Alberta, Canada
Yacine Boufkhad , Olivier Dubois , Maurice Nivat, Reconstructing (h,v)-convex 2-dimensional patterns of objects from approximate horizontal and vertical projections, Theoretical Computer Science, v.290 n.3, p.1647-1664, 3 January 2003
Renato Bruni , Antonio Sassano, A complete adaptive algorithm for propositional satisfiability, Discrete Applied Mathematics, v.127 n.3, p.523-534, 01 May 2003
David A. Plaisted , Armin Biere , Yunshan Zhu, A satisfiability procedure for quantified boolean formulae, Discrete Applied Mathematics, v.130 n.2, p.291-328, 15 August 2003
William E. Walsh , Makoto Yokoo , Katsutoshi Hirayama , Michael P. Wellman, On market-inspired approaches to propositional satisfiability, Artificial Intelligence, v.144 n.1-2, p.125-156, March 2003
Chu-Min Li , Sylvain Gérard, On the limit of branching rules for hard random unsatisfiable 3-SAT, Discrete Applied Mathematics, v.130 n.2, p.277-290, 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
Chu-Min Li, Equivalent literal propagation in the DLL procedure, Discrete Applied Mathematics, v.130 n.2, p.251-276, 15 August 2003
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
Stephen M. Majercik , Michael L. Littman, Contingent planning under uncertainty via stochastic satisfiability, Artificial Intelligence, v.147 n.1-2, p.119-162, July 2003
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
Paul E. Dunne , Peter McBurney, Optimal utterances in dialogue protocols, Proceedings of the second international joint conference on Autonomous agents and multiagent systems, July 14-18, 2003, Melbourne, Australia
Dimitris Achlioptas , Lefteris M. Kirousis , Evangelos Kranakis , Danny Krizanc, Rigorous results for random (2 + p)-SAT, Theoretical Computer Science, v.265 n.1_2, p.109-129, 08/28/2001
Dimitris Achlioptas , Paul Beame , Michael Molloy, A sharp threshold in proof complexity yields lower bounds for satisfiability search, Journal of Computer and System Sciences, v.68 n.2, p.238-268, March 2004
Maria Luisa Bonet , Nicola Galesi, Optimality of size-width tradeoffs for resolution, Computational Complexity, v.10 n.4, p.261-276, May 2002
Katarina Britz, Interval satisfiability, Proceedings of the 2004 annual research conference of the South African institute of computer scientists and information technologists on IT research in developing countries, p.244-248, October 04-06, 2004, Stellenbosch, Western Cape, South Africa
Albert Atserias , María Luisa Bonet, On the automatizability of resolution and related propositional proof systems, Information and Computation, v.189 n.2, p.182-201, March 15, 2004
Eli Ben-Sasson , Avi Wigderson, Short proofs are narrow—resolution made simple, Journal of the ACM (JACM), v.48 n.2, p.149-169, March 2001
Pavel Pudlák , Russell Impagliazzo, A lower bound for DLL algorithms for k-SAT (preliminary version), Proceedings of the eleventh annual ACM-SIAM symposium on Discrete algorithms, p.128-136, January 09-11, 2000, San Francisco, California, United States
J. Gu, Global Optimization for Satisfiability (SAT) Problem, IEEE Transactions on Knowledge and Data Engineering, v.6 n.3, p.361-381, June 1994
John Franco, Results related to threshold phenomena research in satisfiability: lower bounds, Theoretical Computer Science, v.265 n.1_2, p.147-157, 08/28/2001
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
J. F. Groote , H. Zantema, Resolution and binary decision diagrams cannot simulate each other polynomially, Discrete Applied Mathematics, v.130 n.2, p.157-171, 15 August 2003
Lei Zheng , Peter J. Stuckey, Improving SAT using 2SAT, Australian Computer Science Communications, v.24 n.1, p.331-340, January-February 2002
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
Jens Gramm , Edward A. Hirsch , Rolf Niedermeier , Peter Rossmanith, Worst-case upper bounds for MAX-2-SAT with an application to MAX-CUT, Discrete Applied Mathematics, v.130 n.2, p.139-155, 15 August 2003
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
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
Lenhart K. Schubert, A new characterization of probabilities in Bayesian networks, Proceedings of the 20th conference on Uncertainty in artificial intelligence, p.495-503, July 07-11, 2004, Banff, Canada
Jun Gu , Qian-Ping Gu , Ding-Zhu Du, Convergence Properties of Optimization Algorithms for the SAT Problem, IEEE Transactions on Computers, v.45 n.2, p.209-218, February 1996
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
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
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
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
Weixiong Zhang, Configuration landscape analysis and backbone guided local search: part I: Satisfiability and maximum satisfiability, Artificial Intelligence, v.158 n.1, p.1-26, September 2004
Frédéric Koriche , Jean Sallantin, A logical toolbox for knowledge approximation, Proceedings of the 8th conference on Theoretical aspects of rationality and knowledge, July 08-10, 2001, Siena, Italy
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
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
Hans Kleine Büning , Xishun Zhao, On the structure of some classes of minimal unsatisfiable formulas, Discrete Applied Mathematics, v.130 n.2, p.185-207, 15 August 2003
Eli Ben-Sasson, Size space tradeoffs for resolution, Proceedings of the thiry-fourth annual ACM symposium on Theory of computing, May 19-21, 2002, Montreal, Quebec, Canada
Claudia Fiorini , Enrico Martinelli , Fabio Massacci, How to fake an RSA signature by encoding modular root finding as a SAT problem, Discrete Applied Mathematics, v.130 n.2, p.101-127, 15 August 2003
Éric Grégoire , Bertrand Mazure, About the incremental validation of first-order stratified knowledge-based decision-support systems, Information Sciences—Informatics and Computer Science: An International Journal, v.142 n.1, p.117-129, May 2002
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
Simona Cocco , Rémi Monasson, Heuristic average-case analysis of the backtrack resolution of random 3-satisfiability instances, Theoretical Computer Science, v.320 n.2-3, p.345-372, June 14, 2004
Stefan Szeider, Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable, Journal of Computer and System Sciences, v.69 n.4, p.656-674, December 2004
Alberto Maria Segre , Sean Forman , Giovanni Resta , Andrew Wildenberg, Nagging: a scalable fault-tolerant paradigm for distributed search, Artificial Intelligence, v.140 n.1-2, p.71-106, September 2002
Manish Vachharajani , Neil Vachharajani , Sharad Malik , David I. August, Facilitating reuse in hardware models with enhanced type inference, Proceedings of the 2nd IEEE/ACM/IFIP international conference on Hardware/software codesign and system synthesis, September 08-10, 2004, Stockholm, Sweden
Marco Cadoli , Andrea Schaerf, Compiling problem specification into SAT, Artificial Intelligence, v.162 n.1-2, p.89-120, February 2005
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
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
Ramamohan Paturi , Pavel Pudlák , Michael E. Saks , Francis Zane, An improved exponential-time algorithm for k-SAT, Journal of the ACM (JACM), v.52 n.3, p.337-364, May 2005
Eyal Amir , Sheila McIlraith, Partition-based logical reasoning for first-order and propositional theories, Artificial Intelligence, v.162 n.1-2, p.49-88, February 2005
Jie Wang, Complete on average Boolean satisfiability, Journal of Complexity, v.18 n.4, p.1024-1036, December 2002
HoonSang Jin , Fabio Somenzi, Prime clauses for fast enumeration of satisfying assignments to boolean circuits, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, San Diego, California, USA
Jerome L. Paul , Michal Kouril , Kenneth A. Berman, A template library to facilitate teaching message passing parallel computing, ACM SIGCSE Bulletin, v.38 n.1, March 2006
G. Parthasarathy , M. K. Iyer , K. T. Cheng , F. Brewer, Structural search for RTL with predicate learning, Proceedings of the 42nd annual conference on Design automation, June 13-17, 2005, San Diego, California, USA
Paolo Liberatore, Complexity results on DPLL and resolution, ACM Transactions on Computational Logic (TOCL), v.7 n.1, p.84-107, January 2006
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
Yinlei Yu , Sharad Malik, Validating the result of a Quantified Boolean Formula (QBF) solver: theory and practice, Proceedings of the 2005 conference on Asia South Pacific design automation, January 18-21, 2005, Shanghai, China
Ji-Ae Shin , Ernest Davis, Processes and continuous change in a SAT-based planner, Artificial Intelligence, v.166 n.1-2, p.194-253, August 2005
Michael Alekhnovich , Jan Johannsen , Toniann Pitassi , Alasdair Urquhart, An exponential separation between regular and general resolution, Proceedings of the thiry-fourth annual ACM symposium on Theory of computing, May 19-21, 2002, Montreal, Quebec, Canada
Paul Beame , Joseph Culberson , David Mitchell , Cristopher Moore, The resolution complexity of random graphk-colorability, Discrete Applied Mathematics, v.153 n.1, p.25-47, 1 December 2005
John Franco, Typical case complexity of satisfiability algorithms and the threshold phenomenon, Discrete Applied Mathematics, v.153 n.1, p.89-123, 1 December 2005
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
Amol Dattatraya Mali, On quantified weighted MAX-SAT, Decision Support Systems, v.40 n.2, p.257-268, August 2005
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
Jakob Nordström, Narrow proofs may be spacious: separating space and width in resolution, Proceedings of the thirty-eighth annual ACM symposium on Theory of computing, May 21-23, 2006, Seattle, WA, USA
Alexis C. Kaporis , Lefteris M. Kirousis , Efthimios G. Lalas, The probabilistic analysis of a greedy satisfiability algorithm, Random Structures & Algorithms, v.28 n.4, p.444-480, July 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
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
Teresa Alsinet , Felip Manyà , Jordi Planes, An efficient solver for weighted Max-SAT, Journal of Global Optimization, v.41 n.1, p.61-73, May 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
Matti Järvisalo , Tommi Junttila , Ilkka Niemelä, Unrestricted vs restricted cut in a tableau method for Boolean circuits, Annals of Mathematics and Artificial Intelligence, v.44 n.4, p.373-399, August 2005
Haiou Shen , Hantao Zhang, Improving exact algorithms for MAX-2-SAT, Annals of Mathematics and Artificial Intelligence, v.44 n.4, p.419-436, August 2005
Steven A. Wolfman , Daniel S. Weld, Combining linear programming and satisfiability solving for resource planning, The Knowledge Engineering Review, v.16 n.1, p.85-99, March 2001
Etienne De Klerk , Hans Van Maaren , Joost P. Warners, Relaxations of the Satisfiability Problem Using Semidefinite Programming, Journal of Automated Reasoning, v.24 n.1-2, p.37-65, February 2000
Carla P. Gomes , Bart Selman , Nuno Crato , Henry Kautz, Heavy-Tailed Phenomena in Satisfiability and Constraint Satisfaction Problems, Journal of Automated Reasoning, v.24 n.1-2, p.67-100, February 2000
Jan Friso Groote , Joost P. Warners, The Propositional Formula Checker HeerHugo, Journal of Automated Reasoning, v.24 n.1-2, p.101-125, February 2000
Dmitry Tsarkov , Ian Horrocks , Peter F. Patel-Schneider, Optimizing Terminological Reasoning for Expressive Description Logics, Journal of Automated Reasoning, v.39 n.3, p.277-316, October 2007
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
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
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
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
Jörg Hoffmann , Ronen I. Brafman, Conformant planning via heuristic forward search: A new approach, Artificial Intelligence, v.170 n.6-7, p.507-541, May, 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
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
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
Youichi Hanatani , Takashi Horiyama , Kazuo Iwama, Density condensation of boolean formulas, Discrete Applied Mathematics, v.154 n.16, p.2263-2270, 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
Jan Krajíček, Substitutions into propositional tautologies, Information Processing Letters, v.101 n.4, p.163-167, February, 2007
Eugene Goldberg , Yakov Novikov, BerkMin: A fast and robust Sat-solver, Discrete Applied Mathematics, v.155 n.12, p.1549-1561, June, 2007
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
Katarina Britz , Tertia Hörne, A constraint-based decision procedure for the description logic ALCN, Proceedings of the 2006 annual research conference of the South African institute of computer scientists and information technologists on IT research in developing couuntries, p.230-237, October 09-11, 2006, Somerset West, South Africa
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
Brian C. Williams , Robert J. Ragno, Conflict-directed A* and its role in model-based embedded systems, Discrete Applied Mathematics, v.155 n.12, p.1562-1595, June, 2007
Robert Nieuwenhuis , Albert Oliveras, Fast congruence closure and extensions, Information and Computation, v.205 n.4, p.557-580, April, 2007
Henry Kautz , Bart Selman, The state of SAT, Discrete Applied Mathematics, v.155 n.12, p.1514-1524, June, 2007
Henry Kautz , Bart Selman, The state of SAT, Discrete Applied Mathematics, v.155 n.12, p.1514-1524, June, 2007
Hasan Amjad, Compressing Propositional Refutations, Electronic Notes in Theoretical Computer Science (ENTCS), 185, p.3-15, 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
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
Jean-Christophe Filliâtre , Sylvain Conchon, Type-safe modular hash-consing, Proceedings of the 2006 workshop on ML, September 16-16, 2006, Portland, Oregon, USA
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
Jeremy Bongio , Cyrus Katrak , Hai Lin , Christopher Lynch , Ralph Eric McGregor, Encoding First Order Proofs in SMT, Electronic Notes in Theoretical Computer Science (ENTCS), v.198 n.2, p.71-84, May, 2008
Karl-Heinz Pennemann, An Algorithm for Approximating the Satisfiability Problem of High-level Conditions, Electronic Notes in Theoretical Computer Science (ENTCS), v.213 n.1, p.75-94, May, 2008
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
Bahareh Badban , Jaco van de Pol , Olga Tveretina , Hans Zantema, Generalizing DPLL and satisfiability for equalities, Information and Computation, v.205 n.8, p.1188-1211, August, 2007
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
Loganathan Lingappan , Niraj K. Jha, Satisfiability-based automatic test program generation and design for testability for microprocessors, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, v.15 n.5, p.518-530, May 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
Nicolas Peltier, Extended resolution simulates binary decision diagrams, Discrete Applied Mathematics, v.156 n.6, p.825-837, March, 2008
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
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
Z. Khasidashvili , M. Skaba , D. Kaiss , Z. Hanna, Theoretical framework for compositional sequential hardware equivalence verification in presence of design constraints, Proceedings of the 2004 IEEE/ACM International conference on Computer-aided design, p.58-65, November 07-11, 2004
Allen Van Gelder, Another look at graph coloring via propositional satisfiability, Discrete Applied Mathematics, v.156 n.2, p.230-243, January, 2008
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
Enrico Giunchiglia , Armando Tacchella, A Subset-Matching Size-Bounded Cache for Testing Satisfiability in Modal Logics, Annals of Mathematics and Artificial Intelligence, v.33 n.1, p.39-67, September 2001
Hans van Maaren , Joost P. Warners, Solving Satisfiability Problems Using Elliptic Approximations. A Note on Volumes and Weights, Annals of Mathematics and Artificial Intelligence, v.37 n.3, p.273-283, March 2003
J. Franco , R. P. Swaminathan, Average case results for satisfiability algorithms under the random-clause-width model, Annals of Mathematics and Artificial Intelligence, v.20 n.1-4, p.357-391, 1997
Fumiaki Okushi, Parallel cooperative propositional theorem proving, Annals of Mathematics and Artificial Intelligence, v.26 n.1-4, p.59-85, 1999
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
Allen Van Gelder , Fumiaki Okushi, A propositional theorem prover to solve planning and other problems, Annals of Mathematics and Artificial Intelligence, v.26 n.1-4, p.87-112, 1999
John Franco, Some interesting research directions in satisfiability, Annals of Mathematics and Artificial Intelligence, v.28 n.1-4, p.7-15, 2000
Maria Paola Bonacina, A taxonomy of parallel strategies for deduction, Annals of Mathematics and Artificial Intelligence, v.29 n.1-4, p.223-257, 2000
M. Kacprzak , A. Lomuscio , W. Penczek, From Bounded to Unbounded Model Checking for Temporal Epistemic Logic, Fundamenta Informaticae, v.63 n.2-3, p.221-240, April 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
Bernard Jurkowiak , Chu Min Li , Gil Utard, A Parallelization Scheme Based on Work Stealing for a Class of SAT Solvers, Journal of Automated Reasoning, v.34 n.1, p.73-101, January 2005
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
Magdalena Kacprzak , Wojciech Penczek, Fully Symbolic Unbounded Model Checking for Alternating-time Temporal Logic1, Autonomous Agents and Multi-Agent Systems, v.11 n.1, p.69-89, July 2005
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
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
Sylvie Coste-Marquis , Pierre Marquis, On Stratified Belief Base Compilation, Annals of Mathematics and Artificial Intelligence, v.42 n.4, p.399-442, December 2004
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
Simona Cocco , Rémi Monasson, Restarts and Exponential Acceleration of the Davis–Putnam–Loveland–Logemann Algorithm: A Large Deviation Analysis of the Generalized Unit Clause Heuristic for Random 3-SAT, Annals of Mathematics and Artificial Intelligence, v.43 n.1-4, p.153-172, 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
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
Pierre Marquis , Nadège Porquet, Resource-Bounded Paraconsistent Inference, Annals of Mathematics and Artificial Intelligence, v.39 n.4, p.349-384, December 2003
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
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
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
Michael Alekhnovich , Edward A. Hirsch , Dmitry Itsykson, Exponential Lower Bounds for the Running Time of DPLL Algorithms on Satisfiable Formulas, Journal of Automated Reasoning, v.35 n.1-3, p.51-72, October 2005
Stefan Szeider, Backdoor Sets for DLL Subsolvers, Journal of Automated Reasoning, v.35 n.1-3, p.73-88, October 2005
Jan Johannsen, The Complexity of Pure Literal Elimination, Journal of Automated Reasoning, v.35 n.1-3, p.89-95, October 2005
Alan M. Frisch , Timothy J. Peugniez , Anthony J. Doggett , Peter W. Nightingale, Solving Non-Boolean Satisfiability Problems with Stochastic Local Search: A Comparison of Encodings, Journal of Automated Reasoning, v.35 n.1-3, p.143-179, October 2005
Éric Grégoire , Bertrand Mazure , Cédric Piette, Local-search Extraction of MUSes, Constraints, v.12 n.3, p.325-344, 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
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
Guoqiang Pan , Moshe Y. Vardi, Symbolic Techniques in Satisfiability Solving, Journal of Automated Reasoning, v.35 n.1-3, p.25-50, October 2005
Fabio Massacci , Laura Marraro, Logical Cryptanalysis as a SAT Problem, Journal of Automated Reasoning, v.24 n.1-2, p.165-203, February 2000
Irina Rish , Rina Dechter, Resolution versus Search: Two Strategies for SAT, Journal of Automated Reasoning, v.24 n.1-2, p.225-275, February 2000
Hantao Zhang , Mark Stickel, Implementing the Davis–Putnam Method, Journal of Automated Reasoning, v.24 n.1-2, p.277-296, February 2000
Wolfgang Kuuml;chlin , Carsten Sinz, Proving Consistency Assertions for Automotive Product Data Management, Journal of Automated Reasoning, v.24 n.1-2, p.145-163, February 2000
Eugene Goldberg, Proving Unsatisfiability of CNFs Locally, Journal of Automated Reasoning, v.28 n.4, p.417-434, May 2002
Edward A. Hirsch, New Worst-Case Upper Bounds for SAT, Journal of Automated Reasoning, v.24 n.4, p.397-420, May 2000
Holger H. Hoos , Thomas Stützle, Local Search Algorithms for SAT: An Empirical Evaluation, Journal of Automated Reasoning, v.24 n.4, p.421-481, May 2000
Ian Horrocks , Peter F. Patel-Schneider, Evaluating Optimized Decision Procedures for Propositional Modal K(m) Satisfiability, Journal of Automated Reasoning, v.28 n.2, p.173-204, February 2002
Michael L. Littman , Stephen M. Majercik , Toniann Pitassi, Stochastic Boolean Satisfiability, Journal of Automated Reasoning, v.27 n.3, p.251-296, October 2001
Allen Van Gelder, Autarky Pruning in Propositional Model Elimination Reduces Failure Redundancy, Journal of Automated Reasoning, v.23 n.2, p.137-193, August 1999
Thomas Vossen , Michael Ball , Amnon Lotem , Dana Nau, Applying integer programming to AI planning, The Knowledge Engineering Review, v.15 n.1, p.85-100, March 2000
Marc-Michel Corsini , Antoine Rauzy, Toupie: The µ-calculus over Finite Domains as a Constraint Language, Journal of Automated Reasoning, v.19 n.2, p.143-171, October 1997
David A. Plaisted , Yunshan Zhu, Ordered Semantic Hyper-Linking, Journal of Automated Reasoning, v.25 n.3, p.167-217, October 2000
Belaïd Benhamou , Mohamed Réda Saïdi, A new incomplete method for CSP inconsistency checking, Proceedings of the 23rd national conference on Artificial intelligence, p.229-234, July 13-17, 2008, Chicago, Illinois
Stefan Andrei , Wei Ngan Chin , Albert Mo Kim Cheng , Mihai Lupu, Automatic Debugging of Real-Time Systems Based on Incremental Satisfiability Counting, IEEE Transactions on Computers, v.55 n.7, p.830-842, July 2006
Roman Gershman , Maya Koifman , Ofer Strichman, An approach for extracting a small unsatisfiable core, Formal Methods in System Design, v.33 n.1-3, p.1-27, December 2008
Jonathan Edwards, No ifs, ands, or buts: uncovering the simplicity of conditionals, ACM SIGPLAN Notices, v.42 n.10, October 2007
Matteo Pradella , Stefano Crespi Reghizzi, A SAT-based parser and completer for pictures specified by tiling, Pattern Recognition, v.41 n.2, p.555-566, February, 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
Mark Chavira , Adnan Darwiche, On probabilistic inference by weighted model counting, Artificial Intelligence, v.172 n.6-7, p.772-799, April, 2008
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
Konstantin Kutzkov, New upper bound for the #3-SAT problem, Information Processing Letters, v.105 n.1, p.1-5, December, 2007
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
Steven Prestwich, Generalised graph colouring by a hybrid of local search and constraint programming, Discrete Applied Mathematics, v.156 n.2, p.148-158, January, 2008
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
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
Ian P. Gent , Peter Nightingale , Andrew Rowley , Kostas Stergiou, Solving quantified constraint satisfaction problems, Artificial Intelligence, v.172 n.6-7, p.738-771, April, 2008
Javier Larrosa , Federico Heras , Simon de Givry, A logical approach to efficient Max-SAT solving, Artificial Intelligence, v.172 n.2-3, p.204-233, February, 2008
Robert Cowen , Adam Kolany, Davis-Putnam Style Rules for Deciding Property S, Fundamenta Informaticae, v.79 n.1-2, p.5-15, January 2007
Joao Marques-Silva , Jordi Planes, Algorithms for maximum satisfiability using unsatisfiable cores, Proceedings of the conference on Design, automation and test in Europe, March 10-14, 2008, Munich, Germany
Markus Borschbach , Andre Exeler, A search agent for a Max-2sat memetic algorithm approach, Proceedings of the 7th WSEAS International Conference on Applied Computer and Applied Computational Science, p.284-289, April 06-08, 2008, Hangzhou, China
Marian Srebrny , Lidia Stȩpień, A Propositional Programming Environment for Linear Algebra, Fundamenta Informaticae, v.81 n.1-3, p.325-345, January 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
Joachim Biskup , Lena Wiese, Preprocessing for controlled query evaluation with availability policy, Journal of Computer Security, v.16 n.4, p.477-494, September 2008
Jakob Nordström , Johan Håstad, Towards an optimal separation of space and length in resolution, Proceedings of the 40th annual ACM symposium on Theory of computing, May 17-20, 2008, Victoria, British Columbia, Canada
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
Joao Marques-Silva, Model checking with Boolean Satisfiability, Journal of Algorithms, v.63 n.1-3, p.3-16, January, 2008
Lei Fang , Michael S. Hsiao, A fast approximation algorithm for MIN-ONE SAT, Proceedings of the conference on Design, automation and test in Europe, March 10-14, 2008, Munich, Germany
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
Hung Viet Le , Enrico Pontelli, Dynamic scheduling in parallel answer set programming solvers, Proceedings of the 2007 spring simulation multiconference, March 25-29, 2007, Norfolk, Virginia
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
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
Luca Pulina , Armando Tacchella, A self-adaptive multi-engine solver for quantified Boolean formulas, Constraints, v.14 n.1, p.80-116, March 2009
Arjen Hommersom , Peter j. f. Lucas , Patrick Van bommel, Checking the quality of clinical guidelines using automated reasoning tools, Theory and Practice of Logic Programming, v.8 n.5-6, p.611-641, November 2008
Enrico Pontelli , Tran cao Son , Omar Elkhatib, Justifications for logic programs under answer set semantics, Theory and Practice of Logic Programming, v.9 n.1, p.1-56, January 2009
Magnus Björk, First Order Stålmarck, Journal of Automated Reasoning, v.42 n.1, p.99-122, January 2009
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
Brian R. Gaines, Designing Visual Languages for Description Logics, Journal of Logic, Language and Information, v.18 n.2, p.217-250, April 2009
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
Zijiang Yang , Chao Wang , Aarti Gupta , Franjo Ivanvčić, Model checking sequential software programs via mixed symbolic analysis, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.14 n.1, p.1-26, January 2009
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
Alban Grastien , Anbulagan Anbulagan , Jussi Rintanen , Elena Kelareva, Diagnosis of discrete-event systems using satisfiability algorithms, Proceedings of the 22nd national conference on Artificial intelligence, p.305-310, July 22-26, 2007, Vancouver, British Columbia, Canada
Olga Tveretina , Wieger Wesselink, EufDpll - A Tool to Check Satisfiability of Equality Logic Formulas, Electronic Notes in Theoretical Computer Science (ENTCS), 225, p.405-420, January, 2009
Vibhav Gogate , Rina Dechter, Approximate counting by sampling the backtrack-free search space, Proceedings of the 22nd national conference on Artificial intelligence, p.198-203, July 22-26, 2007, Vancouver, British Columbia, Canada
Esben Rune Hansen , Henrik Reif Andersen, Interactive configuration with regular string constraints, Proceedings of the 22nd national conference on Artificial intelligence, p.217-223, 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
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
Tian Sang , Paul Bearne , Henry Kautz, Performing Bayesian inference by weighted model counting, Proceedings of the 20th national conference on Artificial intelligence, p.475-481, July 09-13, 2005, Pittsburgh, Pennsylvania
Stephen M. Majercik , Byron Boots, DC-SSAT: a divide-and-conquer approach to solving stochastic satisfiability problems efficiently, Proceedings of the 20th national conference on Artificial intelligence, p.416-422, 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
Zhi-Hong Tao , Cong-Hua Zhou , Zhong Chen , Li-Fu Wang, Bounded model checking of CTL, Journal of Computer Science and Technology, v.22 n.1, p.39-43, January 2007
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
Haiou Shen , Hantao Zhang, Study of lower bound functions for MAX-2-SAT, Proceedings of the 19th national conference on Artifical intelligence, p.185-190, July 25-29, 2004, San Jose, California
Fabian M. Suchanek , Mauro Sozio , Gerhard Weikum, SOFIE: a self-organizing framework for information extraction, Proceedings of the 18th international conference on World wide web, April 20-24, 2009, Madrid, Spain
Filip Marić, Formalization and Implementation of Modern SAT Solvers, Journal of Automated Reasoning, v.43 n.1, p.81-119, June 2009
Federico Heras , Javier Larrosa, New inference rules for efficient Max-SAT solving, Proceedings of the 21st national conference on Artificial intelligence, p.68-73, 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
Natarajan Shankar, Automated deduction for verification, ACM Computing Surveys (CSUR), v.41 n.4, p.1-56, October 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
Éric Grégoire , Bertrand Mazure , Cédric Piette, Extracting MUSes, Proceeding of the 2006 conference on ECAI 2006: 17th European Conference on Artificial Intelligence August 29 -- September 1, 2006, Riva del Garda, Italy, p.387-391, May 22, 2006
Pilar Dellunde, On the Multimodal Logic of Elementary Normative Systems, Proceeding of the 2007 conference on Artificial Intelligence Research and Development, p.57-66, June 13, 2007
Igor Stéphan, Boolean Propagation Based on Literals for Quantified Boolean Formulae, Proceeding of the 2006 conference on ECAI 2006: 17th European Conference on Artificial Intelligence August 29 -- September 1, 2006, Riva del Garda, Italy, p.452-456, May 22, 2006
Fedor V. Fomin , Fabrizio Grandoni , Dieter Kratsch, A measure & conquer approach for the analysis of exact algorithms, Journal of the ACM (JACM), v.56 n.5, p.1-32, August 2009
Uwe Egly , Martina Seidl , Stefan Woltran, A Solver for QBFs in Nonprenex Form, Proceeding of the 2006 conference on ECAI 2006: 17th European Conference on Artificial Intelligence August 29 -- September 1, 2006, Riva del Garda, Italy, p.477-481, 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
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
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
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
Chu Min Li , Felip Manyà , Jordi Planes, New inference rules for Max-SAT, Journal of Artificial Intelligence Research, v.30 n.1, p.321-359, September 2007
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
Jinbo Huang , Adnan Darwiche, The language of search, Journal of Artificial Intelligence Research, v.29 n.1, p.191-219, May 2007
Hoifung Poon , Pedro Domingos , Marc Sumner, A general method for reducing the complexity of relational inference and its application to MCMC, Proceedings of the 23rd national conference on Artificial intelligence, p.1075-1080, July 13-17, 2008, Chicago, Illinois
Philipp Hertel , Fahiem Bacchus , Toniann Pitassi , Allen Van Gelder, Clause learning can effectively P-simulate general propositional resolution, Proceedings of the 23rd national conference on Artificial intelligence, p.283-290, July 13-17, 2008, Chicago, Illinois
Matti Järvisalo , Tommi Junttila, On the power of top-down branching heuristics, Proceedings of the 23rd national conference on Artificial intelligence, p.304-309, July 13-17, 2008, Chicago, Illinois
Cynthia A. Brown , Paul Walton Purdom, How to search efficiently, Proceedings of the 7th international joint conference on Artificial intelligence, p.588-594, August 24-28, 1981, Vancouver, BC, Canada
Alexander Feldman , Gregory Provan , Arjan Van Gemund, Computing minimal diagnoses by greedy stochastic search, Proceedings of the 23rd national conference on Artificial intelligence, p.911-918, July 13-17, 2008, Chicago, Illinois
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
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
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
Jussi Rintanen, Constructing conditional plans by a theorem-prover, Journal of Artificial Intelligence Research, v.10 n.1, p.323-352, January 1999
Jussi Rintanen, Improvements to the evaluation of quantified boolean formulae, Proceedings of the 16th international joint conference on Artificial intelligence, p.1192-1197, July 31-August 06, 1999, Stockholm, Sweden
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
Chu Min Li , Anbulagan Anbulagan, Heuristics based on unit propagation for satisfiability problems, Proceedings of the 15th international joint conference on Artifical intelligence, p.366-371, August 23-29, 1997, Nagoya, Japan
Thierry Castell , Michel Cayrol, Hidden gold in random generation of SAT satisfiable instances, Proceedings of the 15th international joint conference on Artifical intelligence, p.372-377, August 23-29, 1997, Nagoya, Japan
Rouen I. Brafman, Reachability, relevance, resolution and the planning as satisfiability approach, Proceedings of the 16th international joint conference on Artificial intelligence, p.976-981, July 31-August 06, 1999, Stockholm, Sweden
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
Han Lin , Kaile Su, Exploiting inference rules to compute lower bounds for MAX-SAT solving, Proceedings of the 20th international joint conference on Artifical intelligence, p.2334-2339, January 06-12, 2007, Hyderabad, India
Steven Prestwich , Inês Lynce, Refutation by randomised general resolution, Proceedings of the 22nd national conference on Artificial intelligence, p.1667-1670, July 22-26, 2007, Vancouver, British Columbia, Canada
Daniel Große , Robert Wille , Gerhard W. Dueck , Rolf Drechsler, Exact multiple-control toffoli network synthesis with SAT techniques, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, v.28 n.5, p.703-715, May 2009
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
Marco Cadoli , Andrea Schaerf, Compiling problem specifications into SAT, Artificial Intelligence, v.162 n.1-2, p.89-120, February 2005
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
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
Weixiong Zhang , Ananda Rangan , Moshe Looks, Backbone guided local search for maximum satisfiability, Proceedings of the 18th international joint conference on Artificial intelligence, p.1179-1184, August 09-15, 2003, Acapulco, Mexico
Olivier Dubois , Gilles Dequen, A backbone-search heuristic for efficient solving of hard 3-SAT formulae, Proceedings of the 17th international joint conference on Artificial intelligence, p.248-253, August 04-10, 2001, Seattle, WA, USA
Enrico Giunchiglia , Massimo Narizzano , Armando Tacchella, Backjumping for quantified Boolean logic satisfiability, Proceedings of the 17th international joint conference on Artificial intelligence, p.275-281, August 04-10, 2001, Seattle, WA, USA
Ronen I. Brafman, A simplifier for propositional formulas with many binary clauses, Proceedings of the 17th international joint conference on Artificial intelligence, p.515-520, August 04-10, 2001, Seattle, WA, USA
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
Frédéric Lardeux , Frédéric Saubion , Jin-Kao Hao, Three truth values for the SAT and Max-SAT problems, Proceedings of the 19th international joint conference on Artificial intelligence, p.187-192, July 30-August 05, 2005, Edinburgh, Scotland
Javier Larrosa , Federico Heras, Resolution in Max-SAT and its relation to local consistency in weighted CSPs, Proceedings of the 19th international joint conference on Artificial intelligence, p.193-198, July 30-August 05, 2005, Edinburgh, Scotland
Mark Chavira , Adnan Darwiche, Compiling Bayesian networks with local structure, Proceedings of the 19th international joint conference on Artificial intelligence, p.1306-1312, 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
Thomas Stibor, Foundations of r-contiguous matching in negative selection for anomaly detection, Natural Computing: an international journal, v.8 n.3, p.613-641, September 2009
Romanelli Zuim , José T. de Sousa , Claudionor N. Coelho, A fast SAT solver algorithm best suited to reconfigurable hardware, Proceedings of the 19th annual symposium on Integrated circuits and systems design, August 28-September 01, 2006, Ouro Preto, MG, Brazil
Ashish Sabharwal, SymChaff: exploiting symmetry in a structure-aware satisfiability solver, Constraints, v.14 n.4, p.478-505, December 2009
Lukas Kroc , Ashish Sabharwal , Carla P. Gomes , Bart Selman, Integrating systematic and local search paradigms: a new strategy for MaxSAT, Proceedings of the 21st international jont conference on Artifical intelligence, p.544-551, July 11-17, 2009, Pasadena, California, USA
Knot Pipatsrisawat , Adnan Darwiche, A new d-DNNF-based bound computation algorithm for functional E-MAJSAT, Proceedings of the 21st international jont conference on Artifical intelligence, p.590-595, July 11-17, 2009, Pasadena, California, USA
Youssef Hamadi , Said Jabbour , Lakhdar Sais, Control-based clause sharing in parallel SAT solving, Proceedings of the 21st international jont conference on Artifical intelligence, p.499-504, July 11-17, 2009, Pasadena, California, USA
Koen Claessen , Niklas Een , Mary Sheeran , Niklas Sörensson , Alexey Voronov , Knut Åkesson, SAT-Solving in Practice, with a Tutorial Example from Supervisory Control, Discrete Event Dynamic Systems, v.19 n.4, p.495-524, December 2009
Fadi A. Aloul , Mohamed El-Tarhuni, PN code acquisition using Boolean satisfiability techniques, Proceedings of the 2009 IEEE conference on Wireless Communications & Networking Conference, p.632-637, April 05-08, 2009, Budapest, Hungary
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
Eyal Amir , Sheila McIlraith, Partition-based logical reasoning for first-order and propositional theories, Artificial Intelligence, v.162 n.1-2, p.49-88, February 2005
Ji-Ae Shin , Ernest Davis, Processes and continuous change in a SAT-based planner, Artificial Intelligence, v.166 n.1-2, p.194-253, August 2005
Maria Paola Bonacina , Mnacho Echenim, Theory decision by decomposition, Journal of Symbolic Computation, v.45 n.2, p.229-260, February, 2010
Jürgen Bokowski , David Bremner , Gábor Gévay, Symmetric matroid polytopes and their generation, European Journal of Combinatorics, v.30 n.8, p.1758-1777, November, 2009
Florian Lonsing , Armin Biere, Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers, Electronic Notes in Theoretical Computer Science (ENTCS), 251, p.83-95, September, 2009
Asim Munawar , Mohamed Wahib , Masaharu Munetomo , Kiyoshi Akama, Hybrid of genetic algorithm and local search to solve MAX-SAT problem using nVidia CUDA framework, Genetic Programming and Evolvable Machines, v.10 n.4, p.391-415, December 2009
Pascal Vander-Swalmen , Gilles Dequen , Michaël Krajecki, A collaborative approach for multi-threaded SAT solving, International Journal of Parallel Programming, v.37 n.3, p.324-342, June 2009
Collaborative Colleagues:
Martin Davis: colleagues
George Logemann: colleagues
Donald Loveland: colleagues

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

Useful downloads: Adobe Acrobat    QuickTime    Windows Media Player    Real Player