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.

Implement IC3 (PDR)

Case Study: Verified Algorithm or Data Structure in Isabelle

Case Study: Verified Algorithm or Data Structure in Coq

Case Study: Verified Algorithm or Data Structure in Stainless

Extend Functionality of Stainless