Clause Elimination for SAT and QSAT

DOI10.1613/jair.4694zbMath1336.68231OpenAlexW2212515300MaRDI 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

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