Theory and Applications of Satisfiability Testing
From MaRDI portal
Publication:5714773
DOI10.1007/11527695zbMath1122.68585OpenAlexW2483910514MaRDI QIDQ5714773
Publication date: 16 December 2005
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11527695
Related Items
Backdoors to Normality for Disjunctive Logic Programs ⋮ Solution validation and extraction for QBF preprocessing ⋮ Preprocessing for DQBF ⋮ Solving quantified constraint satisfaction problems ⋮ Symbolic techniques in satisfiability solving ⋮ Conformant planning as a case study of incremental QBF solving ⋮ Mining definitions in Kissat with Kittens ⋮ Never trust your solver: certification for SAT and QBF ⋮ Symbolic algorithmic verification of intransitive generalized noninterference ⋮ Efficiently solving quantified bit-vector formulas ⋮ Incremental preprocessing methods for use in BMC ⋮ Quantifier elimination by dependency sequents ⋮ Models and quantifier elimination for quantified Horn formulas ⋮ Failed Literal Detection for QBF ⋮ Ranking function synthesis for bit-vector relations ⋮ Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers ⋮ A Unified Framework for Certificate and Compilation for QBF ⋮ Blocked Clause Elimination for QBF ⋮ Predicate Elimination for Preprocessing in First-Order Theorem Proving ⋮ Incremental Determinization ⋮ Q-Resolution with Generalized Axioms ⋮ Dependency Schemes for DQBF ⋮ Dual proof generation for quantified Boolean formulas with a BDD-based solver ⋮ A self-adaptive multi-engine solver for quantified Boolean formulas ⋮ A solver for QBFs in negation normal form ⋮ A Compact Representation for Syntactic Dependencies in QBFs ⋮ Beyond CNF: A Circuit-Based QBF Solver ⋮ Quantor ⋮ Learning to Integrate Deduction and Search in Reasoning about Quantified Boolean Formulas ⋮ Backdoor sets of quantified Boolean formulas ⋮ Compressing BMC Encodings with QBF ⋮ The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1 ⋮ CAQE and QuAbS: Abstraction Based QBF Solvers ⋮ SAT-Inspired Eliminations for Superposition ⋮ Proof complexity of symbolic QBF reasoning
