Boolean satisfiability
Axeyum SAT Solver
A native CDCL solver with AIG and CNF lowering and certificate support.
New to SAT?
How can a set of ordinary yes-or-no rules become one exact formula?
Lesson 2 introduces Boolean formulas and assignments. Lesson 3 explains propagation, decisions, conflicts, learned clauses, and DRAT evidence.
Implementation
Axeyum implements its SAT solver in Rust. The solver accepts clauses produced by Axeyum's own lowering pipeline, searches with conflict-driven clause learning, and can emit evidence for selected unsat results.
The SAT solver is also the final decision layer for bit-blasted SMT queries. It remains a distinct component because its clauses, search behavior, and proof evidence can be tested without the SMT front end.
- CDCL search and learned clauses
- AIG construction and simplification
- CNF lowering
- DRAT evidence on supported routes
Rust crates
These crates implement the component or connect its results to another Axeyum checker. Each link opens the crate's source directory.
Reference systems and results
CaDiCaL and Kissat provide reference points for SAT solving and proof production.
Read SAT and SMT resultsProblems studied with this component
- Two four-color Rado numbers Combinatorics
- Optimal sorting networks on three to six channels Computer science