DRAT-trim
From MaRDI portal
Cited in
(only showing first 100 items - show all)- kcnfs
- ChvatalIP
- Exact SCIP
- PReLearn
- Goeland
- FRAT
- Sylvan
- PaPILO
- Dsharp
- Paracooba
- Kissat
- SLIME
- cake_lpr
- SBSAT
- WALA
- Machine learning-based restart policy for CDCL SAT solvers
- A little blocked literal goes a long way
- Efficient, verified checking of propositional proofs
- QSopt_ex
- A semantic framework for proof evidence
- \({\textsf{QRAT}}^{+}\): generalizing QRAT by a more powerful QBF redundancy property
- Investigating the existence of large sets of idempotent quasigroups via satisfiability testing
- Extended resolution simulates \({\mathsf{DRAT}}\)
- NiVER
- Plingeling
- PicoSAT
- SMTInterpol
- CLSAT
- versat
- SAT competition 2020
- Flexible proof production in an industrial-strength SMT solver
- Preprocessing of propagation redundant clauses
- ProCount: weighted projected model counting with graded project-join trees
- On crossing-families in planar point sets
- Bloqqer
- DepQBF
- Equinox
- DRAT-based bit-vector proofs in CVC4
- Guiding high-performance SAT solvers with unsat-core predictions
- CrystalBall: gazing in the black box of SAT solving
- D-FLAT
- CryptoMiniSat
- Simulating strong practical proof systems with extended resolution
- tawSolver
- Strong extension-free proof systems
- Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
- Solution validation and extraction for QBF preprocessing
- Skeptik
- Computing the Ramsey number \(R(4,3,3)\) using abstraction and symmetry breaking
- Verifying integer programming results
- Efficient certified RAT verification
- Autoref
- Treengeling
- MathCheck
- Lynx
- Proof checking and logic programming
- libclang
- QMaxSATpb: a certified MaxSAT solver
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- DRAT proofs for XOR reasoning
- sharpSAT
- Coprocessor
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- An expressive model for instance decomposition based parallel SAT solvers
- VIPR
- COMiniSatPS
- Jimple
- GPU-PRISM
- GPUexplore
- SageSAT
- Truth assignments as conditional autarkies
- Shatter
- Teyjus
- LRAT
- MaxPre
- GRAT
- GRATchk
- Expressing symmetry breaking in DRAT proofs
- Compositional propositional proofs
- multi2boolean
- CAQE
- FlowDroid
- conauto
- Lingeling
- ZRes
- HQSpre
- Imperative Refinement
- BooleForce
- YalSAT
- CaDiCaL
- IEEE_Floating_Point
- SMTCoq
- Local redundancy in SAT: generalizations of blocked clauses
- Local negative circuits and cyclic attractors in Boolean networks with at most five components
- DRAT and propagation redundancy proofs without new variables
- Nonexistence Certificates for Ovals in a Projective Plane of Order Ten
- A flexible proof format for SAT solver-elaborator communication
- Inconsistency proofs for ASP: the ASP-DRUPE format
- GenMul
- egg
This page was built for software: DRAT-trim
