Resolution for quantified Boolean formulas
From MaRDI portal
Publication:1891159
DOI10.1006/inco.1995.1025zbMath0828.68045OpenAlexW1976876676WikidataQ55889272 ScholiaQ55889272MaRDI QIDQ1891159
Hans Kleine Büning, Andreas Flögel, Marek Karpinski
Publication date: 28 May 1995
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1006/inco.1995.1025
Analysis of algorithms and problem complexity (68Q25) Logic programming (68N17) Word problems, etc. in computability and recursion theory (03D40)
Related Items
Quantified maximum satisfiability, Solution validation and extraction for QBF preprocessing, Hardness Characterisations and Size-width Lower Bounds for QBF Resolution, Erratum to: ``Analyzing restricted fragments of the theory of linear arithmetic, The QBF Gallery: behind the scenes, Quantifier reordering for QBF, Feasible Interpolation for QBF Resolution Calculi, The complexity of constraint satisfaction games and QCSP, QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving, Unnamed Item, Backdoors to Satisfaction, Equilibrium logic, Boolean functions as models for quantified Boolean formulas, Relating size and width in variants of Q-resolution, Conformant planning as a case study of incremental QBF solving, A simple proof of QBF hardness, Lower Bound Techniques for QBF Proof Systems, Long-distance Q-resolution with dependency schemes, Unnamed Item, Soundness of \(\mathcal{Q}\)-resolution with dependency schemes, Never trust your solver: certification for SAT and QBF, A game characterisation of tree-like Q-resolution size, Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution, Capturing the polynomial hierarchy by second-order revised Krom logic, Towards Uniform Certification in QBF, Level-ordered \(Q\)-resolution and tree-like \(Q\)-resolution are incomparable, Subsumption-linear Q-resolution for QBF theorem proving, A satisfiability procedure for quantified Boolean formulae, Quantified Constraint Satisfaction and the Polynomially Generated Powers Property, On the exact complexity of evaluating quantified \(k\)-\textsc{cnf}, Henkin quantifiers and Boolean formulae: a certification perspective of DQBF, Unified QBF certification and its applications, Quantified Constraints in Twenty Seventeen, Bounded-width QBF is PSPACE-complete, Out of order quantifier elimination for standard quantified linear programs, Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems, Models and quantifier elimination for quantified Horn formulas, Failed Literal Detection for QBF, Lower bound techniques for QBF expansion, Analyzing restricted fragments of the theory of linear arithmetic, Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers, Quantified constraint satisfaction and the polynomially generated powers property, Lower bounds for QCDCL via formula gauge, On deciding subsumption problems, Characterising tree-like Frege proofs for QBF, Computational methods for database repair by signed formulae, Unnamed Item, A Unified Framework for Certificate and Compilation for QBF, Understanding cutting planes for QBFs, On the Exact Complexity of Evaluating Quantified k-CNF, Building strategies into QBF proofs, Blocked Clause Elimination for QBF, A Game Characterisation of Tree-like Q-resolution Size, Short proofs for some symmetric quantified Boolean formulas, Existentially restricted quantified constraint satisfaction, The complexity of satisfiability problems: Refining Schaefer's theorem, On Q-Resolution and CDCL QBF Solving, On Stronger Calculi for QBFs, Q-Resolution with Generalized Axioms, Lifting QBF Resolution Calculi to DQBF, Long Distance Q-Resolution with Dependency Schemes, HordeQBF: A Modular and Massively Parallel QBF Solver, Using decomposition-parameters for QBF: mind the prefix!, Validating QBF Validity in HOL4, Dual proof generation for quantified Boolean formulas with a BDD-based solver, A self-adaptive multi-engine solver for quantified Boolean formulas, Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations, Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits, A Compact Representation for Syntactic Dependencies in QBFs, BDD-based decision procedures for the modal logic K ★, Unnamed Item, Learning to Integrate Deduction and Search in Reasoning about Quantified Boolean Formulas, Reinterpreting dependency schemes: soundness meets incompleteness in DQBF, Backdoor sets of quantified Boolean formulas, Unnamed Item, Expansion-based QBF solving versus Q-resolution, How QBF expansion makes strategy extraction hard, The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1, CAQE and QuAbS: Abstraction Based QBF Solvers, On the restricted equivalence for subclasses of propositional logic, On Quantifying Literals in Boolean Logic and its Applications to Explainable AI, Solving QBF with counterexample guided refinement, Backjumping for quantified Boolean logic satisfiability, QBFFam: a tool for generating QBF families from proof complexity, Davis and Putnam meet Henkin: solving DQBF with resolution, Lower bounds for QCDCL via formula gauge, Hardness and optimality in QBF proof systems modulo NP, Proof complexity of symbolic QBF reasoning
