Topics for Personalized Projects
Suggestion: release results under MIT license
Extend SAT Solver
Clause learning, decision heuristics, lower-level data structures, restarts, evaluation
Solver suitable for a project:
- represent all clauses as one array of literals with indices into clauses, literals are Int-s (negative for negation)
- implement a resolution proof checker for sets of clauses, be able to write proof as list of clauses along with proof indicating parent clause and variable. load proof from a file
- add simple clause learning: add resolvent of clauses directly leading to a conflict
- add generation of resolution proof trees for UNSAT answers
- generate interpolants
DIMACS file format:
Enhancement Schemes for Constraint Processing: Backjumping, Learning, and Cutset Decomposition
Formal Verification of a Modern SAT Solver by Shallow Embedding into Isabelle/HOL
A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality
Verified SAT Solver
BDD Operations and Reachability Checking
Also heuristics for ordering
SAT Proof Generation and Interpolation Model Checking
Add proof generation (through simple clause learning), interpolant generation, interpolation-based model checking.