Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
114 | Franc Brglez, Xiao Yu Li, Matthias F. M. Stallmann |
On SAT instance classes and a method for reliable performance experiments with SAT solvers. |
Ann. Math. Artif. Intell. |
2005 |
DBLP DOI BibTeX RDF |
exponential and heavy-tail distributions, reliability function, satisfiability, experimental design, equivalence classes, conjunctive normal form |
95 | Ramón Béjar, Alba Cabiscol, Cèsar Fernández, Felip Manyà, Carla P. Gomes |
Capturing Structure with Satisfiability. |
CP |
2001 |
DBLP DOI BibTeX RDF |
|
93 | Bernd Becker 0001, Valeria Bertacco, Rolf Drechsler, Masahiro Fujita |
09461 Abstracts Collection - Algorithms and Applications for Next Generation SAT Solvers. |
Algorithms and Applications for Next Generation SAT Solvers |
2009 |
DBLP BibTeX RDF |
|
89 | Ateet Bhalla, Inês Lynce, José T. de Sousa, João Marques-Silva 0001 |
Heuristic Backtracking Algorithms for SAT. |
MTV |
2003 |
DBLP DOI BibTeX RDF |
|
85 | Inês Lynce, João Marques-Silva 0001 |
Efficient data structures for backtrack search SAT solvers. |
Ann. Math. Artif. Intell. |
2005 |
DBLP DOI BibTeX RDF |
backtrack search, propositional satisfiability |
83 | Fadi A. Aloul, Arathi Ramani, Karem A. Sakallah, Igor L. Markov |
Solution and Optimization of Systems of Pseudo-Boolean Constraints. |
IEEE Trans. Computers |
2007 |
DBLP DOI BibTeX RDF |
Pseudo Boolean (PB), Max-ONE, Global Routing, Conjunctive Normal Form (CNF), Backtrack Search, Integer Linear Programming (ILP), Max-SAT, Boolean Satisfiability (SAT) |
83 | Ateet Bhalla, Inês Lynce, José T. de Sousa, João Marques-Silva 0001 |
Heuristic-Based Backtracking for Propositional Satisfiability. |
EPIA |
2003 |
DBLP DOI BibTeX RDF |
|
79 | Chu Min Li, Felip Manyà, Jordi Planes |
Exploiting Unit Propagation to Compute Lower Bounds in Branch and Bound Max-SAT Solvers. |
CP |
2005 |
DBLP DOI BibTeX RDF |
|
79 | Lintao Zhang, Sharad Malik |
Cache Performance of SAT Solvers: a Case Study for Efficient Implementation of Algorithms. |
SAT |
2003 |
DBLP DOI BibTeX RDF |
|
78 | Josep Argelich, Felip Manyà |
Partial Max-SAT Solvers with Clause Learning. |
SAT |
2007 |
DBLP DOI BibTeX RDF |
|
78 | 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 |
76 | Ateet Bhalla, Inês Lynce, José T. de Sousa, João Marques-Silva 0001 |
Heuristic-Based Backtracking Relaxation for Propositional Satisfiability. |
J. Autom. Reason. |
2005 |
DBLP DOI BibTeX RDF |
|
76 | Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah |
Generic ILP versus specialized 0-1 ILP: an update. |
ICCAD |
2002 |
DBLP DOI BibTeX RDF |
|
76 | Per Bjesse |
Industrial Model Checking Based on Satisfiability Solvers. |
SPIN |
2002 |
DBLP DOI BibTeX RDF |
|
76 | Louise Leenen, Anbulagan, Thomas Meyer 0002, Aditya K. Ghose |
Modeling and Solving Semiring Constraint Satisfaction Problems by Transformation to Weighted Semiring Max-SAT. |
Australian Conference on Artificial Intelligence |
2007 |
DBLP DOI BibTeX RDF |
|
72 | Knot Pipatsrisawat, Adnan Darwiche |
On the Power of Clause-Learning SAT Solvers with Restarts. |
CP |
2009 |
DBLP DOI BibTeX RDF |
|
72 | Bernd Becker 0001, V. Bertacoo, Rolf Drechsler, Masahiro Fujita (eds.) |
Algorithms and Applications for Next Generation SAT Solvers, 08.11. - 13.11.2009 |
Algorithms and Applications for Next Generation SAT Solvers |
2009 |
DBLP BibTeX RDF |
|
72 | Daniel Große, Hoang Minh Le 0001, Rolf Drechsler |
Formal Verification of Abstract SystemC Models. |
Algorithms and Applications for Next Generation SAT Solvers |
2009 |
DBLP BibTeX RDF |
|
72 | Martin Gogolla |
Towards Model Validation and Verification with SAT Techniques. |
Algorithms and Applications for Next Generation SAT Solvers |
2009 |
DBLP BibTeX RDF |
|
72 | Markus Wedler, Evgeny Pavlenko, Alexander Dreyer, Frank Seelisch, Dominik Stoffel, Gert-Martin Greuel, Wolfgang Kunz |
Solving hard instances in QF-BV combining Boolean reasoning with computer algebra. |
Algorithms and Applications for Next Generation SAT Solvers |
2009 |
DBLP BibTeX RDF |
|
72 | Erika Ábrahám, Ulrich Loup |
SMT-Solving for the First-Order Theory of the Reals. |
Algorithms and Applications for Next Generation SAT Solvers |
2009 |
DBLP BibTeX RDF |
|
72 | Robert Wille, Jean Christoph Jung, André Sülflow, Rolf Drechsler |
SWORD - Module-based SAT Solving. |
Algorithms and Applications for Next Generation SAT Solvers |
2009 |
DBLP BibTeX RDF |
|
70 | Peter Hawkins, Peter J. Stuckey |
A Hybrid BDD and SAT Finite Domain Constraint Solver. |
PADL |
2006 |
DBLP DOI BibTeX RDF |
|
70 | Florian Letombe, João Marques-Silva 0001 |
Improvements to Hybrid Incremental SAT Algorithms. |
SAT |
2008 |
DBLP DOI BibTeX RDF |
|
66 | Yinlei Yu, Cameron Brien, Sharad Malik |
Exploiting Circuit Reconvergence through Static Learning in CNF SAT Solvers. |
VLSI Design |
2008 |
DBLP DOI BibTeX RDF |
|
66 | Emmanuel Zarpas |
Benchmarking SAT Solvers for Bounded Model Checking. |
SAT |
2005 |
DBLP DOI BibTeX RDF |
|
66 | Jinbo Huang |
A Case for Simple SAT Solvers. |
CP |
2007 |
DBLP DOI BibTeX RDF |
|
66 | Emad Saad |
Probabilistic Reasoning by SAT Solvers. |
ECSQARU |
2009 |
DBLP DOI BibTeX RDF |
|
64 | 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 |
64 | Yinlei Yu, Sharad Malik |
Lemma Learning in SMT on Linear Constraints. |
SAT |
2006 |
DBLP DOI BibTeX RDF |
|
64 | Roman Gershman, Ofer Strichman |
Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas. |
SAT |
2005 |
DBLP DOI BibTeX RDF |
|
63 | Shinya Hiramoto, Masaki Nakanishi, Shigeru Yamashita, Yasuhiko Nakashima |
A Hardware SAT Solver Using Non-chronological Backtracking and Clause Recording Without Overheads. |
ARC |
2007 |
DBLP DOI BibTeX RDF |
|
63 | João Marques-Silva 0001, Inês Lynce |
Towards Robust CNF Encodings of Cardinality Constraints. |
CP |
2007 |
DBLP DOI BibTeX RDF |
|
63 | Alessandro Armando, Claudio Castellini, Enrico Giunchiglia, Fausto Giunchiglia, Armando Tacchella |
SAT-Based Decision Procedures for Automated Reasoning: A Unifying Perspective. |
Mechanizing Mathematical Reasoning |
2005 |
DBLP DOI BibTeX RDF |
|
63 | Olivier Bailleux, Pierre Marquis |
Some Computational Aspects of distance-sat. |
J. Autom. Reason. |
2006 |
DBLP DOI BibTeX RDF |
computational complexity, satisfiability |
60 | Cameron Brien, Sharad Malik |
Understanding the Dynamic Behavior of Modern DPLL SAT Solvers through Visual Analysis. |
FMCAD |
2006 |
DBLP DOI BibTeX RDF |
|
59 | Kenneth L. McMillan |
Methods for exploiting SAT solvers in unbounded model checking. |
MEMOCODE |
2003 |
DBLP DOI BibTeX RDF |
|
59 | Mate Soos, Karsten Nohl, Claude Castelluccia |
Extending SAT Solvers to Cryptographic Problems. |
SAT |
2009 |
DBLP DOI BibTeX RDF |
|
59 | Josep Argelich, Felip Manyà |
Exact Max-SAT solvers for over-constrained problems. |
J. Heuristics |
2006 |
DBLP DOI BibTeX RDF |
Soft constraints, Solvers, Max-SAT |
59 | Ilya Mironov, Lintao Zhang |
Applications of SAT Solvers to Cryptanalysis of Hash Functions. |
SAT |
2006 |
DBLP DOI BibTeX RDF |
|
59 | 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 |
59 | Sean Safarpour, Andreas G. Veneris, Rolf Drechsler |
Integrating observability don't cares in all-solution SAT solvers. |
ISCAS |
2006 |
DBLP DOI BibTeX RDF |
|
59 | Andreas Dandalis, Viktor K. Prasanna |
Run-time performance optimization of an FPGA-based deduction engine for SAT solvers. |
ACM Trans. Design Autom. Electr. Syst. |
2002 |
DBLP DOI BibTeX RDF |
reconfigurable components, reconfigurable computing, configurable, high performance, Boolean satisfiability, reconfigurable systems, Adaptive computing, performance trade-offs |
59 | Andreas Dandalis, Viktor K. Prasanna, Bharani Thiruvengadam |
Run-Time Performance Optimization of an FPGA-Based Deduction Engine for SAT Solvers. |
FPL |
2001 |
DBLP DOI BibTeX RDF |
|
57 | Leonardo Mendonça de Moura, Bruno Dutertre, Natarajan Shankar |
A Tutorial on Satisfiability Modulo Theories. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
57 | Guoqiang Pan, Moshe Y. Vardi |
Symbolic Decision Procedures for QBF. |
CP |
2004 |
DBLP DOI BibTeX RDF |
|
57 | Xiuqin Wang, Hao Wang, Guangsheng Ma |
Hybrid SAT Solver Considering Circuit Observability. |
ICYCS |
2008 |
DBLP DOI BibTeX RDF |
|
57 | Rolf Drechsler, Görschwin Fey, Sebastian Kinder |
An Integrated Approach for Combining BDD and SAT Provers. |
VLSI Design |
2006 |
DBLP DOI BibTeX RDF |
|
57 | Yogesh S. Mahajan, Zhaohui Fu, Sharad Malik |
Zchaff2004: An Efficient SAT Solver. |
SAT (Selected Papers |
2004 |
DBLP DOI BibTeX RDF |
|
57 | Pavel Surynek |
Solving Difficult SAT Instances Using Greedy Clique Decomposition. |
SARA |
2007 |
DBLP DOI BibTeX RDF |
difficult instances, search, consistency, SAT, clique |
57 | Ben Browning, Anja Remshagen |
A SAT-based solver for Q-ALL SAT. |
ACM Southeast Regional Conference |
2006 |
DBLP DOI BibTeX RDF |
learning, logic programming, quantified Boolean formula |
57 | Zhaohui Fu, Yinlei Yu, Sharad Malik |
Considering Circuit Observability Don't Cares in CNF Satisfiability. |
DATE |
2005 |
DBLP DOI BibTeX RDF |
|
54 | Nicolas T. Courtois, Sean O'Neil, Jean-Jacques Quisquater |
Practical Algebraic Attacks on the Hitag2 Stream Cipher. |
ISC |
2009 |
DBLP DOI BibTeX RDF |
Hitag 2 algorithm, MiFare Crypto-1 cipher, Gröbner bases, Boolean functions, stream ciphers, RFID tags, SAT solvers, algebraic cryptanalysis |
54 | Fabrício Vivas Andrade, Leandro Maia Silva, Antônio Otávio Fernandes |
BenCGen: a digital circuit generation tool for benchmarks. |
SBCCI |
2008 |
DBLP DOI BibTeX RDF |
benchmarks, sat solvers, combinational equivalence checking |
53 | Baiqiang Chen |
Strategies on Algebraic Attacks Using SAT Solvers. |
ICYCS |
2008 |
DBLP DOI BibTeX RDF |
|
53 | Tobias Eibach, Enrico Pilz, Gunnar Völkel |
Attacking Bivium Using SAT Solvers. |
SAT |
2008 |
DBLP DOI BibTeX RDF |
Rsat, Bivium, Gröbner Base, Cryptography, Application, Stream Cipher, BDD, SAT Solver, eSTREAM, Trivium |
53 | Eugene Goldberg |
A Decision-Making Procedure for Resolution-Based SAT-Solvers. |
SAT |
2008 |
DBLP DOI BibTeX RDF |
|
53 | Lintao Zhang, Sharad Malik |
Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications. |
DATE |
2003 |
DBLP DOI BibTeX RDF |
|
53 | Parosh Aziz Abdulla, Per Bjesse, Niklas Eén |
Symbolic Reachability Analysis Based on SAT-Solvers. |
TACAS |
2000 |
DBLP DOI BibTeX RDF |
|
53 | 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 |
|
51 | Alexandra Goultiaeva, Vicki Iverson, Fahiem Bacchus |
Beyond CNF: A Circuit-Based QBF Solver. |
SAT |
2009 |
DBLP DOI BibTeX RDF |
|
51 | Horst Samulowitz, Fahiem Bacchus |
Dynamically Partitioning for Solving QBF. |
SAT |
2007 |
DBLP DOI BibTeX RDF |
|
51 | Ashish Sabharwal, Carlos Ansótegui, Carla P. Gomes, Justin W. Hart, Bart Selman |
QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency. |
SAT |
2006 |
DBLP DOI BibTeX RDF |
|
51 | 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 |
|
51 | Per Bjesse, Tim Leonard, Abdel Mokkedem |
Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
51 | Lin Xu, Frank Hutter, Holger H. Hoos, Kevin Leyton-Brown |
: The Design and Analysis of an Algorithm Portfolio for SAT. |
CP |
2007 |
DBLP DOI BibTeX RDF |
|
51 | 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 |
51 | Hantao Zhang 0001 |
A Complete Random Jump Strategy with Guiding Paths. |
SAT |
2006 |
DBLP DOI BibTeX RDF |
|
51 | Sathiamoorthy Subbarayan, Dhiraj K. Pradhan |
NiVER: Non-increasing Variable Elimination Resolution for Preprocessing SAT Instances. |
SAT (Selected Papers |
2004 |
DBLP DOI BibTeX RDF |
|
51 | 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 |
|
51 | Cristian Coarfa, Demetrios D. Demopoulos, Alfonso San Miguel Aguirre, Devika Subramanian, Moshe Y. Vardi |
Random 3-SAT: The Plot Thickens. |
CP |
2000 |
DBLP DOI BibTeX RDF |
|
51 | Kei Ohmura, Kazunori Ueda |
c-sat: A Parallel SAT Solver for Clusters. |
SAT |
2009 |
DBLP DOI BibTeX RDF |
|
51 | John D. Davis, Zhangxi Tan, Fang Yu 0002, Lintao Zhang |
A practical reconfigurable hardware accelerator for Boolean satisfiability solvers. |
DAC |
2008 |
DBLP DOI BibTeX RDF |
BCP, FPGA, reconfigurable, SAT solver, co-processor |
51 | Malay K. Ganai, Aarti Gupta, Zijiang Yang 0006, Pranav Ashar |
Efficient distributed SAT and SAT-based distributed Bounded Model Checking. |
Int. J. Softw. Tools Technol. Transf. |
2006 |
DBLP DOI BibTeX RDF |
Distributed-SAT, Parallel SAT, Model Checking, Formal Verification, SAT, BMC |
51 | Mona Safar, M. Watheq El-Kharashi, Ashraf Salem |
FPGA-Based SAT Solver. |
CCECE |
2006 |
DBLP DOI BibTeX RDF |
|
51 | Darko Marinov, Sarfraz Khurshid, Suhabe Bugrara, Lintao Zhang, Martin C. Rinard |
Optimizations for Compiling Declarative Models into Boolean Formulas. |
SAT |
2005 |
DBLP DOI BibTeX RDF |
|
51 | Zhao Xing, Weixiong Zhang |
Efficient Strategies for (Weighted) Maximum Satisfiability. |
CP |
2004 |
DBLP DOI BibTeX RDF |
|
51 | Malay K. Ganai, Aarti Gupta, Zijiang Yang 0006, Pranav Ashar |
Efficient Distributed SAT and SAT-Based Distributed Bounded Model Checking. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
48 | Yang Liu 0003, Jun Sun 0001, Jin Song Dong |
An analyzer for extended compositional process algebras. |
ICSE Companion |
2008 |
DBLP DOI BibTeX RDF |
simulation, model checking, fairness, sat solvers |
47 | Alessandro Cimatti, Roberto Sebastiani |
Building Efficient Decision Procedures on Top of SAT Solvers. |
SFM |
2006 |
DBLP DOI BibTeX RDF |
|
47 | Carlos Ansótegui, Jose Larrubia, Chu Min Li, Felip Manyà |
Exploiting multivalued knowledge in variable selection heuristics for SAT solvers. |
Ann. Math. Artif. Intell. |
2007 |
DBLP DOI BibTeX RDF |
Mathematics Subject Classifications (2000) 03B50, 03B05, 03B70 |
47 | Raihan H. Kibria |
Evolving a Neural Net-Based Decision and Search Heuristic for DPLL SAT Solvers. |
IJCNN |
2007 |
DBLP DOI BibTeX RDF |
|
47 | Nachum Dershowitz, Ziyad Hanna, Alexander Nadel |
A Clause-Based Heuristic for SAT Solvers. |
SAT |
2005 |
DBLP DOI BibTeX RDF |
|
47 | Armin Biere |
Adaptive Restart Strategies for Conflict Driven SAT Solvers. |
SAT |
2008 |
DBLP DOI BibTeX RDF |
|
45 | Alessandro Armando, Jacopo Mantovani, Lorenzo Platania |
Bounded model checking of software using SMT solvers instead of SAT solvers. |
Int. J. Softw. Tools Technol. Transf. |
2009 |
DBLP DOI BibTeX RDF |
|
45 | Alessandro Armando, Jacopo Mantovani, Lorenzo Platania |
Bounded Model Checking of Software Using SMT Solvers Instead of SAT Solvers. |
SPIN |
2006 |
DBLP DOI BibTeX RDF |
|
45 | Lengning Liu, Miroslaw Truszczynski |
Local-Search Techniques for Propositional Logic Extended with Cardinality Constraints. |
CP |
2003 |
DBLP DOI BibTeX RDF |
|
45 | Tomi Janhunen, Ilkka Niemelä, Mark Sevalnev |
Computing Stable Models via Reductions to Difference Logic. |
LPNMR |
2009 |
DBLP DOI BibTeX RDF |
|
45 | Cesare Tinelli |
An Abstract Framework for Satisfiability Modulo Theories. |
TABLEAUX |
2007 |
DBLP DOI BibTeX RDF |
|
45 | Daijue Tang, Sharad Malik |
Solving Quantified Boolean Formulas with Circuit Observability Don't Cares. |
SAT |
2006 |
DBLP DOI BibTeX RDF |
|
45 | Xiao Yu Li, Matthias F. M. Stallmann, Franc Brglez |
A Local Search SAT Solver Using an Effective Switching Strategy and an Efficient Unit Propagation. |
SAT |
2003 |
DBLP DOI BibTeX RDF |
|
44 | Geng-Dian Huang, Bow-Yaw Wang |
Complete SAT-Based Model Checking for Context-Free Processes. |
ATVA |
2007 |
DBLP DOI BibTeX RDF |
|
44 | K. Rustan M. Leino, Madan Musuvathi, Xinming Ou |
A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover. |
TACAS |
2005 |
DBLP DOI BibTeX RDF |
|
44 | Christian Thiffault, Fahiem Bacchus, Toby Walsh |
Solving Non-clausal Formulas with DPLL Search. |
CP |
2004 |
DBLP DOI BibTeX RDF |
|
44 | João Marques-Silva 0001, Jordi Planes |
Algorithms for Maximum Satisfiability using Unsatisfiable Cores. |
DATE |
2008 |
DBLP DOI BibTeX RDF |
|
44 | Antti Eero Johannes Hyvärinen, Tommi A. Junttila, Ilkka Niemelä |
Incorporating Learning in Grid-Based Randomized SAT Solving. |
AIMSA |
2008 |
DBLP DOI BibTeX RDF |
|
44 | Mona Safar, Mohamed Shalan, M. Watheq El-Kharashi, Ashraf Salem |
Interactive presentation: A shift register based clause evaluator for reconfigurable SAT solver. |
DATE |
2007 |
DBLP DOI BibTeX RDF |
|
44 | Lei Fang 0002, Michael S. Hsiao |
A new hybrid solution to boost SAT solver performance. |
DATE |
2007 |
DBLP DOI BibTeX RDF |
|
44 | Michael Codish |
Proving Termination with (Boolean) Satisfaction. |
LOPSTR |
2007 |
DBLP DOI BibTeX RDF |
|
44 | Himanshu Jain, Constantinos Bartzis, Edmund M. Clarke |
Satisfiability Checking of Non-clausal Formulas Using General Matings. |
SAT |
2006 |
DBLP DOI BibTeX RDF |
|