Inprocessing Rules

DOI10.1007/978-3-642-31365-3_28zbMath1358.68256OpenAlexW2913257024MaRDI QIDQ2908507

Armin Biere, Matti Järvisalo, Marijn J. H. Heule

Publication date: 5 September 2012

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-31365-3_28

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (49)

On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers ⋮ On preprocessing techniques and their impact on propositional model counting ⋮ Solution validation and extraction for QBF preprocessing ⋮ The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs ⋮ HordeSat: A Massively Parallel Portfolio SAT Solver ⋮ Using Community Structure to Detect Relevant Learnt Clauses ⋮ Evaluating CDCL Variable Scoring Schemes ⋮ Propositional SAT Solving ⋮ Expressing Symmetry Breaking in DRAT Proofs ⋮ SAT race 2015 ⋮ Conformant planning as a case study of incremental QBF solving ⋮ Automatically improving constraint models in Savile Row ⋮ Mining definitions in Kissat with Kittens ⋮ Efficient, verified checking of propositional proofs ⋮ Never trust your solver: certification for SAT and QBF ⋮ An Expressive Model for Instance Decomposition Based Parallel SAT Solvers ⋮ Simulating strong practical proof systems with extended resolution ⋮ Algorithms for computing minimal equivalent subformulas ⋮ Truth Assignments as Conditional Autarkies ⋮ \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML ⋮ Preprocessing of propagation redundant clauses ⋮ Unnamed Item ⋮ On Incremental Pre-processing for SMT ⋮ A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper) ⋮ Unnamed Item ⋮ Unsatisfiability proofs for distributed clause-sharing SAT solvers ⋮ Clausal proofs for pseudo-Boolean reasoning ⋮ Clause vivification by unit propagation in CDCL SAT solvers ⋮ Certified SAT solving with GPU accelerated inprocessing ⋮ The resolution of Keller's conjecture ⋮ A flexible proof format for SAT solver-elaborator communication ⋮ Strong extension-free proof systems ⋮ Super-Blocked Clauses ⋮ Extreme Cases in SAT Problems ⋮ Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer ⋮ Predicate Elimination for Preprocessing in First-Order Theorem Proving ⋮ LMHS: A SAT-IP Hybrid MaxSAT Solver ⋮ SpyBug: Automated Bug Detection in the Configuration Space of SAT Solvers ⋮ Non-clausal redundancy properties ⋮ DRAT Proofs for XOR Reasoning ⋮ Set-blocked clause and extended set-blocked clause in first-order logic ⋮ Covered clauses are not propagation redundant ⋮ The resolution of Keller's conjecture ⋮ Clause redundancy and preprocessing in maximum satisfiability ⋮ Preprocessing of propagation redundant clauses ⋮ Hash-based preprocessing and inprocessing techniques in SAT solvers ⋮ Assessing progress in SAT solvers through the Lens of incremental SAT ⋮ XOR local search for Boolean Brent equations

This page was built for publication: Inprocessing Rules