Inprocessing rules
From MaRDI portal
Recommendations
Cited in
(59)- On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers
- Reconstructing solutions after blocked clause elimination
- Local redundancy in SAT: generalizations of blocked clauses
- Clause redundancy and preprocessing in maximum satisfiability
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
- Using Community Structure to Detect Relevant Learnt Clauses
- Certified SAT solving with GPU accelerated inprocessing
- Conformant planning as a case study of incremental QBF solving
- Set-blocked clause and extended set-blocked clause in first-order logic
- On preprocessing techniques and their impact on propositional model counting
- HordeSat: a massively parallel portfolio SAT solver
- Algorithms for computing minimal equivalent subformulas
- Hash-based preprocessing and inprocessing techniques in SAT solvers
- XOR local search for Boolean Brent equations
- Clause simplifications in search-space decomposition-based SAT solvers
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- Expressing symmetry breaking in DRAT proofs
- Predicate Elimination for Preprocessing in First-Order Theorem Proving
- Extreme cases in SAT problems
- Propositional SAT solving
- An expressive model for instance decomposition based parallel SAT solvers
- Soundness of inprocessing in clause sharing SAT solvers
- Simulating strong practical proof systems with extended resolution
- Preprocessing of propagation redundant clauses
- RAT elimination
- Preprocessing of propagation redundant clauses
- Mining definitions in Kissat with Kittens
- Satisfiability modulo user propagators
- Using Boolean Constraint Propagation for Sub-clauses Deduction
- A flexible proof format for SAT solver-elaborator communication
- scientific article; zbMATH DE number 7566059 (Why is no real title available?)
- SAT race 2015
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- Super-blocked clauses
- DRAT proofs for XOR reasoning
- Unsatisfiability proofs for distributed clause-sharing SAT solvers
- The resolution of Keller's conjecture
- The resolution of Keller's conjecture
- Evaluating CDCL variable scoring schemes
- Non-clausal redundancy properties
- Dynamic blocked clause elimination for projected model counting
- Covered clauses are not propagation redundant
- Assessing progress in SAT solvers through the Lens of incremental SAT
- Automatically improving constraint models in Savile Row
- Truth assignments as conditional autarkies
- LMHS: a SAT-IP hybrid MaxSat solver
- Strong extension-free proof systems
- Incremental inprocessing in SAT solving
- A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper)
- On Incremental Pre-processing for SMT
- Solution validation and extraction for QBF preprocessing
- Theory and Applications of Satisfiability Testing
- Clause vivification by unit propagation in CDCL SAT solvers
- Efficient, verified checking of propositional proofs
- Lower bounds for set-blocked clauses proofs
- Clausal proofs for pseudo-Boolean reasoning
- Never trust your solver: certification for SAT and QBF
- SpyBug: automated bug detection in the configuration space of SAT solvers
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
This page was built for publication: Inprocessing rules
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2908507)
