jix.one

Blog Posts Tagged ‘refactoring-varisat’

2019

Refactoring Varisat: 1. Basics and Parsing

Posted on February 3rd 2019, tagged refactoring-varisat, rust, sat

Refactoring my CDCL based SAT solver written in Rust.

Refactoring Varisat: 2. Clause Storage and Unit Propagation

Posted on March 2nd 2019, tagged algorithms, refactoring-varisat, rust, sat

Implementing a clause allocator and watchlist based unit propagation.

Refactoring Varisat: 3. Conflict Driven Clause Learning

Posted on March 18th 2019, tagged algorithms, refactoring-varisat, rust, sat

Implementing search using decisions and clause learning.

Refactoring Varisat: 4. Heuristics

Posted on March 21st 2019, tagged refactoring-varisat, rust, sat

Implementing heuristics for decisions, restarts and clause deletions. Also clause minimization.

Refactoring Varisat: 5. Incremental Solving and Proofs

Posted on April 26th 2019, tagged refactoring-varisat, rust, sat

Implementing assumption based incremental solving and proof logging, including LRAT proof logging.