The following pages link to Inprocessing Rules (Q2908507):
Displaying 35 items.
- The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Q286790) (← links)
- SAT race 2015 (Q334795) (← links)
- Algorithms for computing minimal equivalent subformulas (Q460638) (← links)
- On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers (Q823775) (← links)
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs (Q832719) (← links)
- Automatically improving constraint models in Savile Row (Q1680696) (← links)
- Efficient, verified checking of propositional proofs (Q1687744) (← links)
- A flexible proof format for SAT solver-elaborator communication (Q2044190) (← links)
- Non-clausal redundancy properties (Q2055860) (← links)
- Covered clauses are not propagation redundant (Q2096437) (← links)
- Clause redundancy and preprocessing in maximum satisfiability (Q2104499) (← links)
- Preprocessing of propagation redundant clauses (Q2104502) (← links)
- Hash-based preprocessing and inprocessing techniques in SAT solvers (Q2118288) (← links)
- Assessing progress in SAT solvers through the Lens of incremental SAT (Q2118309) (← links)
- XOR local search for Boolean Brent equations (Q2118332) (← links)
- Simulating strong practical proof systems with extended resolution (Q2209554) (← links)
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML (Q2233509) (← links)
- Clause vivification by unit propagation in CDCL SAT solvers (Q2287199) (← links)
- Strong extension-free proof systems (Q2303251) (← links)
- Set-blocked clause and extended set-blocked clause in first-order logic (Q2333858) (← links)
- On preprocessing techniques and their impact on propositional model counting (Q2362107) (← links)
- Solution validation and extraction for QBF preprocessing (Q2362496) (← links)
- Conformant planning as a case study of incremental QBF solving (Q2398267) (← links)
- Super-Blocked Clauses (Q2817910) (← links)
- Extreme Cases in SAT Problems (Q2818004) (← links)
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer (Q2818017) (← links)
- Predicate Elimination for Preprocessing in First-Order Theorem Proving (Q2818027) (← links)
- LMHS: A SAT-IP Hybrid MaxSAT Solver (Q2818041) (← links)
- SpyBug: Automated Bug Detection in the Configuration Space of SAT Solvers (Q2818043) (← links)
- DRAT Proofs for XOR Reasoning (Q2835888) (← links)
- An Expressive Model for Instance Decomposition Based Parallel SAT Solvers (Q2964456) (← links)
- Propositional SAT Solving (Q3176367) (← links)
- Truth Assignments as Conditional Autarkies (Q3297584) (← links)
- Preprocessing of propagation redundant clauses (Q6053844) (← links)
- Mining definitions in Kissat with Kittens (Q6056639) (← links)
