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 reasoning; Quantified Boolean Logic; Satisfiability testing

Mathematics Subject Classification ID

68Q25: Analysis of algorithms and problem complexity

Related Items

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

Uses Software

• QuBE++
• QUBE

Cites Work

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item