Blog Posts Tagged ‘refactoring-varisat’
Refactoring Varisat: 1. Basics and Parsing
Refactoring my CDCL based SAT solver written in Rust.
Refactoring Varisat: 2. Clause Storage and Unit Propagation
Implementing a clause allocator and watchlist based unit propagation.
Refactoring Varisat: 3. Conflict Driven Clause Learning
Implementing search using decisions and clause learning.
Refactoring Varisat: 4. Heuristics
Implementing heuristics for decisions, restarts and clause deletions. Also clause minimization.
Refactoring Varisat: 5. Incremental Solving and Proofs
Implementing assumption based incremental solving and proof logging, including LRAT proof logging.