Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
147 | 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 |
|
121 | 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 |
|
121 | Horst Samulowitz, Jessica Davies 0001, Fahiem Bacchus |
Preprocessing QBF. |
CP |
2006 |
DBLP DOI BibTeX RDF |
|
121 | Nachum Dershowitz, Ziyad Hanna, Jacob Katz |
Bounded Model Checking with QBF. |
SAT |
2005 |
DBLP DOI BibTeX RDF |
|
121 | Horst Samulowitz, Fahiem Bacchus |
Using SAT in QBF. |
CP |
2005 |
DBLP DOI BibTeX RDF |
|
111 | 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 |
|
107 | Alexandra Goultiaeva, Vicki Iverson, Fahiem Bacchus |
Beyond CNF: A Circuit-Based QBF Solver. |
SAT |
2009 |
DBLP DOI BibTeX RDF |
|
107 | Toni Jussila, Armin Biere, Carsten Sinz, Daniel Kröning, Christoph M. Wintersteiger |
A First Step Towards a Unified Proof Checker for QBF. |
SAT |
2007 |
DBLP DOI BibTeX RDF |
|
107 | Kameshwar Chandrasekar, Michael S. Hsiao |
Q-PREZ: QBF Evaluation Using Partition, Resolution and Elimination with ZBDDs. |
VLSI Design |
2005 |
DBLP DOI BibTeX RDF |
|
107 | Guoqiang Pan, Moshe Y. Vardi |
Symbolic Decision Procedures for QBF. |
CP |
2004 |
DBLP DOI BibTeX RDF |
|
103 | 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 |
103 | Ian P. Gent, Holger H. Hoos, Andrew G. D. Rowley, Kevin Smyth |
Using Stochastic Local Search to Solve Quantified Boolean Formulae. |
CP |
2003 |
DBLP DOI BibTeX RDF |
|
103 | Jussi Rintanen |
Partial Implicit Unfolding in the Davis-Putnam Procedure for Quantified Boolean Formulae. |
LPAR |
2001 |
DBLP DOI BibTeX RDF |
|
92 | Christine Collet, Tuyet-Trinh Vu |
QBF: A Query Broker Framework for Adaptable Query Evaluation. |
FQAS |
2004 |
DBLP DOI BibTeX RDF |
Adaptable Query Evaluation, Query Framework, Query Processing |
88 | Daijue Tang, Sharad Malik |
Solving Quantified Boolean Formulas with Circuit Observability Don't Cares. |
SAT |
2006 |
DBLP DOI BibTeX RDF |
|
88 | Jacob Katz, Ziyad Hanna, Nachum Dershowitz |
Space-Efficient Bounded Model Checking. |
DATE |
2005 |
DBLP DOI BibTeX RDF |
|
88 | Lintao Zhang, Sharad Malik |
Conflict driven learning in a quantified Boolean Satisfiability solver. |
ICCAD |
2002 |
DBLP DOI BibTeX RDF |
|
88 | Matthew Lewis 0004, Paolo Marin, Tobias Schubert 0001, Massimo Narizzano, Bernd Becker 0001, Enrico Giunchiglia |
PaQuBE: Distributed QBF Solving with Advanced Knowledge Sharing. |
SAT |
2009 |
DBLP DOI BibTeX RDF |
Parallel QBF Solving, Master/Slave Architecture, MPI, Message Passing |
84 | 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 |
77 | Horst Samulowitz, Fahiem Bacchus |
Dynamically Partitioning for Solving QBF. |
SAT |
2007 |
DBLP DOI BibTeX RDF |
|
77 | Yinlei Yu, Sharad Malik |
Validating the result of a Quantified Boolean Formula (QBF) solver: theory and practice. |
ASP-DAC |
2005 |
DBLP DOI BibTeX RDF |
|
74 | Marc Herbstritt, Bernd Becker 0001 |
On Combining 01X-Logic and QBF. |
EUROCAST |
2007 |
DBLP DOI BibTeX RDF |
01X, Blackbox Designs, Bounded Model Checking, QBF |
74 | Florian Lonsing, Armin Biere |
A Compact Representation for Syntactic Dependencies in QBFs. |
SAT |
2009 |
DBLP DOI BibTeX RDF |
|
74 | N. Hristov, Anja Remshagen |
Local search for quantified Boolean formulas. |
ACM Southeast Regional Conference (1) |
2005 |
DBLP DOI BibTeX RDF |
local search, logic, quantified Boolean formula, polynomial hierarchy |
74 | Gilles Audemard, Lakhdar Sais |
SAT Based BDD Solver for Quantified Boolean Formulas. |
ICTAI |
2004 |
DBLP DOI BibTeX RDF |
|
72 | Luca Pulina |
The Ninth QBF Solvers Evaluation - Preliminary Report. |
QBF@SAT |
2016 |
DBLP BibTeX RDF |
|
72 | Christoph Scholl 0001, Florian Pigorsch |
The QBF Solver AIGSolve. |
QBF@SAT |
2016 |
DBLP BibTeX RDF |
|
72 | Joshua Blinkhorn, Olaf Beyersdorff |
Dependency Schemes in QBF Calculi: Semantics and Soundness. |
QBF@SAT |
2016 |
DBLP BibTeX RDF |
|
72 | Diptarama, Ryo Yoshinaka, Ayumi Shinohara |
QBF Encoding of Generalized Tic-Tac-Toe. |
QBF@SAT |
2016 |
DBLP BibTeX RDF |
|
72 | Günther Charwat, Stefan Woltran |
Dynamic Programming-based QBF Solving. |
QBF@SAT |
2016 |
DBLP BibTeX RDF |
|
63 | Florian Pigorsch, Christoph Scholl 0001 |
An AIG-Based QBF-solver using SAT for preprocessing. |
DAC |
2010 |
DBLP DOI BibTeX RDF |
Boolean satisfiability, quantified boolean formulas |
63 | Igor Stéphan, Benoit Da Mota |
A Unified Framework for Certificate and Compilation for QBF. |
ICLA |
2009 |
DBLP DOI BibTeX RDF |
|
63 | Horst Samulowitz, Fahiem Bacchus |
Binary Clause Reasoning in QBF. |
SAT |
2006 |
DBLP DOI BibTeX RDF |
|
59 | Luca Pulina, Armando Tacchella |
A self-adaptive multi-engine solver for quantified Boolean formulas. |
Constraints An Int. J. |
2009 |
DBLP DOI BibTeX RDF |
Self-adaptive multi-engine solver, AQME, Quantified Boolean formulas |
59 | Mohammad Faizal Ahmad Fauzi, Paul H. Lewis |
Query by Fax for Content-Based Image Retrieval. |
CIVR |
2002 |
DBLP DOI BibTeX RDF |
|
59 | Lintao Zhang, Sharad Malik |
Towards a Symmetric Treatment of Satisfaction and Conflicts in Quantified Boolean Formula Evaluation. |
CP |
2002 |
DBLP DOI BibTeX RDF |
|
54 | Florian Lonsing, Martina Seidl (eds.) |
Proceedings of the 4th International Workshop on Quantified Boolean Formulas (QBF 2016) co-located with 19th International Conference on Theory and Applications of Satisfiability Testing (SAT 2016), Bordeaux, France, July 4, 2016. |
QBF@SAT |
2016 |
DBLP BibTeX RDF |
|
54 | Bart Bogaerts 0001, Tomi Janhunen, Shahab Tasharrofi |
SAT-to-SAT in QBFEval 2016. |
QBF@SAT |
2016 |
DBLP BibTeX RDF |
|
54 | Giovanni Amendola, Carmine Dodaro, Francesco Ricca |
ASPQ: An ASP-Based 2QBF Solver. |
QBF@SAT |
2016 |
DBLP BibTeX RDF |
|
48 | Florian Lonsing, Armin Biere |
Nenofex: Expanding NNF for QBF Solving. |
SAT |
2008 |
DBLP DOI BibTeX RDF |
|
48 | Conghua Zhou, Zhenyu Chen 0001, Zhihong Tao |
QBF-Based Symbolic Model Checking for Knowledge and Time. |
TAMC |
2007 |
DBLP DOI BibTeX RDF |
|
48 | Hratch Mangassarian, Andreas G. Veneris, Sean Safarpour, Marco Benedetti, Duncan Exon Smith |
A performance-driven QBF-based iterative logic array representation with applications to verification, debug and test. |
ICCAD |
2007 |
DBLP DOI BibTeX RDF |
|
48 | Ian P. Gent, Andrew G. D. Rowley |
Local and Global Complete Solution Learning Methods for QBF. |
SAT |
2005 |
DBLP DOI BibTeX RDF |
|
48 | Tuyet-Trinh Vu, Christine Collet |
Adaptable Query Evaluation Using QBF. |
IDEAS |
2004 |
DBLP DOI BibTeX RDF |
|
48 | Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella |
QBF Reasoning on Real-World Instances. |
SAT (Selected Papers |
2004 |
DBLP DOI BibTeX RDF |
|
48 | Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella |
QuBE++: An Efficient QBF Solver. |
FMCAD |
2004 |
DBLP DOI BibTeX RDF |
|
45 | Hratch Mangassarian, Andreas G. Veneris, Marco Benedetti |
Robust QBF Encodings for Sequential Circuits with Applications to Verification, Debug, and Test. |
IEEE Trans. Computers |
2010 |
DBLP DOI BibTeX RDF |
k-induction, sequential ATPG, SAT, QBF, design debugging, BMC |
44 | Cédric Pralet, Thomas Schiex, Gérard Verfaillie |
Decomposition of Multi-operator Queries on Semiring-Based Graphical Models. |
CP |
2006 |
DBLP DOI BibTeX RDF |
|
37 | Olaf Beyersdorff, Benjamin Böhm 0001 |
Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution. |
Log. Methods Comput. Sci. |
2023 |
DBLP DOI BibTeX RDF |
|
37 | Olaf Beyersdorff, Benjamin Böhm 0001 |
Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution. |
CoRR |
2021 |
DBLP BibTeX RDF |
|
37 | Olaf Beyersdorff, Benjamin Böhm 0001 |
Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution. |
ITCS |
2021 |
DBLP DOI BibTeX RDF |
|
37 | Olaf Beyersdorff, Benjamin Böhm 0001 |
Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution. |
Electron. Colloquium Comput. Complex. |
2020 |
DBLP BibTeX RDF |
|
37 | Wenhui Zhang |
QBF Encoding of Temporal Properties and QBF-Based Verification. |
IJCAR |
2014 |
DBLP DOI BibTeX RDF |
|
33 | Luca Pulina, Armando Tacchella |
Hard QBF Encodings Made Easy: Dream or Reality? |
AI*IA |
2009 |
DBLP DOI BibTeX RDF |
|
33 | Uwe Bubeck, Hans Kleine Büning |
Bounded Universal Expansion for Preprocessing QBF. |
SAT |
2007 |
DBLP DOI BibTeX RDF |
|
33 | Stefan Staber, Roderick Bloem |
Fault Localization and Correction with QBF. |
SAT |
2007 |
DBLP DOI BibTeX RDF |
|
33 | Daniel Le Berre, Massimo Narizzano, Laurent Simon, Armando Tacchella |
The Second QBF Solvers Comparative Evaluation. |
SAT (Selected Papers |
2004 |
DBLP DOI BibTeX RDF |
|
33 | Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella |
Monotone Literals and Learning in QBF Reasoning. |
CP |
2004 |
DBLP DOI BibTeX RDF |
|
33 | Ian P. Gent, Enrico Giunchiglia, Massimo Narizzano, Andrew G. D. Rowley, Armando Tacchella |
Watched Data Structures for QBF Solvers. |
SAT |
2003 |
DBLP DOI BibTeX RDF |
|
33 | Maher N. Mneimneh, Karem A. Sakallah |
Computing Vertex Eccentricity in Exponentially Large Graphs: QBF Formulation and Solution. |
SAT |
2003 |
DBLP DOI BibTeX RDF |
|
29 | Uwe Egly, Martina Seidl, Stefan Woltran |
A solver for QBFs in negation normal form. |
Constraints An Int. J. |
2009 |
DBLP DOI BibTeX RDF |
Negation normal form, Solver, QBFs |
29 | Luca Pulina, Armando Tacchella |
Treewidth: A Useful Marker of Empirical Hardness in Quantified Boolean Logic Encodings. |
LPAR |
2008 |
DBLP DOI BibTeX RDF |
|
29 | Robert Wille, Hoang Minh Le 0001, Gerhard W. Dueck, Daniel Große |
Quantified Synthesis of Reversible Logic. |
DATE |
2008 |
DBLP DOI BibTeX RDF |
|
29 | Ansuman Banerjee, Pallab Dasgupta, P. P. Chakrabarti 0001 |
Formal methods for checking realizability of coalitions in 3-party systems. |
MEMOCODE |
2006 |
DBLP DOI BibTeX RDF |
|
29 | Marc Herbstritt, Bernd Becker 0001, Christoph Scholl 0001 |
Advanced SAT-Techniques for Bounded Model Checking of Blackbox Designs. |
MTV |
2006 |
DBLP DOI BibTeX RDF |
|
29 | Guoqiang Pan, Moshe Y. Vardi |
Fixed-Parameter Hierarchies inside PSPACE. |
LICS |
2006 |
DBLP DOI BibTeX RDF |
|
29 | Marco Cadoli, Marco Schaerf |
Partial Solutions with Unique Completion. |
Reasoning, Action and Interaction in AI Theories and Systems |
2006 |
DBLP DOI BibTeX RDF |
|
29 | Marco Benedetti |
Quantifier Trees for QBFs. |
SAT |
2005 |
DBLP DOI BibTeX RDF |
|
29 | Kostas Stergiou 0001 |
Repair-Based Methods for Quantified CSPs. |
CP |
2005 |
DBLP DOI BibTeX RDF |
|
29 | Armin Biere |
Resolve and Expand. |
SAT (Selected Papers |
2004 |
DBLP DOI BibTeX RDF |
|
29 | Philippe Besnard, Torsten Schaub, Hans Tompits, Stefan Woltran |
Paraconsistent Logics for Reasoning via Quantified Boolean Formulas, II: Circumscribing Inconsistent Theories. |
ECSQARU |
2003 |
DBLP DOI BibTeX RDF |
|
29 | Andrew G. D. Rowley |
Watching Clauses in Quantified Boolean Formulae. |
CP |
2003 |
DBLP DOI BibTeX RDF |
|
29 | Ryan Williams 0001 |
Algorithms for quantified Boolean formulas. |
SODA |
2002 |
DBLP BibTeX RDF |
|
29 | Thomas Eiter, Volker Klotz, Hans Tompits, Stefan Woltran |
Modal Nonmonotonic Logics Revisited: Efficient Encodings for the Basic Reasoning Tasks. |
TABLEAUX |
2002 |
DBLP DOI BibTeX RDF |
|
29 | Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella |
QUBE: A System for Deciding Quantified Boolean Formulas Satisfiability. |
IJCAR |
2001 |
DBLP DOI BibTeX RDF |
|
26 | Ansuman Banerjee |
Synthesizability of 3 Party Formal Specifications-Does My Controller See Enough?. |
VLSI Design |
2010 |
DBLP DOI BibTeX RDF |
Satisfiability, LTL, Realizability, QBF |
26 | Zhi-Hong Tao, Conghua Zhou, Zhong Chen, Lifu Wang |
Bounded Model Checking of CTL. |
J. Comput. Sci. Technol. |
2007 |
DBLP DOI BibTeX RDF |
symbolic model checking, bounded model checking, QBF, CTL* |
26 | Mukul R. Prasad, Armin Biere, Aarti Gupta |
A survey of recent advances in SAT-based formal verification. |
Int. J. Softw. Tools Technol. Transf. |
2005 |
DBLP DOI BibTeX RDF |
Model checking, Verification, ATPG, SAT, QBF |
26 | Anja Remshagen, Klaus Truemper |
An Effective Algorithm for the Futile Questioning Problem. |
J. Autom. Reason. |
2005 |
DBLP DOI BibTeX RDF |
futile questioning, learning, QBF |
25 | T. V. Thirumala Reddy, D. Sai Krishna, C. Pandu Rangan |
The Guarding Problem - Complexity and Approximation. |
IWOCA |
2009 |
DBLP DOI BibTeX RDF |
QBF (Quantified Boolean Formula), QSAT (Quantified Satisfiability), Approximation Algorithms, PSPACE-complete |
25 | Rajeev Alur, P. Madhusudan, Wonhong Nam |
Symbolic computational techniques for solving games. |
Int. J. Softw. Tools Technol. Transf. |
2005 |
DBLP DOI BibTeX RDF |
QBF solving, Games, Formal verification, Symbolic model checking, Bounded model checking |
19 | Leroy Chew, Friedrich Slivovsky |
Towards Uniform Certification in QBF. |
Log. Methods Comput. Sci. |
2024 |
DBLP DOI BibTeX RDF |
|
19 | Axel Bergström, Tjark Weber |
Verified QBF Solving. |
Arch. Formal Proofs |
2024 |
DBLP BibTeX RDF |
|
19 | Yifan He, Abdallah Saffidine, Michael Thielscher |
Solving Two-player Games with QBF Solvers in General Game Playing. |
AAMAS |
2024 |
DBLP BibTeX RDF |
|
19 | Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomás Peitl |
Hardness Characterisations and Size-width Lower Bounds for QBF Resolution. |
ACM Trans. Comput. Log. |
2023 |
DBLP DOI BibTeX RDF |
|
19 | Agnes Schleitzer, Olaf Beyersdorff |
Classes of Hard Formulas for QBF Resolution. |
J. Artif. Intell. Res. |
2023 |
DBLP DOI BibTeX RDF |
|
19 | Benjamin Böhm 0001, Olaf Beyersdorff |
QCDCL vs QBF Resolution: Further Insights. |
Electron. Colloquium Comput. Complex. |
2023 |
DBLP BibTeX RDF |
|
19 | Abhimanyu Choudhury, Meena Mahajan |
Dependency schemes in CDCL-based QBF solving: a proof-theoretic study. |
Electron. Colloquium Comput. Complex. |
2023 |
DBLP BibTeX RDF |
|
19 | Leroy Chew |
Proof Simulation via Round-based Strategy Extraction for QBF. |
Electron. Colloquium Comput. Complex. |
2023 |
DBLP BibTeX RDF |
|
19 | Maximilian Heisinger, Irfansha Shaik, Martina Seidl, Jaco van de Pol |
Search-Space Pruning with Int-Splits for Faster QBF Solving. |
CoRR |
2023 |
DBLP DOI BibTeX RDF |
|
19 | Irfansha Shaik, Valentin Mayer-Eichberger, Jaco van de Pol, Abdallah Saffidine |
Implicit State and Goals in QBF Encodings for Positional Games (extended version). |
CoRR |
2023 |
DBLP DOI BibTeX RDF |
|
19 | Eduardo Calò, Jordi Levy |
General Boolean Formula Minimization with QBF Solvers. |
CoRR |
2023 |
DBLP DOI BibTeX RDF |
|
19 | Johannes Klaus Fichte, Robert Ganian, Markus Hecher, Friedrich Slivovsky, Sebastian Ordyniak |
Structure-Aware Lower Bounds and Broadening the Horizon of Tractability for QBF. |
CoRR |
2023 |
DBLP DOI BibTeX RDF |
|
19 | Irfansha Shaik, Jaco van de Pol |
Concise QBF Encodings for Games on a Grid (extended version). |
CoRR |
2023 |
DBLP DOI BibTeX RDF |
|
19 | Levent Aksoy, Muhammad Yasin, Samuel Pagliarini |
KRATT: QBF-Assisted Removal and Structural Analysis Attack Against Logic Locking. |
CoRR |
2023 |
DBLP DOI BibTeX RDF |
|
19 | Allen Van Gelder |
Subsumption-Linear Q-Resolution for QBF Theorem Proving. |
WoLLIC |
2023 |
DBLP DOI BibTeX RDF |
|
19 | Irfansha Shaik, Valentin Mayer-Eichberger, Jaco van de Pol, Abdallah Saffidine |
Implicit QBF Encodings for Positional Games. |
ACG |
2023 |
DBLP DOI BibTeX RDF |
|
19 | Eduardo Calò, Jordi Levy |
General Boolean Formula Minimization with QBF Solvers. |
CCIA |
2023 |
DBLP DOI BibTeX RDF |
|
19 | Johannes Klaus Fichte, Robert Ganian, Markus Hecher, Friedrich Slivovsky, Sebastian Ordyniak |
Structure-Aware Lower Bounds and Broadening the Horizon of Tractability for QBF. |
LICS |
2023 |
DBLP DOI BibTeX RDF |
|
19 | Franz-Xaver Reichl, Friedrich Slivovsky, Stefan Szeider |
Circuit Minimization with QBF-Based Exact Synthesis. |
AAAI |
2023 |
DBLP DOI BibTeX RDF |
|