swMATH13313MaRDI QIDQ25228FDOQ25228
Author name not available (Why is that?)
Official website: http://www.cs.utexas.edu/~marijn/drat-trim/
Cited In (only showing first 100 items - show all)
- Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
- Two disjoint 5-holes in point sets
- CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver
- Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
- A proof system for graph (non)-isomorphism verification
- Computing the Ramsey number \(R(4,3,3)\) using abstraction and symmetry breaking
- Kissat
- Paracooba
- Sylvan
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- Expressing symmetry breaking in DRAT proofs
- Proof checking and logic programming
- Proof checking and logic programming
- An expressive model for instance decomposition based parallel SAT solvers
- Simulating strong practical proof systems with extended resolution
- Preprocessing of propagation redundant clauses
- DRAT-based bit-vector proofs in CVC4
- Investigating the existence of large sets of idempotent quasigroups via satisfiability testing
- Efficient certified RAT verification
- Machine learning-based restart policy for CDCL SAT solvers
- Title not available (Why is that?)
- A Safe Computational Framework for Integer Programming Applied to Chvátal’s Conjecture
- A computational status update for exact rational mixed integer programming
- WALA
- QSopt_ex
- NiVER
- PicoSAT
- Plingeling
- SMTInterpol
- CLSAT
- versat
- Bloqqer
- DepQBF
- Equinox
- D-FLAT
- CryptoMiniSat
- tawSolver
- Skeptik
- Autoref
- Lynx
- MathCheck
- Treengeling
- libclang
- Coprocessor
- sharpSAT
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- COMiniSatPS
- Jimple
- VIPR
- GPU-PRISM
- GPUexplore
- SageSAT
- Shatter
- LRAT
- GRAT
- GRATchk
- MaxPre
- Teyjus
- multi2boolean
- CAQE
- FlowDroid
- conauto
- Lingeling
- HQSpre
- BooleForce
- Imperative Refinement
- ZRes
- CaDiCaL
- IEEE_Floating_Point
- YalSAT
- SMTCoq
- GenMul
- egg
- multgen
- cnf2aig
- ChvatalIP
- Exact SCIP
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
- Dsharp
- A nonexistence certificate for projective planes of order ten with weight 15 codewords
- A little blocked literal goes a long way
- Efficient, verified checking of propositional proofs
- PReLearn
- Goeland
- FRAT
- PaPILO
- cake_lpr
- SLIME
- A semantic framework for proof evidence
- SAT competition 2020
- Local redundancy in SAT: generalizations of blocked clauses
- Arg2P
- QMaxSATpb
- TBUDDY
- Transition_Systems_and_Automata
- Flexible proof production in an industrial-strength SMT solver
- Compositional propositional proofs
- DRABT
- BoSy
- ProCount: weighted projected model counting with graded project-join trees
This page was built for software: DRAT-trim
