QUBOS: Deciding quantified Boolean logic using propositional satisfiability solvers

DOI10.1007/3-540-36126-X_12MaRDI QIDQ4427904zbMATH OpenFDO

Authors Abdelwaheb Ayari, David Basin

Publication date 14 September 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2517/25170187.htm

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25)

Recommendations

• A satisfiability procedure for quantified Boolean formulae
• Contributions to the theory of practical quantified Boolean formula solving
• Resolve and expand
• Principles and Practice of Constraint Programming – CP 2004
• scientific article; zbMATH DE number 5719280

Cited in

(24)

• A solver for QBFs in negation normal form
• Backdoor sets of quantified Boolean formulas
• A satisfiability procedure for quantified Boolean formulae
• Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
• Expansion-based QBF solving versus Q-resolution
• Solution validation and extraction for QBF preprocessing
• Computational methods for database repair by signed formulae
• Solving QBF with counterexample guided refinement
• Q-resolution with generalized axioms
• Parametric quantified SAT solving
• A Splitting Algorithm Based on Soft Constraints for the Computation of Truth Degree in Quantitative Logic
• A Unified Framework for Certificate and Compilation for QBF
• A Compact Representation for Syntactic Dependencies in QBFs
• Symmetry in Gardens of Eden
• Lemma and model caching in decision procedures for quantified Boolean formulas
• Quantifier elimination by dependency sequents
• CAQE and QuAbS: Abstraction Based QBF Solvers
• Efficiently representing existential dependency sets for expansion-based QBF solvers
• Backdoors to normality for disjunctive logic programs
• Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
• Propositional PSPACE reasoning with Boolean programs versus quantified Boolean formulas
• Never trust your solver: certification for SAT and QBF
• Quantified constraint handling rules
• Backjumping for quantified Boolean logic satisfiability

Describes a project that uses

Uses Software

• Chaff
• HeerHugo
• QUBOS
• SATO

This page was built for publication: QUBOS: Deciding quantified Boolean logic using propositional satisfiability solvers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4427904)