A self-adaptive multi-engine solver for quantified Boolean formulas

DOI10.1007/s10601-008-9051-2zbMath1183.68589OpenAlexW2013951121MaRDI QIDQ1020496

Luca Pulina, Armando Tacchella

Publication date: 29 May 2009

Published in: Constraints (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10601-008-9051-2

zbMATH Keywords

quantified Boolean formulasAQMEself-adaptive multi-engine solver

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (17)

Algorithm portfolios for noisy optimization ⋮ ASlib: a benchmark library for algorithm selection ⋮ Portfolio theorem proving and prover runtime prediction for geometry ⋮ SUNNY: a Lazy Portfolio Approach for Constraint Solving ⋮ An algorithm selection approach for the flexible job shop scheduling problem: choosing constraint programming solvers through machine learning ⋮ aspeed: Solver scheduling via answer set programming ⋮ Logic-based ontology comparison and module extraction, with an application to DL-Lite ⋮ Benchmarking a model checker for algorithmic improvements and tuning for performance ⋮ What Works Best When? A Systematic Evaluation of Heuristics for Max-Cut and QUBO ⋮ A complexity perspective on entailment of parameterized linear constraints ⋮ Empirical software metrics for benchmarking of verification tools ⋮ Why CP Portfolio Solvers Are (under)Utilized? Issues and Challenges ⋮ Efficiently Coupling the I-DLV Grounder with ASP Solvers ⋮ A self-adaptive multi-engine solver for quantified Boolean formulas ⋮ The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17) ⋮ Learning to Integrate Deduction and Search in Reasoning about Quantified Boolean Formulas ⋮ Proof complexity of symbolic QBF reasoning

Uses Software

• QBFLIB
• C4.5
• QBFEVAL
• Quantor
• sKizzo

Cites Work

• SAT-based planning in complex domains: Concurrency, constraints and nondeterminism
• A self-adaptive multi-engine solver for quantified Boolean formulas
• Resolution for quantified Boolean formulas
• Compressing BMC Encodings with QBF
• Partial Implicit Unfolding in the Davis-Putnam Procedure for Quantified Boolean Formulae
• Hierarchical Hardness Models for SAT
• Ridge Estimators in Logistic Regression
• Theory and Applications of Satisfiability Testing
• Automated Deduction – CADE-20
• A machine program for theorem-proving
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Principles and Practice of Constraint Programming – CP 2004
• Automated Deduction – CADE-19
• Algorithm portfolios
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A self-adaptive multi-engine solver for quantified Boolean formulas