Blog Posts Tagged ‘sat’
The Assembly Language of Satisfiability
Posted on October 3rd 2020, tagged sat
How SAT solvers relate to higher level tools like SMT solvers.
Varisat 0.2.0 Released
Release of my refactored CDCL based SAT solver written in Rust.
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.
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: 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: 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: 1. Basics and Parsing
Posted on February 3rd 2019, tagged refactoring-varisat, rust, sat
Refactoring my CDCL based SAT solver written in Rust.
Encoding Matrix Rank for SAT Solvers
Posted on December 7th 2018, tagged sat
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.
Inroducing a CDCL SAT solver written in Rust.