Blog Posts Tagged ‘sat’

2020

The Assembly Language of Satisfiability

How SAT solvers relate to higher level tools like SMT solvers.

2019

Varisat 0.2.0 Released

Release of my refactored CDCL based SAT solver written in Rust.

Refactoring Varisat: 5. Incremental Solving and Proofs

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

Refactoring Varisat: 4. Heuristics

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

Refactoring Varisat: 3. Conflict Driven Clause Learning

Implementing search using decisions and clause learning.

Refactoring Varisat: 2. Clause Storage and Unit Propagation

Implementing a clause allocator and watchlist based unit propagation.

Refactoring Varisat: 1. Basics and Parsing

Refactoring my CDCL based SAT solver written in Rust.

2018

Encoding Matrix Rank for SAT Solvers

Using a variant of the LU-decomposition to encode matrix rank constraints for SAT and SMT solvers.

Varisat 0.1.3: LRAT Generation and Proof Trimming

Varisat can now directly output and trim LRAT proofs.

Introducing Varisat

Inroducing a CDCL SAT solver written in Rust.