Search results for "Davis-Putnam"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
149	Andreas Goerdt	Davis-Putnam Resolution versus Unrestricted Resolution.	CSL	1989	DBLP DOI BibTeX RDF
107	Philippe Chatalic, Laurent Simon	Multi-resolution on compressed sets of clauses.	ICTAI	2000	DBLP DOI BibTeX RDF	compressed sets, compressed clauses, propositional clauses, compression power, structured instances, specialized operator, clause sets, polynomial size data structures, ZREs system, Davis-Putnam procedure, hard problems, SAT provers, zero-suppressed binary decision diagrams, computational complexity, data structures, data structures, data compression, theorem proving, computability, encodings, directed graphs, binary decision diagrams, set theory, multi-resolution, cut eliminations, ZBDDs
107	Maria Luisa Bonet, Juan Luis Esteban, Nicola Galesi, Jan Johannsen	Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems.	FOCS	1998	DBLP DOI BibTeX RDF	Cutting Planes proof, tree-like proof, regular resolution, Davis-Putnam resolution, monotone real circuit, real communication complexity, lower bounds, resolution, propositional proof complexity
97	Wen-Tsuen Chen, Ming-Yi Fang	Theorem proving in propositional logic on vector computers using a generalized Davis-Putnam procedure.	SC	1990	DBLP DOI BibTeX RDF
81	David Eppstein	Quasiconvex analysis of multivariate recurrence equations for backtracking algorithms.	ACM Trans. Algorithms	2006	DBLP DOI BibTeX RDF	Automated analysis of algorithms, Davis-Putnam procedures, method of feasible directions, multivariate recurrences, quasiconvex programming, backtracking, worst-case analysis
71	Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli	Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T).	J. ACM	2006	DBLP DOI BibTeX RDF	SAT solvers, Satisfiability Modulo Theories
71	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.	Ann. Math. Artif. Intell.	2005	DBLP DOI BibTeX RDF	satisfiability, large deviations, restart, DPLL
71	Jussi Rintanen	Partial Implicit Unfolding in the Davis-Putnam Procedure for Quantified Boolean Formulae.	LPAR	2001	DBLP DOI BibTeX RDF
71	Peter Baumgartner 0001	FDPLL - A First Order Davis-Putnam-Longeman-Loveland Procedure.	CADE	2000	DBLP DOI BibTeX RDF
71	Enrico Giunchiglia, Roberto Sebastiani	Applying the Davis-Putnam Procedure to Non-clausal Formulas.	AI*IA	1999	DBLP DOI BibTeX RDF
55	Paolo Liberatore	Complexity results on DPLL and resolution.	ACM Trans. Comput. Log.	2006	DBLP DOI BibTeX RDF	Davis-Putnam, NP-completeness, propositional satisfiability
52	Dimitris Achlioptas, Paul Beame, Michael S. O. Molloy	A sharp threshold in proof complexity.	STOC	2001	DBLP DOI BibTeX RDF
52	Toby Walsh	SAT v CSP.	CP	2000	DBLP DOI BibTeX RDF
52	Fabio Massacci	Simplification: A General Constraint Propagation Technique for Propositional and Modal Tableaux.	TABLEAUX	1998	DBLP DOI BibTeX RDF
44	Oliver Kullmann, Xishun Zhao	On Davis-Putnam reductions for minimally unsatisfiable clause-sets.	Theor. Comput. Sci.	2013	DBLP DOI BibTeX RDF
44	Oliver Kullmann, Xishun Zhao	On Davis-Putnam reductions for minimally unsatisfiable clause-sets	CoRR	2012	DBLP BibTeX RDF
44	Oliver Kullmann, Xishun Zhao	On Davis-Putnam Reductions for Minimally Unsatisfiable Clause-Sets.	SAT	2012	DBLP DOI BibTeX RDF
44	Elazar Birnbaum, Eliezer L. Lozinskii	The Good Old Davis-Putnam Procedure Helps Counting Models	CoRR	2011	DBLP BibTeX RDF
44	Robert Cowen	Generalized Davis-Putnam and satisfiability problems in mathematics.	Log. J. IGPL	2010	DBLP DOI BibTeX RDF
44	Romanelli Lodron Zuim, José T. de Sousa, Claudionor Coelho	Decision heuristic for Davis Putnam, Loveland and Logemann algorithm satisfiability solving based on cube subtraction.	IET Comput. Digit. Tech.	2008	DBLP DOI BibTeX RDF
44	Robert Cowen, Adam Kolany	Davis-Putnam Style Rules for Deciding Property S.	Fundam. Informaticae	2007	DBLP BibTeX RDF
44	Paul Beame, Richard M. Karp, Toniann Pitassi, Michael E. Saks	The Efficiency of Resolution and Davis--Putnam Procedures.	SIAM J. Comput.	2002	DBLP DOI BibTeX RDF
44	Fahiem Bacchus	Enhancing Davis Putnam with Extended Binary Clause Reasoning.	AAAI/IAAI	2002	DBLP BibTeX RDF
44	Hantao Zhang 0001, Mark E. Stickel	Implementing the Davis-Putnam Method.	J. Autom. Reason.	2000	DBLP DOI BibTeX RDF
44	Chu Min Li	Integrating Equivalency Reasoning into Davis-Putnam Procedure.	AAAI/IAAI	2000	DBLP BibTeX RDF
44	Elazar Birnbaum, Eliezer L. Lozinskii	The Good Old Davis-Putnam Procedure Helps Counting Models.	J. Artif. Intell. Res.	1999	DBLP DOI BibTeX RDF
44	Jon W. Freeman	Hard Random 3-SAT Problems and the Davis-Putnam Procedure.	Artif. Intell.	1996	DBLP DOI BibTeX RDF
44	Nobuhiro Yugami	Theoretical Analysis of Davis-Putnam Procedure and Propositional Satisfiability.	IJCAI	1995	DBLP BibTeX RDF
44	Rina Dechter, Irina Rish	Directional Resolution: The Davis-Putnam Procedure, Revisited.	KR	1994	DBLP BibTeX RDF
44	Tomás E. Uribe, Mark E. Stickel	Ordered Binary Decision Diagrams and the Davis-Putnam Procedure.	CCL	1994	DBLP DOI BibTeX RDF
44	Richard J. Wallace, Eugene C. Freuder	Comparative studies of constraint satisfaction and Davis-Putnam algorithms for maximum satisfiability problems.	Cliques, Coloring, and Satisfiability	1993	DBLP DOI BibTeX RDF
44	Andreas Goerdt	Davis-Putnam Resolution versus Unrestricted Resolution.	Ann. Math. Artif. Intell.	1992	DBLP DOI BibTeX RDF
44	John Franco, Jacob Manuel Plotkin, John W. Rosenthal	Correction to probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem.	Discret. Appl. Math.	1987	DBLP DOI BibTeX RDF
44	John Franco, Marvin C. Paull	Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem.	Discret. Appl. Math.	1983	DBLP DOI BibTeX RDF
44	Allen Goldberg, Paul Walton Purdom Jr., Cynthia A. Brown	Average Time Analyses of Simplified Davis-Putnam Procedures.	Inf. Process. Lett.	1982	DBLP DOI BibTeX RDF
44	Zvi Galil	On the Complexity of Regular Resolution and the Davis-Putnam Procedure.	Theor. Comput. Sci.	1977	DBLP DOI BibTeX RDF
40	Martin Davis	SAT: Past and Future.	SAT	2007	DBLP DOI BibTeX RDF
26	Matti Järvisalo, Tommi A. Junttila	Limitations of restricted branching in clause learning.	Constraints An Int. J.	2009	DBLP DOI BibTeX RDF	Branching heuristics, Clause learning, Backdoor sets, Proof complexity, Propositional satisfiability, DPLL, Problem structure
26	Moshe Y. Vardi	Symbolic Techniques in Propositional Satisfiability Solving.	SAT	2009	DBLP DOI BibTeX RDF
26	Shai Haim, Toby Walsh	Restart Strategy Selection Using Machine Learning Techniques.	SAT	2009	DBLP DOI BibTeX RDF
26	Himanshu Jain, Edmund M. Clarke	Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts.	DAC	2009	DBLP DOI BibTeX RDF	NNF, verification, Boolean satisfiability, DPLL
26	Yuliya Lierler	Abstract Answer Set Solvers.	ICLP	2008	DBLP DOI BibTeX RDF
26	Wolfgang Faber 0001, Nicola Leone, Gerald Pfeifer, Francesco Ricca	On look-ahead heuristics in disjunctive logic programming.	Ann. Math. Artif. Intell.	2007	DBLP DOI BibTeX RDF	Mathematics Subject Classifications (2000) 68N17, 68T27, 68T20
26	Michael Codish	Proving Termination with (Boolean) Satisfaction.	LOPSTR	2007	DBLP DOI BibTeX RDF
26	Shujun Deng, Jinian Bian, Weimin Wu, Xiaoqing Yang, Yanni Zhao	EHSAT: An Efficient RTL Satisfiability Solver Using an Extended DPLL Procedure.	DAC	2007	DBLP DOI BibTeX RDF
26	Richard J. Wallace, Stuart Bain	Branching Rules for Satisfiability Analysed with Factor Analysis.	Australian Conference on Artificial Intelligence	2007	DBLP DOI BibTeX RDF
26	John N. Hooker	Duality in Optimization and Constraint Satisfaction.	CPAIOR	2006	DBLP DOI BibTeX RDF
26	Fedor V. Fomin, Fabrizio Grandoni 0001, Dieter Kratsch	Measure and conquer: a simple O(20.288n) independent set algorithm.	SODA	2006	DBLP DOI BibTeX RDF	exponential-time exact algorithms, independent set problem, NP-hard problems, algorithms and data structures
26	Romanelli Lodron Zuim, José T. de Sousa, Claudionor José Nunes Coelho Jr.	A fast SAT solver algorithm best suited to reconfigurable hardware.	SBCCI	2006	DBLP DOI BibTeX RDF	formal verification, SAT, CNF, DPLL
26	Matti Järvisalo, Tommi A. Junttila, Ilkka Niemelä	Unrestricted vs restricted cut in a tableau method for Boolean circuits.	Ann. Math. Artif. Intell.	2005	DBLP DOI BibTeX RDF	cut rule, satisfiability, proof complexity, Boolean circuits, DPLL
26	Michael Alekhnovich, Edward A. Hirsch, Dmitry Itsykson	Exponential Lower Bounds for the Running Time of DPLL Algorithms on Satisfiable Formulas.	J. Autom. Reason.	2005	DBLP DOI BibTeX RDF	DPLL algorithms, satisfiability
26	Madhu K. Iyer, Ganapathy Parthasarathy, Kwang-Ting Cheng	Efficient Conflict-Based Learning in an RTL Circuit Constraint Solver.	DATE	2005	DBLP DOI BibTeX RDF
26	Fedor V. Fomin, Fabrizio Grandoni 0001, Dieter Kratsch	Measure and Conquer: Domination - A Case Study.	ICALP	2005	DBLP DOI BibTeX RDF
26	Kevin Casey, David Gregg, M. Anton Ertl	Tiger - An Interpreter Generation Tool.	CC	2005	DBLP DOI BibTeX RDF
26	Carsten Sinz, Edda-Maria Dieringer	DPvis - A Tool to Visualize the Structure of SAT Instances.	SAT	2005	DBLP DOI BibTeX RDF
26	Rémi Monasson	A Generating Function Method for the Average-Case Analysis of DPLL.	APPROX-RANDOM	2005	DBLP DOI BibTeX RDF
26	Kameshwar Chandrasekar, Michael S. Hsiao	Q-PREZ: QBF Evaluation Using Partition, Resolution and Elimination with ZBDDs.	VLSI Design	2005	DBLP DOI BibTeX RDF
26	Natarajan Shankar	Inference Systems for Logical Algorithms.	FSTTCS	2005	DBLP DOI BibTeX RDF
26	Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli	Abstract DPLL and Abstract DPLL Modulo Theories.	LPAR	2004	DBLP DOI BibTeX RDF
26	David Eppstein	Quasiconvex analysis of backtracking algorithms.	SODA	2004	DBLP BibTeX RDF
26	Markus Wedler, Dominik Stoffel, Wolfgang Kunz	Arithmetic Reasoning in DPLL-Based SAT Solving.	DATE	2004	DBLP DOI BibTeX RDF
26	Anbulagan	Extending Unit Propagation Look-Ahead of DPLL Procedure.	PRICAI	2004	DBLP DOI BibTeX RDF
26	Morten Irgens, William S. Havens	On Selection Strategies for the DPLL Algorithm.	Canadian AI	2004	DBLP DOI BibTeX RDF
26	Haixia Jia, Cristopher Moore, Bart Selman	From Spin Glasses to Hard Satisfiable Formulas.	SAT (Selected Papers	2004	DBLP DOI BibTeX RDF
26	Haixia Jia, Cristopher Moore	How Much Backtracking Does It Take to Color Random Graphs? Rigorous Results on Heavy Tails.	CP	2004	DBLP DOI BibTeX RDF
26	Zhao Xing, Weixiong Zhang	Efficient Strategies for (Weighted) Maximum Satisfiability.	CP	2004	DBLP DOI BibTeX RDF
26	Poul Frederick Williams, Henrik Reif Andersen, Henrik Hulgaard	Satisfiability checking using Boolean Expression Diagrams.	Int. J. Softw. Tools Technol. Transf.	2003	DBLP DOI BibTeX RDF
26	Martin Fränzle, Christian Herde	Efficient SAT Engines for Concise Logics: Accelerating Proof Search for Zero-One Linear Constraint Systems.	LPAR	2003	DBLP DOI BibTeX RDF	non-clausal propositional logic, zero-one linear constraint systems, Satisfiability, proof search, acceleration techniques
26	Daniel Le Berre, Laurent Simon, Armando Tacchella	Challenges in the QBF Arena: the SAT'03 Evaluation of QBF Solvers.	SAT	2003	DBLP DOI BibTeX RDF
26	Reinhold Letz, Gernot Stenz	Universal Variables in Disconnection Tableaux.	TABLEAUX	2003	DBLP DOI BibTeX RDF
26	Anbulagan, John Thornton 0001, Abdul Sattar 0001	Dynamic Variable Filtering for Hard Random 3-SAT Problems.	Australian Conference on Artificial Intelligence	2003	DBLP DOI BibTeX RDF	Search, Constraints, Problem Solving
26	Lintao Zhang, Sharad Malik	The Quest for Efficient Boolean Satisfiability Solvers.	CAV	2002	DBLP DOI BibTeX RDF
26	Alexis C. Kaporis, Lefteris M. Kirousis, Efthimios G. Lalas	The Probabilistic Analysis of a Greedy Satisfiability Algorithm.	ESA	2002	DBLP DOI BibTeX RDF
26	Wenhui Zhang, Zhuo Huang, Jian Zhang 0001	Parallel Execution of Stochastic Search Procedures on Reduced SAT Instances.	PRICAI	2002	DBLP DOI BibTeX RDF
26	Lintao Zhang, Sharad Malik	The Quest for Efficient Boolean Satisfiability Solvers.	CADE	2002	DBLP DOI BibTeX RDF
26	Lintao Zhang, Sharad Malik	Towards a Symmetric Treatment of Satisfaction and Conflicts in Quantified Boolean Formula Evaluation.	CP	2002	DBLP DOI BibTeX RDF
26	Sherief Reda, Rolf Drechsler, Alex Orailoglu	On the Relation between SAT and BDDs for Equivalence Checking.	ISQED	2002	DBLP DOI BibTeX RDF
26	Francisco-Jesús Martín-Mateos, José-Antonio Alonso, María-José Hidalgo, José-Luis Ruiz-Reina	Verification in ACL2 of a Generic Framework to Synthesize SAT-Provers.	LOPSTR	2002	DBLP DOI BibTeX RDF
26	Takayuki Suyama, Makoto Yokoo, Hiroshi Sawada, Akira Nagoya	Solving satisfiability problems using reconfigurable computing.	IEEE Trans. Very Large Scale Integr. Syst.	2001	DBLP DOI BibTeX RDF
26	Maria Luisa Bonet, Nicola Galesi	Optimality of size-width tradeoffs for resolution.	Comput. Complex.	2001	DBLP DOI BibTeX RDF	complexity of proofs, automated theorem proving.¶ Subject classification. 03F20, 03B05, Resolution, 68T15
26	David Eppstein	Improved algorithms for 3-coloring, 3-edge-coloring, and constraint satisfaction.	SODA	2001	DBLP BibTeX RDF
26	Mati Tombak, Ain Isotamm, Tõnu Tamme	On Logical Method for Counting Dedekind Numbers.	FCT	2001	DBLP DOI BibTeX RDF
26	Poul Frederick Williams, Henrik Reif Andersen, Henrik Hulgaard	Satisfiability Checking Using Boolean Expression Diagrams.	TACAS	2001	DBLP DOI BibTeX RDF
26	Lyndon Drake	Automatic Generation of Implied Clauses for SAT.	CP	2001	DBLP DOI BibTeX RDF
26	Parosh Aziz Abdulla, Per Bjesse, Niklas Eén	Symbolic Reachability Analysis Based on SAT-Solvers.	TACAS	2000	DBLP DOI BibTeX RDF
26	Toby Walsh	Reformulating Propositional Satisfiability as Constraint Satisfaction.	SARA	2000	DBLP DOI BibTeX RDF
26	Ramón Béjar, Felip Manyà	Phase Transitions in the Regular Random 3-SAT Problem.	ISMIS	1999	DBLP DOI BibTeX RDF	regular CNF formulas, benchmarks, satisfiability, threshold, Multiple-valued logics, phase transitions
26	Maria Luisa Bonet, Nicola Galesi	A Study of Proof Search Algorithms for Resolution and Polynomial Calculus.	FOCS	1999	DBLP DOI BibTeX RDF
26	Ramón Béjar, Felip Manyà	A Comparison of Systematic and Local Search Algorithms for Regular CNF Formulas.	ESCQARU	1999	DBLP DOI BibTeX RDF
26	Zineb Habbas, Francine Herrmann, Daniel Singer, Michaël Krajecki	A Methodological Approach to Implement CSP on FPGA.	IEEE International Workshop on Rapid System Prototyping	1999	DBLP DOI BibTeX RDF
26	Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu	Symbolic Model Checking without BDDs.	TACAS	1999	DBLP DOI BibTeX RDF
26	Felip Manyà, Ramón Béjar, Gonzalo Escalada-Imaz	The satisfiability problem in regular CNF-formulas.	Soft Comput.	1998	DBLP DOI BibTeX RDF	Multiple-valued regular CNF-formulas, benchmarks, threshold, satisfiability problem
26	Fausto Giunchiglia, Roberto Sebastiani	Building Decision Procedures for Modal Logics from Propositional Decision Procedure - The Case Study of Modal K.	CADE	1996	DBLP DOI BibTeX RDF
26	Bernhard Beckert, Reiner Hähnle	Deduction by Combining Semantic Tableaux and Integer Programming.	CSL	1995	DBLP DOI BibTeX RDF
26	Jun Gu, Qian-Ping Gu	Average Time Complexity of the SAT 1.2 Algorithm.	ISAAC	1994	DBLP DOI BibTeX RDF
26	Peter Heusch, Ewald Speckenmeyer	Some Aspects of the Probabilistic Behavior of Variants of Resolution.	CSL	1991	DBLP DOI BibTeX RDF
26	Allen Van Gelder	A Satisfiability Tester for Non-Clausal Propositional Calculus.	CADE	1984	DBLP DOI BibTeX RDF