Backjumping for quantified Boolean logic satisfiability

DOI10.1016/S0004-3702(02)00373-9zbMath1082.68795WikidataQ62040564 ScholiaQ62040564MaRDI QIDQ814445

Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella

Publication date: 7 February 2006

Published in: Artificial Intelligence (Search for Journal in Brave)

zbMATH Keywords

Automated reasoningQuantified Boolean LogicSatisfiability testing

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25)

Related Items

The complexity of constraint satisfaction games and QCSP, Characterising equilibrium logic and nested logic programs: Reductions and complexity,, Solving quantified constraint satisfaction problems, Filter-based resolution principle for lattice-valued propositional logic LP\((X)\), Unnamed Item, Multistage robust discrete optimization via quantified integer programming, OuterCount: a first-level solution-counter for quantified Boolean formulas, Solution Directed Backjumping for QCSP, Stochastic Satisfiability Modulo Theories for Non-linear Arithmetic, Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers, Value ordering for quantified CSPs, A solver for QBFs in negation normal form, A Compact Representation for Syntactic Dependencies in QBFs, Non-binary quantified CSP: Algorithms and modelling, Learning to Integrate Deduction and Search in Reasoning about Quantified Boolean Formulas, Backjumping for quantified Boolean logic satisfiability

Uses Software

• QuBE++
• QUBE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Backjumping for quantified Boolean logic satisfiability
• A fast parallel SAT-solver -- efficient workload balancing
• A theoretical evaluation of selected backtracking algorithms.
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• Resolution for quantified Boolean formulas
• A machine program for theorem-proving