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 |
|