jix.one

Blog

Tags

All Blog Posts

2021

Proving 50-Year-Old Sorting Networks Optimal: Part 1

Posted on May 4th 2021, tagged sorting-networks

Introducing the problem of minimal size sorting networks and summarizing the previous state of the art.

2020

The Assembly Language of Satisfiability

Posted on October 3rd 2020, tagged sat

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

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.

Varisat 0.2.0 Released

Posted on May 4th 2019, tagged rust, sat

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

2018

Introducing Varisat

Posted on May 20th 2018, tagged rust, sat

Inroducing a CDCL SAT solver written in Rust.

Varisat 0.1.3: LRAT Generation and Proof Trimming

Posted on September 14th 2018, tagged rust, sat

Varisat can now directly output and trim LRAT proofs.

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.

Introducing partial_ref

Posted on December 24th 2018, tagged rust

Inroducing a Rust library to work around interprocedural borrowing conflicts.

2017

Pushing Polygons on the Mega Drive

Posted on May 16th 2017, tagged algorithms, demoscene, graphics

Write-up of the polygon renderer used for the Mega Drive demo “Overdrive 2”.

Not Even Coppersmith’s Attack

Posted on December 23rd 2017, tagged algorithms, cryptography

Factoring ROCA weak RSA keys without using Coppersmith’s method.