Blog
Tags
All Blog Posts
2021
Proving 50-Year-Old Sorting Networks Optimal: Part 2
Partial sorting networks and recursive minimal size computation.
Proving 50-Year-Old Sorting Networks Optimal: Part 1
Introducing the problem of minimal size sorting networks and summarizing the previous state of the art.
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
Introducing partial_ref
Inroducing a Rust library to work around interprocedural borrowing conflicts.
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.
2017
Not Even Coppersmith’s Attack
Factoring ROCA weak RSA keys without using Coppersmith’s method.
Pushing Polygons on the Mega Drive
Write-up of the polygon renderer used for the Mega Drive demo “Overdrive 2”.