A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper)
From MaRDI portal
Publication:6492741
DOI10.1007/978-3-031-38499-8_12MaRDI QIDQ6492741
Publication date: 26 April 2024
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Unnamed Item
- Unnamed Item
- Isabelle/HOL. A proof assistant for higher-order logic
- A verified SAT solver framework with learn, forget, restart, and incrementality
- Refinement to imperative HOL
- Incremental inprocessing in SAT solving
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
- versat: A Verified Modern SAT Solver
- Inprocessing Rules
- DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
- Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
- Imperative Functional Programming with Isabelle/HOL
- Code Generation via Higher-Order Rewrite Systems
- Better Decision Heuristics in CDCL through Local Search and Target Phases
- Automatic Data Refinement
- Efficient verified (UN)SAT certificate checking
This page was built for publication: A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper)
