Clause Elimination for SAT and QSAT

DOI10.1613/JAIR.4694zbMath1336.68231OpenAlexW2212515300WikidataQ129489075 ScholiaQ129489075MaRDI QIDQ2941732

Martina Seidl, Matti Järvisalo, Armin Biere, Marijn J. H. Heule, Florian Lonsing

Publication date: 25 August 2015

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

Full work available at URL: https://doi.org/10.1613/jair.4694

Mathematics Subject Classification ID

Related Items (21)

On preprocessing techniques and their impact on propositional model counting ⋮ Solution validation and extraction for QBF preprocessing ⋮ Conformant planning as a case study of incremental QBF solving ⋮ Mining definitions in Kissat with Kittens ⋮ OuterCount: a first-level solution-counter for quantified Boolean formulas ⋮ Never trust your solver: certification for SAT and QBF ⋮ True crafted formula families for benchmarking quantified satisfiability solvers ⋮ Contradiction separation based dynamic multi-clause synergized automated deduction ⋮ Logical reduction of metarules ⋮ Truth Assignments as Conditional Autarkies ⋮ Unnamed Item ⋮ New models for generating hard random Boolean formulas and disjunctive logic programs ⋮ Solving Advanced Argumentation Problems with Answer Set Programming ⋮ Super-Blocked Clauses ⋮ Q-Resolution with Generalized Axioms ⋮ HordeQBF: A Modular and Massively Parallel QBF Solver ⋮ Non-clausal redundancy properties ⋮ Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations ⋮ Covered clauses are not propagation redundant ⋮ The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1 ⋮ Clause redundancy and preprocessing in maximum satisfiability

This page was built for publication: Clause Elimination for SAT and QSAT