Search results for "DPLL"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
21	Renato Bruni, Andrea Santori	New updating criteria for conflict-based branching heuristics in DPLL algorithms for satisfiability.	Discret. Optim.	2008	DBLP DOI BibTeX RDF
21	Jörg Hoffmann 0001, Carla P. Gomes, Bart Selman	Structure and Problem Hardness: Goal Asymmetry and DPLL Proofs in SAT-Based Planning	CoRR	2007	DBLP BibTeX RDF
21	Jörg Hoffmann 0001, Carla P. Gomes, Bart Selman	Structure and Problem Hardness: Goal Asymmetry and DPLL Proofs in SAT-Based Planning.	Log. Methods Comput. Sci.	2007	DBLP DOI BibTeX RDF
21	Bahareh Badban, Jaco van de Pol, Olga Tveretina, Hans Zantema	Generalizing DPLL and satisfiability for equalities.	Inf. Comput.	2007	DBLP DOI BibTeX RDF
21	Sava Krstic, Amit Goel	Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL.	FroCoS	2007	DBLP DOI BibTeX RDF
21	Romanelli Lodron Zuim	Uma heurística de decisão baseada na subtração de cubos para solucionadores DPLL do problema de satisfabilidade.		2007	RDF
21	Paul Beame, Russell Impagliazzo, Toniann Pitassi, Nathan Segerlind	Formula Caching in DPLL.	Electron. Colloquium Comput. Complex.	2006	DBLP BibTeX RDF
21	Jörg Hoffmann 0001, Carla P. Gomes, Bart Selman	Structure and Problem Hardness: Goal Asymmetry and DPLL Proofs in SAT-Based Planning.	ICAPS	2006	DBLP BibTeX RDF
21	Rémi Monasson	A generating function method for the average-case analysis of DPLL	CoRR	2005	DBLP BibTeX RDF
21	Jinbo Huang, Adnan Darwiche	DPLL with a Trace: From SAT to Knowledge Compilation.	IJCAI	2005	DBLP BibTeX RDF
21	Michael Alekhnovich, Edward A. Hirsch, Dmitry Itsykson	Exponential lower bounds for the running time of DPLL algorithms on satisfiable formulas	Electron. Colloquium Comput. Complex.	2004	DBLP BibTeX RDF
21	Barry O'Donnell, Orla Feely, Paul F. Curran, Ketan Mistry	Nonlinear dynamics of first-order DPLL with FM input and phase detector DC offset.	ICECS	2004	DBLP DOI BibTeX RDF
21	Olga Tveretin	DPLL-based Procedure for Equality Logic with Uninterpreted Functions.	IJCAR Doctoral Programme	2004	DBLP BibTeX RDF
21	Jinbo Huang, Adnan Darwiche	Using DPLL for Efficient OBDD Construction.	SAT	2004	DBLP BibTeX RDF
21	Harold S. Connamacher	A Random Constraint Satisfaction Problem That Seems Hard for DPLL.	SAT	2004	DBLP BibTeX RDF
21	Renato Bruni, Andrea Santori	Adding a New Conflict Based Branching Heuristic in two Evolved DPLL SAT Solvers.	SAT	2004	DBLP BibTeX RDF
21	Christian Thiffault, Fahiem Bacchus, Toby Walsh	Solving Non-clausal Formulas with DPLL search.	SAT	2004	DBLP BibTeX RDF
21	Fahiem Bacchus, Shannon Dalmao, Toniann Pitassi	DPLL with Caching: A new algorithm for #SAT and Bayesian Inference	Electron. Colloquium Comput. Complex.	2003	DBLP BibTeX RDF
21	Sergey I. Nikolenko	Hard satisfiable formulas for DPLL-type algorithms	CoRR	2003	DBLP BibTeX RDF
21	Paolo Liberatore	Complexity Results on DPLL and Resolution	CoRR	2002	DBLP BibTeX RDF
21	Inês Lynce, João Marques-Silva 0001	The Effect of Nogood Recording in DPLL-CBJ SAT Algorithms.	International Workshop on Constraint Solving and Constraint Logic Programming	2002	DBLP DOI BibTeX RDF
21	Michail G. Lagoudakis, Michael L. Littman	Learning to Select Branching Rules in the DPLL Procedure for Satisfiability.	Electron. Notes Discret. Math.	2001	DBLP DOI BibTeX RDF
21	Ilias Panayiotopoulos, Demosthenes G. Doumenis, Phillip Constantinou	Anti-hangup binary quantized DPLL technique for timing recovery in QAM symbol-rate sampled receivers.	IEEE Trans. Commun.	2001	DBLP DOI BibTeX RDF
21	Paolo Liberatore	On the complexity of choosing the branching literal in DPLL.	Artif. Intell.	2000	DBLP DOI BibTeX RDF
21	Ilias Panayiotopoulos, Phillip Constantinou	Adaptive statistical loop filtering technique for fast and reliable polarity-DPLL synchronizers.	ICASSP	2000	DBLP DOI BibTeX RDF
21	Alexander Podgorny, Orla C. Feely	Global nonlinear dynamics of second-order DPLL.	ISCAS	2000	DBLP DOI BibTeX RDF
21	Orla C. Feely	Nonlinear dynamics of first-order DPLL with FM input.	ISCAS	2000	DBLP DOI BibTeX RDF
21	Fabio Massacci	Reduction rules and universal variables for first order tableaux and DPLL.	KR	2000	DBLP BibTeX RDF
21	Ming Ouyang	How Good Are Branching Rules in DPLL?	Discret. Appl. Math.	1998	DBLP DOI BibTeX RDF
21	Byungjin Chun, Yong Hoon Lee, Beomsup Kim	Design of variable loop gains of dual-loop DPLL.	IEEE Trans. Commun.	1997	DBLP DOI BibTeX RDF
21	Byungjin Chun, Beomsup Kim, Yong Hong Lee	Adaptive Carrier Recovery Using Multi-Order DPLL for Mobile Communication Applications.	ISCAS	1995	DBLP DOI BibTeX RDF
21	Peter F. Driessen	DPLL bit synchronizer with rapid acquisition using adaptive Kalman filtering techniques.	IEEE Trans. Commun.	1994	DBLP DOI BibTeX RDF
21	Helmuth Brügel, Peter F. Driessen	Variable bandwidth DPLL bit synchronizer with rapid acquisition implemented as a finite state machine.	IEEE Trans. Commun.	1994	DBLP DOI BibTeX RDF
21	Yasunori Iwanami	A DSP DPLL demodulator with sequence estimation for MSK signal in the presence of Doppler shift on Rician fading channel.	PIMRC	1994	DBLP DOI BibTeX RDF
21	Beomup Kim	Digital carrier recovery with adaptive dual loop DPLL for mobile communication applications.	ICASSP (3)	1993	DBLP DOI BibTeX RDF
21	Beomsup Kim	Optical MMSE gear-shifting algorithm for the fast synchronization of DPLL.	ISCAS	1993	DBLP BibTeX RDF
21	Patrick G. Ogmundson, Peter F. Driessen	Zero-crossing DPLL bit synchronizer with pattern jitter compensation.	IEEE Trans. Commun.	1991	DBLP DOI BibTeX RDF
21	W. McCain, Clare D. McGillem	Performance Improvement of DPLL's in Non-Gaussian Noise Using Robust Estimators.	IEEE Trans. Commun.	1987	DBLP DOI BibTeX RDF
21	Werner Rosenkranz	Design and optimization of a digital FM receiver using DPLL techniques.	ICASSP	1985	DBLP DOI BibTeX RDF
21	Aldo N. D'Andrea, Franco Russo	Noise Analysis of a PSK Carrier Recovery DPLL.	IEEE Trans. Commun.	1983	DBLP DOI BibTeX RDF
21	Holly C. Osborne	Stability Analysis of an Nth Power Digital Phase-Locked Loop-Part I: First-Order DPLL.	IEEE Trans. Commun.	1980	DBLP DOI BibTeX RDF
21	Nunzio Aldo D'Andrea, Franco Russo	Multilevel Quantized DPLL Behavior with Phase- and Frequency-Step Plus Noise Input.	IEEE Trans. Commun.	1980	DBLP DOI BibTeX RDF
21	Holly C. Osborne	Stability Analysis of an Nth Power Digital Phase-Locked Loop-Part II: Second- and Third-Order DPLL's.	IEEE Trans. Commun.	1980	DBLP DOI BibTeX RDF
13	Peter Baumgartner 0001, Uwe Waldmann	Superposition and Model Evolution Combined.	CADE	2009	DBLP DOI BibTeX RDF
13	Albert Atserias, Johannes Klaus Fichte, Marc Thurley	Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution.	SAT	2009	DBLP DOI BibTeX RDF
13	Robert Nieuwenhuis	SAT Modulo Theories: Enhancing SAT with Special-Purpose Algorithms.	SAT	2009	DBLP DOI BibTeX RDF
13	HyoJung Han, Fabio Somenzi	On-the-Fly Clause Improvement.	SAT	2009	DBLP DOI BibTeX RDF
13	Mladen Nikolic, Filip Maric, Predrag Janicic	Instance-Based Selection of Policies for SAT Solvers.	SAT	2009	DBLP DOI BibTeX RDF
13	Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell	Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates.	SAT	2009	DBLP DOI BibTeX RDF
13	Christoph Wernhard	Tableaux for Projection Computation and Knowledge Compilation.	TABLEAUX	2009	DBLP DOI BibTeX RDF
13	Malay K. Ganai, Franjo Ivancic	Efficient decision procedure for non-linear arithmetic constraints using CORDIC.	FMCAD	2009	DBLP DOI BibTeX RDF
13	Peter Baumgartner 0001, Alexander Fuchs 0003, Cesare Tinelli	(LIA) - Model Evolution with Linear Integer Arithmetic Constraints.	LPAR	2008	DBLP DOI BibTeX RDF
13	Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell	Efficient Generation of Unsatisfiability Proofs and Cores in SAT.	LPAR	2008	DBLP DOI BibTeX RDF
13	Oliver Kullmann	Present and Future of Practical SAT Solving.	Complexity of Constraints	2008	DBLP DOI BibTeX RDF
13	Xiuqin Wang, Hao Wang, Guangsheng Ma	Hybrid SAT Solver Considering Circuit Observability.	ICYCS	2008	DBLP DOI BibTeX RDF
13	Arnaud Fietzke, Christoph Weidenbach	Labelled Splitting.	IJCAR	2008	DBLP DOI BibTeX RDF
13	Vadim Ryvchin, Ofer Strichman	Local Restarts.	SAT	2008	DBLP DOI BibTeX RDF
13	Eugene Goldberg	A Decision-Making Procedure for Resolution-Based SAT-Solvers.	SAT	2008	DBLP DOI BibTeX RDF
13	Omer Bar-Ilan, Oded Fuhrmann, Shlomo Hoory, Ohad Shacham, Ofer Strichman	Linear-Time Reductions of Resolution Proofs.	Haifa Verification Conference	2008	DBLP DOI BibTeX RDF
13	Pablo San Segundo, Cristóbal Tapia, Julio Puente, Diego Rodríguez-Losada	A New Exact Bit-Parallel Algorithm for SAT.	ICTAI (2)	2008	DBLP DOI BibTeX RDF
13	Djamal Habet	Enhancing the Robustness/Efficiency of Local Search Algorithms for SAT.	ICTAI (1)	2008	DBLP DOI BibTeX RDF
13	Chu Min Li, Felip Manyà, Nouredine Ould Mohamedou, Jordi Planes	Transforming Inconsistent Subformulas in MaxSAT Lower Bound Computation.	CP	2008	DBLP DOI BibTeX RDF
13	Jakob Nordström, Johan Håstad	Towards an optimal separation of space and length in resolution.	STOC	2008	DBLP DOI BibTeX RDF	length, lower bound, resolution, space, separation, pebbling, proof complexity
13	Martin Fränzle, Christian Herde	HySAT: An efficient proof engine for bounded model checking of hybrid systems.	Formal Methods Syst. Des.	2007	DBLP DOI BibTeX RDF	Verification, Hybrid systems, Satisfiability, Decision procedures, Bounded model checking, Infinite-state systems
13	Cormac de Frein, Anthony D. Fagan	Maximum Likelihood Frequency Detection for Discrete Hadamard Precoded OFDM.	VTC Spring	2007	DBLP DOI BibTeX RDF
13	Martin Lukasiewycz, Michael Glaß, Christian Haubelt, Jürgen Teich	SAT-decoding in evolutionary algorithms for discrete constrained optimization problems.	IEEE Congress on Evolutionary Computation	2007	DBLP DOI BibTeX RDF
13	Jianmin Zhang, ShengYu Shen, Sikun Li	Finding Unsatisfiable Subformulas with Stochastic Method.	IDEAL	2007	DBLP DOI BibTeX RDF	Unsatisfiable subformula, Resolution sequence, Refutation trace, Local search, Stochastic method
13	Guohua Liu, Jia-Huai You	On the Effectiveness of Looking Ahead in Search for Answer Sets.	LPNMR	2007	DBLP DOI BibTeX RDF
13	Yeting Ge, Clark W. Barrett, Cesare Tinelli	Solving Quantified Verification Conditions Using Satisfiability Modulo Theories.	CADE	2007	DBLP DOI BibTeX RDF
13	Knot Pipatsrisawat, Adnan Darwiche	A Lightweight Component Caching Scheme for Satisfiability Solvers.	SAT	2007	DBLP DOI BibTeX RDF
13	Cesare Tinelli	An Abstract Framework for Satisfiability Modulo Theories.	TABLEAUX	2007	DBLP DOI BibTeX RDF
13	Guohua Liu, Jia-Huai You	Adaptive Lookahead for Answer Set Computation.	ICTAI (2)	2007	DBLP DOI BibTeX RDF
13	Jianmin Zhang, ShengYu Shen, Sikun Li	A Heuristic Local Search Algorithm for Unsatisfiable Cores Extraction.	ICCSA (3)	2007	DBLP DOI BibTeX RDF	Unsatisfiable core, Unit clause propagation, Binary clause resolution, Equality reduction, Local search
13	Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio	Challenges in Satisfiability Modulo Theories.	RTA	2007	DBLP DOI BibTeX RDF
13	Alexander Hertel, Alasdair Urquhart	Game Characterizations and the PSPACE-Completeness of Tree Resolution Space.	CSL	2007	DBLP DOI BibTeX RDF
13	Shuvendu K. Lahiri, Robert Nieuwenhuis, Albert Oliveras	SMT Techniques for Fast Predicate Abstraction.	CAV	2006	DBLP DOI BibTeX RDF
13	HoonSang Jin, Fabio Somenzi	Strong conflict analysis for propositional satisfiability.	DATE	2006	DBLP DOI BibTeX RDF
13	Haripriya Janardhan, Mahmoud Fawzy Wagdy	Design of a 1GHz Digital PLL Using 0.18\mu m CMOS Technology.	ITNG	2006	DBLP DOI BibTeX RDF
13	Shilpa Ambarish, Mahmoud Fawzy Wagdy	A Wide-Band Digital Phase-Locked Looop.	ITNG	2006	DBLP DOI BibTeX RDF
13	Shujun Deng, Weimin Wu, Jinian Bian	Cooperative Bounded Model Checking Using STE and Hybrid Three-Valued SAT Solving.	CSCWD	2006	DBLP DOI BibTeX RDF
13	Adnan Darwiche	Searching While Keeping a Trace: The Evolution from Satisfiability to Knowledge Compilation.	IJCAR	2006	DBLP DOI BibTeX RDF
13	Hossein M. Sheini, Karem A. Sakallah	From Propositional Satisfiability to Satisfiability Modulo Theories.	SAT	2006	DBLP DOI BibTeX RDF
13	Eugene Goldberg	Determinization of Resolution by an Algorithm Operating on Complete Assignments.	SAT	2006	DBLP DOI BibTeX RDF
13	Hossein M. Sheini, Karem A. Sakallah	A Progressive Simplifier for Satisfiability Modulo Theories.	SAT	2006	DBLP DOI BibTeX RDF
13	Robert Nieuwenhuis, Albert Oliveras	On SAT Modulo Theories and Optimization Problems.	SAT	2006	DBLP DOI BibTeX RDF
13	Marc Thurley	sharpSAT - Counting Models with Advanced Component Caching and Implicit BCP.	SAT	2006	DBLP DOI BibTeX RDF
13	Hossein M. Sheini, Karem A. Sakallah	SMT(CLU): a step toward scalability in system verification.	ICCAD	2006	DBLP DOI BibTeX RDF
13	Chao Wang 0001, Aarti Gupta, Malay K. Ganai	Predicate learning and selective theory deduction for a difference logic solver.	DAC	2006	DBLP DOI BibTeX RDF	difference logic, SAT, decision procedure, SMT solver
13	Gabriel Istrate, Stefan Boettcher, Allon G. Percus	Spines of random constraint satisfaction problems: definition and connection with computational complexity.	Ann. Math. Artif. Intell.	2005	DBLP DOI BibTeX RDF	resolution complexity, constraint satisfaction problems, phase transitions, spine
13	Guoqiang Pan, Moshe Y. Vardi	Symbolic Techniques in Satisfiability Solving.	J. Autom. Reason.	2005	DBLP DOI BibTeX RDF	symbolic decision procedure, satisfiability, binary decision diagram
13	Bernard Jurkowiak, Chu Min Li, Gil Utard	A Parallelization Scheme Based on Work Stealing for a Class of SAT Solvers.	J. Autom. Reason.	2005	DBLP DOI BibTeX RDF	parallelism, automated theorem proving, SAT problem
13	Yang Ran, Qinfen Zheng, Isaac Weiss, Larry S. Davis, Wael Abd-Almageed, Liang Zhao	Pedestrian classification from moving platforms using cyclic motion pattern.	ICIP (2)	2005	DBLP DOI BibTeX RDF
13	Reiner Hähnle, Neil V. Murray, Erik Rosenthal	Normal Forms for Knowledge Compilation.	ISMIS	2005	DBLP DOI BibTeX RDF
13	Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz 0001, Roberto Sebastiani	The MathSAT 3 System.	CADE	2005	DBLP DOI BibTeX RDF
13	Nachum Dershowitz, Ziyad Hanna, Alexander Nadel	A Clause-Based Heuristic for SAT Solvers.	SAT	2005	DBLP DOI BibTeX RDF
13	Wei Wei 0040, Bart Selman	A New Approach to Model Counting.	SAT	2005	DBLP DOI BibTeX RDF
13	HoonSang Jin, Fabio Somenzi	CirCUs: A Hybrid Satisfiability Solver.	SAT (Selected Papers	2004	DBLP DOI BibTeX RDF
13	Armin Biere	Resolve and Expand.	SAT (Selected Papers	2004	DBLP DOI BibTeX RDF
13	Daijue Tang, Yinlei Yu, Darsh Ranjan, Sharad Malik	Analysis of Search Based Algorithms for Satisfiability of Propositional and Quantified Boolean Formulas Arising from Circuit State Space Diameter Problems.	SAT (Selected Papers	2004	DBLP DOI BibTeX RDF
13	Guoqiang Pan, Moshe Y. Vardi	Search vs. Symbolic Techniques in Satisfiability Solving.	SAT (Selected Papers	2004	DBLP DOI BibTeX RDF