Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
116 | Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella |
Quantifier Structure in Search-Based Procedures for QBFs. |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. |
2007 |
DBLP DOI BibTeX RDF |
|
113 | 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 |
98 | Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella |
Quantifier structure in search based procedures for QBFs. |
DATE |
2006 |
DBLP DOI BibTeX RDF |
|
63 | Marco Benedetti |
Evaluating QBFs via Symbolic Skolemization. |
LPAR |
2004 |
DBLP DOI BibTeX RDF |
|
53 | Philippe Besnard, Torsten Schaub, Hans Tompits, Stefan Woltran |
Representing Paraconsistent Reasoning via Quantified Propositional Logic. |
Inconsistency Tolerance |
2005 |
DBLP DOI BibTeX RDF |
|
53 | Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella |
QBF Reasoning on Real-World Instances. |
SAT (Selected Papers |
2004 |
DBLP DOI BibTeX RDF |
|
53 | Uwe Egly, Martina Seidl, Hans Tompits, Stefan Woltran, Michael Zolda |
Comparing Different Prenexing Strategies for Quantified Boolean Formulas. |
SAT |
2003 |
DBLP DOI BibTeX RDF |
|
45 | Marco Benedetti |
sKizzo: A Suite to Evaluate and Certify QBFs. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
45 | 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 |
35 | 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 |
35 | Luca Pulina, Armando Tacchella |
Hard QBF Encodings Made Easy: Dream or Reality? |
AI*IA |
2009 |
DBLP DOI BibTeX RDF |
|
35 | Luca Pulina, Armando Tacchella |
Treewidth: A Useful Marker of Empirical Hardness in Quantified Boolean Logic Encodings. |
LPAR |
2008 |
DBLP DOI BibTeX RDF |
|
35 | Esther Ge, Richi Nayak, Yue Xu 0001, Yuefeng Li |
A User Driven Data Mining Process Model and Learning System. |
DASFAA |
2008 |
DBLP DOI BibTeX RDF |
lifetime prediction, corrosion prediction, Data Mining, feature selection, predictive model, Learning System, civil engineering |
35 | Maher N. Mneimneh, Karem A. Sakallah |
Computing Vertex Eccentricity in Exponentially Large Graphs: QBF Formulation and Solution. |
SAT |
2003 |
DBLP DOI BibTeX RDF |
|
35 | 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 |
|
35 | Ryan Williams 0001 |
Algorithms for quantified Boolean formulas. |
SODA |
2002 |
DBLP BibTeX RDF |
|
35 | 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 |
|
33 | Uwe Egly, Reinhard Pichler, Stefan Woltran |
On deciding subsumption problems. |
Ann. Math. Artif. Intell. |
2005 |
DBLP DOI BibTeX RDF |
equational problems, satisfiability, subsumption, QBFs |
27 | Olaf Beyersdorff, Benjamin Böhm 0001, Meena Mahajan |
Runtime vs. Extracted Proof Size: An Exponential Gap for CDCL on QBFs. |
AAAI |
2024 |
DBLP DOI BibTeX RDF |
|
27 | Sravanthi Chede, Leroy Chew, Balesh Kumar, Anil Shukla |
Understanding Nullstellensatz for QBFs. |
Electron. Colloquium Comput. Complex. |
2023 |
DBLP BibTeX RDF |
|
27 | Anupam Das 0002, Sonia Marin |
Modal logic and the polynomial hierarchy: from QBFs to K and back. |
AiML |
2022 |
DBLP BibTeX RDF |
|
27 | Edith Hemaspaandra, David E. Narváez |
Formal Methods for NFA Equivalence: QBFs, Witness Extraction, and Encoding Verification. |
CICM |
2022 |
DBLP DOI BibTeX RDF |
|
27 | Hannah Miller, David E. Narváez |
Toward Determining NFA Equivalence via QBFs (Student Abstract). |
AAAI |
2021 |
DBLP DOI BibTeX RDF |
|
27 | Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomás Peitl, Gaurav Sood 0001 |
Hard QBFs for Merge Resolution. |
Electron. Colloquium Comput. Complex. |
2020 |
DBLP BibTeX RDF |
|
27 | Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomás Peitl, Gaurav Sood 0001 |
Hard QBFs for Merge Resolution. |
CoRR |
2020 |
DBLP BibTeX RDF |
|
27 | Anupam Das 0002 |
From QBFs to MALL and Back via Focussing. |
J. Autom. Reason. |
2020 |
DBLP DOI BibTeX RDF |
|
27 | Johannes Klaus Fichte, Markus Hecher, Andreas Pfandler |
Lower Bounds for QBFs of Bounded Treewidth. |
LICS |
2020 |
DBLP DOI BibTeX RDF |
|
27 | Olaf Beyersdorff, Joshua Blinkhorn, Meena Mahajan, Tomás Peitl, Gaurav Sood 0001 |
Hard QBFs for Merge Resolution. |
FSTTCS |
2020 |
DBLP DOI BibTeX RDF |
|
27 | Anupam Das 0002 |
From QBFs to MALL and back via focussing: fragments of multiplicative additive linear logic for each level of the polynomial hierarchy. |
CoRR |
2019 |
DBLP BibTeX RDF |
|
27 | Johannes Klaus Fichte, Markus Hecher, Andreas Pfandler |
TE-ETH: Lower Bounds for QBFs of Bounded Treewidth. |
CoRR |
2019 |
DBLP BibTeX RDF |
|
27 | Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde |
Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs. |
Log. Methods Comput. Sci. |
2019 |
DBLP DOI BibTeX RDF |
|
27 | Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla |
Understanding cutting planes for QBFs. |
Inf. Comput. |
2018 |
DBLP DOI BibTeX RDF |
|
27 | Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde |
Size, Cost and Capacity: A Semantic Technique for Hard Random QBFs. |
ITCS |
2018 |
DBLP DOI BibTeX RDF |
|
27 | Holger H. Hoos, Tomás Peitl, Friedrich Slivovsky, Stefan Szeider |
Portfolio-Based Algorithm Selection for Circuit QBFs. |
CP |
2018 |
DBLP DOI BibTeX RDF |
|
27 | Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde |
Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs. |
Electron. Colloquium Comput. Complex. |
2017 |
DBLP BibTeX RDF |
|
27 | Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla |
Understanding Cutting Planes for QBFs. |
Electron. Colloquium Comput. Complex. |
2017 |
DBLP BibTeX RDF |
|
27 | Olaf Beyersdorff, Joshua Blinkhorn, Luke Hinde |
Size, Cost, and Capacity: A Semantic Technique for Hard Random QBFs. |
CoRR |
2017 |
DBLP BibTeX RDF |
|
27 | Uwe Egly |
On Stronger Calculi for QBFs. |
CoRR |
2016 |
DBLP BibTeX RDF |
|
27 | Uwe Egly |
On Stronger Calculi for QBFs. |
SAT |
2016 |
DBLP DOI BibTeX RDF |
|
27 | Olaf Beyersdorff, Leroy Chew, Meena Mahajan, Anil Shukla |
Understanding Cutting Planes for QBFs. |
FSTTCS |
2016 |
DBLP DOI BibTeX RDF |
|
27 | Florian Lonsing, Uwe Egly |
Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API. |
CoRR |
2015 |
DBLP BibTeX RDF |
|
27 | Florian Lonsing, Uwe Egly |
Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API. |
SAT |
2015 |
DBLP DOI BibTeX RDF |
|
27 | Uwe Egly |
On Sequent Systems and Resolution for QBFs. |
SAT |
2012 |
DBLP DOI BibTeX RDF |
|
27 | Enrico Giunchiglia, Paolo Marin, Massimo Narizzano |
sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning. |
SAT |
2010 |
DBLP DOI BibTeX RDF |
|
27 | Massimo Narizzano, Claudia Peschiera, Luca Pulina, Armando Tacchella |
Evaluating and certifying QBFs: A comparison of state-of-the-art tools. |
AI Commun. |
2009 |
DBLP DOI BibTeX RDF |
|
27 | Florian Lonsing, Armin Biere |
A Compact Representation for Syntactic Dependencies in QBFs. |
SAT |
2009 |
DBLP DOI BibTeX RDF |
|
27 | Enrico Giunchiglia, Paolo Marin, Massimo Narizzano |
Preprocessing Techniques for QBFs. |
RCRA |
2008 |
DBLP BibTeX RDF |
|
27 | Uwe Egly, Martina Seidl, Stefan Woltran |
A Solver for QBFs in Nonprenex Form. |
ECAI |
2006 |
DBLP BibTeX RDF |
|
27 | Yannet Interian, Gabriel Corvera, Bart Selman, Ryan Williams 0001 |
Finding Small Unsatisfiable Cores to Prove Unsatisfiability of QBFs. |
AI&M |
2006 |
DBLP BibTeX RDF |
|
27 | Marco Benedetti |
Quantifier Trees for QBFs. |
SAT |
2005 |
DBLP DOI BibTeX RDF |
|
18 | 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 |
18 | Luca Pulina, Armando Tacchella |
Learning to Integrate Deduction and Search in Reasoning about Quantified Boolean Formulas. |
FroCoS |
2009 |
DBLP DOI BibTeX RDF |
|
18 | Luca Pulina, Armando Tacchella |
QuBIS: An (In)complete Solver for Quantified Boolean Formulas. |
MICAI |
2008 |
DBLP DOI BibTeX RDF |
|
18 | Ofer Arieli |
Paraconsistent reasoning and preferential entailments by signed quantified Boolean formulae. |
ACM Trans. Comput. Log. |
2007 |
DBLP DOI BibTeX RDF |
Paraconsistent and nonmonotonic reasoning, preferential semantics, quantified Boolean formulae |
18 | Georges G. E. Gielen, Donatella Sciuto |
Guest Editorial [intro. to the special issue on the 2006 IEEE/ACM Design, Automation and Test in Europe Conference]. |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. |
2007 |
DBLP DOI BibTeX RDF |
|
18 | Luca Pulina, Armando Tacchella |
A Multi-engine Solver for Quantified Boolean Formulas. |
CP |
2007 |
DBLP DOI BibTeX RDF |
|
18 | Daijue Tang, Sharad Malik |
Solving Quantified Boolean Formulas with Circuit Observability Don't Cares. |
SAT |
2006 |
DBLP DOI BibTeX RDF |
|
18 | 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 |
|
18 | Daniel Le Berre, Massimo Narizzano, Laurent Simon, Armando Tacchella |
The Second QBF Solvers Comparative Evaluation. |
SAT (Selected Papers |
2004 |
DBLP DOI BibTeX RDF |
|
18 | Gilles Audemard, Lakhdar Sais |
SAT Based BDD Solver for Quantified Boolean Formulas. |
ICTAI |
2004 |
DBLP DOI BibTeX RDF |
|
18 | Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella |
Monotone Literals and Learning in QBF Reasoning. |
CP |
2004 |
DBLP DOI BibTeX RDF |
|
18 | Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella |
QuBE++: An Efficient QBF Solver. |
FMCAD |
2004 |
DBLP DOI BibTeX RDF |
|
18 | 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 |
|
18 | 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 |
|
18 | Andrew G. D. Rowley |
Watching Clauses in Quantified Boolean Formulae. |
CP |
2003 |
DBLP DOI BibTeX RDF |
|
18 | David Pearce 0001, Hans Tompits, Stefan Woltran |
Encodings for Equilibrium Logic and Logic Programs with Nested Expressions. |
EPIA |
2001 |
DBLP DOI BibTeX RDF |
|
18 | Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella |
An Analysis of Backjumping and Trivial Truth in Quantified Boolean Formulas Satisfiability. |
AI*IA |
2001 |
DBLP DOI BibTeX RDF |
|
18 | Alexander Shen |
IP = PSPACE: Simplified Proof. |
J. ACM |
1992 |
DBLP DOI BibTeX RDF |
interactive proofs, PSPACE |