Inprocessing Rules
From MaRDI portal
Publication:2908507
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
Related Items
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, Unnamed Item, Clause vivification by unit propagation in CDCL SAT solvers, 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
