Search results for "DPLL"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
137	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
134	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
130	Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli	Abstract DPLL and Abstract DPLL Modulo Theories.	LPAR	2004	DBLP DOI BibTeX RDF
101	Matti Järvisalo, Tommi A. Junttila	Limitations of Restricted Branching in Clause Learning.	CP	2007	DBLP DOI BibTeX RDF
84	Roberto Sebastiani	From KSAT to Delayed Theory Combination: Exploiting DPLL Outside the SAT Domain.	FroCoS	2007	DBLP DOI BibTeX RDF
84	Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli	DPLL( T): Fast Decision Procedures.	CAV	2004	DBLP DOI BibTeX RDF
82	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
82	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
74	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
71	Kenneth L. McMillan, Andreas Kuehlmann, Mooly Sagiv	Generalizing DPLL to Richer Logics.	CAV	2009	DBLP DOI BibTeX RDF
71	Paolo Liberatore	Complexity results on DPLL and resolution.	ACM Trans. Comput. Log.	2006	DBLP DOI BibTeX RDF	Davis-Putnam, NP-completeness, propositional satisfiability
63	Carsten Sinz, Edda-Maria Dieringer	DPvis - A Tool to Visualize the Structure of SAT Instances.	SAT	2005	DBLP DOI BibTeX RDF
59	Robert Nieuwenhuis, Albert Oliveras	DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic.	CAV	2005	DBLP DOI BibTeX RDF
59	Michael Alekhnovich, Edward A. Hirsch, Dmitry Itsykson	Exponential Lower Bounds for the Running Time of DPLL Algorithms on Satisfiable Formulas.	ICALP	2004	DBLP DOI BibTeX RDF
59	Cesare Tinelli	A DPLL-Based Calculus for Ground Satisfiability Modulo Theories.	JELIA	2002	DBLP DOI BibTeX RDF
51	Stéphane Lescuyer, Sylvain Conchon	Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme.	FroCoS	2009	DBLP DOI BibTeX RDF
51	Clark W. Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli	Splitting on Demand in SAT Modulo Theories.	LPAR	2006	DBLP DOI BibTeX RDF
51	Romanelli Lodron Zuim, José T. de Sousa, Claudionor José Nunes Coelho Jr.	A Fast SAT Solver Strategy Based on Negated Clauses.	VLSI-SoC	2006	DBLP DOI BibTeX RDF
51	Gilles Audemard, Lakhdar Sais	A Symbolic Search Based Approach for Quantified Boolean Formulas.	SAT	2005	DBLP DOI BibTeX RDF	Satisfiability, Binary decision diagram, Quantified boolean formula
48	Anthony Monnet, Roger Villemaire	Scalable formula decomposition for propositional satisfiability.	C3S2E	2010	DBLP DOI BibTeX RDF	scalability, SAT, tree decomposition, propositional satisfiability, DPLL
48	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
48	Olga Tveretina	A Decision Procedure for Equality Logic with Uninterpreted Functions.	AISC	2004	DBLP DOI BibTeX RDF	equality logic with uninterpreted functions, DPLL procedure, satisfiability
48	Mohammad Ghasemzadeh 0001, Volker Klotz, Christoph Meinel	Embedding Memoization to the Semantic Tree Search for Deciding QBFs.	Australian Conference on Artificial Intelligence	2004	DBLP DOI BibTeX RDF	Zero-Suppressed Binary Decision Diagram (ZDD), Quantified Boolean Formula (QBF), QSAT, Satisfiability, DPLL
46	Adrian Balint, Michael Henn, Oliver Gableske	A Novel Approach to Combine a SLS- and a DPLL-Solver for the Satisfiability Problem.	SAT	2009	DBLP DOI BibTeX RDF
46	Leonardo Mendonça de Moura, Nikolaj S. Bjørner	Engineering DPLL(T) + Saturation.	IJCAR	2008	DBLP DOI BibTeX RDF
46	Bruno Dutertre, Leonardo Mendonça de Moura	A Fast Linear-Arithmetic Solver for DPLL(T).	CAV	2006	DBLP DOI BibTeX RDF
46	Cameron Brien, Sharad Malik	Understanding the Dynamic Behavior of Modern DPLL SAT Solvers through Visual Analysis.	FMCAD	2006	DBLP DOI BibTeX RDF
46	Allen Van Gelder	Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning.	LPAR	2005	DBLP DOI BibTeX RDF
46	Rémi Monasson	A Generating Function Method for the Average-Case Analysis of DPLL.	APPROX-RANDOM	2005	DBLP DOI BibTeX RDF
46	Anbulagan	Extending Unit Propagation Look-Ahead of DPLL Procedure.	PRICAI	2004	DBLP DOI BibTeX RDF
46	Jinbo Huang, Adnan Darwiche	Using DPLL for Efficient OBDD Construction.	SAT (Selected Papers	2004	DBLP DOI BibTeX RDF
46	Paul Beame, Russell Impagliazzo, Toniann Pitassi, Nathan Segerlind	Memoization and DPLL: Formula Caching Proof Systems.	CCC	2003	DBLP DOI BibTeX RDF
44	Carsten Sinz	Visualizing SAT Instances and Runs of the DPLL Algorithm.	J. Autom. Reason.	2007	DBLP DOI BibTeX RDF	SAT instance, DPLL procedure
38	Moshe Y. Vardi	Symbolic Techniques in Propositional Satisfiability Solving.	SAT	2009	DBLP DOI BibTeX RDF
38	Lei Fang 0002, Michael S. Hsiao	A new hybrid solution to boost SAT solver performance.	DATE	2007	DBLP DOI BibTeX RDF
38	Peter Baumgartner 0001, Alexander Fuchs 0003, Cesare Tinelli	Lemma Learning in the Model Evolution Calculus.	LPAR	2006	DBLP DOI BibTeX RDF
38	Fahiem Bacchus	CSPs: Adding Structure to SAT.	SAT	2006	DBLP DOI BibTeX RDF
38	Daijue Tang, Sharad Malik	Solving Quantified Boolean Formulas with Circuit Observability Don't Cares.	SAT	2006	DBLP DOI BibTeX RDF
38	Robert Nieuwenhuis, Albert Oliveras	Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools.	LPAR	2005	DBLP DOI BibTeX RDF
38	Peter Baumgartner 0001, Cesare Tinelli	The Model Evolution Calculus.	CADE	2003	DBLP DOI BibTeX RDF
38	Djamal Habet, Chu Min Li, Laure Devendeville, Michel Vasquez	A Hybrid Approach for SAT.	CP	2002	DBLP DOI BibTeX RDF
38	Lintao Zhang, Sharad Malik	Towards a Symmetric Treatment of Satisfaction and Conflicts in Quantified Boolean Formula Evaluation.	CP	2002	DBLP DOI BibTeX RDF
38	Peter Baumgartner 0001	FDPLL - A First Order Davis-Putnam-Longeman-Loveland Procedure.	CADE	2000	DBLP DOI BibTeX RDF
38	T. M. Almaida, Moisés Simões Piedade	High performance analog and digital PLL design.	ISCAS (4)	1999	DBLP DOI BibTeX RDF
36	Filip Maric	Formalization and Implementation of Modern SAT Solvers.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	Algorithms, Data structures, Software verification, DPLL, SAT solving
36	Ming-e Jing, Dian Zhou, Pushan Tang, Xiaofang Zhou, Hua Zhang 0019	Solving SAT problem by heuristic polarity decision-making algorithm.	Sci. China Ser. F Inf. Sci.	2007	DBLP DOI BibTeX RDF	complete algorithm, decision-making, DPLL, SAT problem
33	Carsten Sinz, Markus Iser	Problem-Sensitive Restart Heuristics for the DPLL Procedure.	SAT	2009	DBLP DOI BibTeX RDF
33	Eric I. Hsu, Sheila A. McIlraith	VARSAT: Integrating Novel Probabilistic Inference Techniques with DPLL Search.	SAT	2009	DBLP DOI BibTeX RDF	Survey Propagation/EMBP, Variable/Value Ordering Heuristics, Probabilistic Inference
33	Leonardo Mendonça de Moura, Nikolaj S. Bjørner	Deciding Effectively Propositional Logic Using DPLL and Substitution Sets.	IJCAR	2008	DBLP DOI BibTeX RDF
33	Dan Goldwasser, Ofer Strichman, Shai Fine	A Theory-Based Decision Heuristic for DPLL(T).	FMCAD	2008	DBLP DOI BibTeX RDF
33	Raihan H. Kibria	Evolving a Neural Net-Based Decision and Search Heuristic for DPLL SAT Solvers.	IJCNN	2007	DBLP DOI BibTeX RDF
33	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
33	Scott Cotton, Oded Maler	Fast and Flexible Difference Constraint Propagation for DPLL(T).	SAT	2006	DBLP DOI BibTeX RDF
33	Raihan H. Kibria, You Li	Optimizing the Initialization of Dynamic Decision Heuristics in DPLL SAT Solvers Using Genetic Programming.	EuroGP	2006	DBLP DOI BibTeX RDF
33	Dimitris Achlioptas, Paul Beame, Michael Molloy 0001	Exponential bounds for DPLL below the satisfiability threshold.	SODA	2004	DBLP BibTeX RDF
33	Markus Wedler, Dominik Stoffel, Wolfgang Kunz	Arithmetic Reasoning in DPLL-Based SAT Solving.	DATE	2004	DBLP DOI BibTeX RDF
33	Morten Irgens, William S. Havens	On Selection Strategies for the DPLL Algorithm.	Canadian AI	2004	DBLP DOI BibTeX RDF
33	Jader A. De Lima, Peterson R. Agostinho	A low-voltage low sensitivity sinusoidal VCO for DPLL realizations.	ISCAS (1)	2004	DBLP DOI BibTeX RDF
33	Christian Thiffault, Fahiem Bacchus, Toby Walsh	Solving Non-clausal Formulas with DPLL Search.	CP	2004	DBLP DOI BibTeX RDF
33	Anna Vasylenko, Orla Feely	Nonlinear dynamics of first-order DPLL with frequency-modulated input.	ISCAS (3)	2001	DBLP DOI BibTeX RDF
33	Ilias Panayiotopoulos, Phillip Constantinou	Performance Improvement of Nonuniform Polarity-DPLL Symbol Synchronizers by Using Novel Adaptive Statistical Loop Filtering Technique.	ISCC	2000	DBLP DOI BibTeX RDF
25	Dhadesugoor R. Vaman, Ashwin Ashok	An Efficient Distributed Synchronization Method for TD/CDMA based Mobile Ad Hoc Networks.	PerCom Workshops	2009	DBLP DOI BibTeX RDF
25	Jingchao Chen	Building a Hybrid SAT Solver via Conflict-Driven, Look-Ahead and XOR Reasoning Techniques.	SAT	2009	DBLP DOI BibTeX RDF	Conflict-driven, XOR reasoning, Hybrid solving technique, search pruning technique, Look-ahead, Boolean satisfiability (SAT)
25	Christopher Lynch, Duc-Khanh Tran	SMELS: Satisfiability Modulo Equality with Lazy Superposition.	ATVA	2008	DBLP DOI BibTeX RDF
25	Yong Gao 0001	Random Instances of W[2]-Complete Problems: Thresholds, Complexity, and Algorithms.	SAT	2008	DBLP DOI BibTeX RDF
25	Amit Stark, Dan Raphaeli	Combining Decision-Feedback Equalization and Carrier Recovery for Two-Dimensional Signal Constellations.	IEEE Trans. Commun.	2007	DBLP DOI BibTeX RDF
25	Jose Marcelo Lima Duarte, Francisco das Chagas Mota, Manoel J. M. Carvalho	Digital PM demodulator for brazilian data collecting system.	SBCCI	2007	DBLP DOI BibTeX RDF	BDCS, control system theory, FPGA, PLL, phase locked loop
25	Martin Davis	SAT: Past and Future.	SAT	2007	DBLP DOI BibTeX RDF
25	Roberto Cavada, Alessandro Cimatti, Anders Franzén, Krishnamani Kalyanasundaram, Marco Roveri, R. K. Shyamasundar	Computing Predicate Abstractions by Integrating BDDs and SMT Solvers.	FMCAD	2007	DBLP DOI BibTeX RDF
25	Michael Codish	Proving Termination with (Boolean) Satisfaction.	LOPSTR	2007	DBLP DOI BibTeX RDF
25	Mahmoud Fawzy Wagdy, Srishti Vaishnava	A Fast-Locking Digital Phase-Locked Loop.	ITNG	2006	DBLP DOI BibTeX RDF
25	Horst Samulowitz, Fahiem Bacchus	Binary Clause Reasoning in QBF.	SAT	2006	DBLP DOI BibTeX RDF
25	Himanshu Jain, Constantinos Bartzis, Edmund M. Clarke	Satisfiability Checking of Non-clausal Formulas Using General Matings.	SAT	2006	DBLP DOI BibTeX RDF
25	Peter Baumgartner 0001, Cesare Tinelli	The Model Evolution Calculus with Equality.	CADE	2005	DBLP DOI BibTeX RDF
25	Kameshwar Chandrasekar, Michael S. Hsiao	Q-PREZ: QBF Evaluation Using Partition, Resolution and Elimination with ZBDDs.	VLSI Design	2005	DBLP DOI BibTeX RDF
25	Sathiamoorthy Subbarayan, Dhiraj K. Pradhan	NiVER: Non-increasing Variable Elimination Resolution for Preprocessing SAT Instances.	SAT (Selected Papers	2004	DBLP DOI BibTeX RDF
25	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
25	Lintao Zhang, Sharad Malik	The Quest for Efficient Boolean Satisfiability Solvers.	CAV	2002	DBLP DOI BibTeX RDF
25	Gilles Audemard, Piergiorgio Bertoli, Alessandro Cimatti, Artur Kornilowicz, Roberto Sebastiani	A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions.	CADE	2002	DBLP DOI BibTeX RDF
25	Lintao Zhang, Sharad Malik	The Quest for Efficient Boolean Satisfiability Solvers.	CADE	2002	DBLP DOI BibTeX RDF
25	Alexey Teplinsky, Orla Feely	Phase-jitter dynamics in second-order DPLLs with irrational and integer input frequencies.	ISCAS (5)	1999	DBLP DOI BibTeX RDF
25	Benyong Zhang, Philip E. Allen	Feed-forward compensated high switching speed digital phase-locked loop frequency synthesizer.	ISCAS (4)	1999	DBLP DOI BibTeX RDF
23	Sandeep Kumar Singla, Pradeep Kumar Jaswal	Hybrid Satisfiability Techniques.	ITNG	2010	DBLP DOI BibTeX RDF	HybridSAT, Satisfiability, SAT, Boolean Satisfiability, DPLL
23	Mahmoud Fawzy Wagdy, Brandon Casey Cabrales	A Novel Flash Fast-Locking Digital Phase-Locked Loop.	ITNG	2009	DBLP DOI BibTeX RDF	lock time, coarse-tuning, fine-tuning, CMOS, DPLL
23	Chang-hong Shan, Zhong-ze Chen, Jin-xiong Jiang	An All Digital Phase-Locked Loop System with High Performance on Wideband Frequency Tracking.	HIS (3)	2009	DBLP DOI BibTeX RDF	All Digital Phase-Locked Loop (all DPLL), Wideband Frequency Tracking, FPGA, Filter, VHDL
23	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
23	Xiaolue Lai, Jaijeet S. Roychowdhury	A multilevel technique for robust and efficient extraction of phase macromodels of digitally controlled oscillators.	DAC	2006	DBLP DOI BibTeX RDF	DCO, PPV, simulation, PLL, macromodel, VCO, DPLL
21	Lili Chen, Morteza Tavakoli Taba, Zainulabideen J. Khalifa, Andreia Cathelin, Ehsan Afshari	A Fast Back-to-Lock DPLL-Based 192-210-GHz Chirp Generator With +5.9-dBm Peak Output Power for Sub-THz Imaging and Sensing.	IEEE J. Solid State Circuits	2024	DBLP DOI BibTeX RDF
21	Zhi-Heng Kang, Shen-Iuan Liu	A 1.6-GHz DPLL Using Feedforward Phase-Error Cancellation.	IEEE J. Solid State Circuits	2023	DBLP DOI BibTeX RDF
21	Abdul Muqueem, Shanky Saxena, Govind Singh Patel	An Ultra-Low-Power C-Band FMCW Transmitter Using a Fast Settling Fractional-N DPLL and Ring-Based Pulse Injection Locking Oscillator.	J. Circuits Syst. Comput.	2023	DBLP DOI BibTeX RDF
21	Zirui Jin, Xiaoyu Shan, Ang Hu, Dongsheng Liu, Xuan Cheng, Jinsong Cui, Chengcheng Zhang, Jianming Lei	A DTC-based Fractional-N DPLL using probability-density-shaping spur immunity and Q-noise reduction techniques for IoT applications.	Microelectron. J.	2023	DBLP DOI BibTeX RDF
21	Marco Favorito	Forward LTLf Synthesis: DPLL At Work.	CoRR	2023	DBLP DOI BibTeX RDF
21	Dusan Guller	A DPLL Procedure with Dichotomous Branching for Propositional Product Logic.	CoRR	2023	DBLP DOI BibTeX RDF
21	Hai Duong, Linhan Li, ThanhVu Nguyen, Matthew B. Dwyer	A DPLL(T) Framework for Verifying Deep Neural Networks.	CoRR	2023	DBLP DOI BibTeX RDF
21	Ping Lu, Bupesh Pandita, Minhan Chen	Reference Clock Jitter Immunity by Accurate DPLL Bandwidth Control in a Multiple-link Die-to-Die Interface.	MWSCAS	2023	DBLP DOI BibTeX RDF
21	Jinghui Jiang, Zhenpei Huang, Qiao Xiang, Lu Tang 0004, Jiwu Shu	Poster: P4-DPLL: Accelerating SAT Solving Using Switching ASICs.	SIGCOMM	2023	DBLP DOI BibTeX RDF
21	Waleed Madany, Yuncheng Zhang, Ashbir Aviat Fadila, Hongye Huang, Junjun Qiu, Atsushi Shirane, Kenichi Okada	A Fully Synthesizable DPLL with Background Gain Mismatch Calibrated Feedforward Phase Noise Cancellation Path.	ESSCIRC	2023	DBLP DOI BibTeX RDF
21	Haoyang Shen, Hao Zheng, Daniel O'Hare, Deepu John, Barry Cardiff	Correcting ADC jitter using DPLL timing error signal.	NEWCAS	2023	DBLP DOI BibTeX RDF
21	Woosong Jung, Hyojun Kim, Yeonggeun Song, Kwang-Hoon Lee, Deog-Kyoon Jeong	A 0.991JS FFT-Based Fast-Locking, 0.82GHz-to-4.lGHz DPLL-Based lnput-Jitter-Filtering Clock Driver with Wide-Range Mode-Switching 8-Shaped LC Oscillator for DRAM Interfaces.	CICC	2023	DBLP DOI BibTeX RDF
21	Marco Favorito	Forward LTLf Synthesis: DPLL At Work.	OVERLAY@AI*IA	2023	DBLP BibTeX RDF