Conformant planning as a case study of incremental QBF solving
From MaRDI portal
Publication:2398267
DOI10.1007/s10472-016-9501-2zbMath1409.68253OpenAlexW2309239751WikidataQ59529080 ScholiaQ59529080MaRDI QIDQ2398267
Andreas Pfandler, Florian Lonsing, Uwe Egly, Martin Kronegger
Publication date: 15 August 2017
Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10472-016-9501-2
preprocessingconformant planningblocked clause eliminationincremental solvingquantified Boolean formulas (QBFs)
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (14)
Hardness Characterisations and Size-width Lower Bounds for QBF Resolution ⋮ Feasible Interpolation for QBF Resolution Calculi ⋮ Unnamed Item ⋮ Conformant planning as a case study of incremental QBF solving ⋮ Unnamed Item ⋮ Lower bound techniques for QBF expansion ⋮ Unnamed Item ⋮ Understanding cutting planes for QBFs ⋮ Building strategies into QBF proofs ⋮ Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations ⋮ Unnamed Item ⋮ CPCES: a planning framework to solve conformant planning problems through a counterexample guided refinement ⋮ Unnamed Item ⋮ Unnamed Item
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Backdoor sets of quantified Boolean formulas
- Fast planning through planning graph analysis
- Computational complexity of planning and approximate planning in the presence of incompleteness
- An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
- Resolution for quantified Boolean formulas
- On a generalization of extended resolution
- Expansion-based QBF solving versus Q-resolution
- Conformant planning as a case study of incremental QBF solving
- Unified QBF certification and its applications
- Conformant planning via heuristic forward search: A new approach
- Extended Failed-Literal Preprocessing for Quantified Boolean Formulas
- Solving QBF with Counterexample Guided Refinement
- On QBF Proofs and Preprocessing
- Incremental QBF Solving by DepQBF
- Inprocessing Rules
- Clause Elimination for SAT and QSAT
- Ultimately Incremental SAT
- Dominant Controllability Check Using QBF-Solver and Netlist Optimizer
- A Unified Proof System for QBF Preprocessing
- Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination
- Nenofex: Expanding NNF for QBF Solving
- Bounded Universal Expansion for Preprocessing QBF
- Compiling Uncertainty Away in Conformant Planning Problems with Bounded Width
- Verification of partial designs using incremental QBF
- sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning
- Reconstructing Solutions after Blocked Clause Elimination
- Blocked Clause Elimination for QBF
- Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
- Factoring Out Assumptions to Speed Up MUS Extraction
- Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction
- A machine program for theorem-proving
- Theory and Applications of Satisfiability Testing
This page was built for publication: Conformant planning as a case study of incremental QBF solving
