Blog by Jannis Harder
A proof that uniformly random high-degree regular graphs are asymptotically almost surely link-irregular, providing another counterexample to a recent conjecture.
Partial sorting networks and recursive minimal size computation.
Introducing the problem of minimal size sorting networks and summarizing the previous state of the art.
How SAT solvers relate to higher level tools like SMT solvers.
Release of my refactored CDCL based SAT solver written in Rust.
Implementing assumption based incremental solving and proof logging, including LRAT proof logging.
Implementing heuristics for decisions, restarts and clause deletions. Also clause minimization.
Implementing search using decisions and clause learning.
Implementing a clause allocator and watchlist based unit propagation.
Refactoring my CDCL based SAT solver written in Rust.
Inroducing a Rust library to work around interprocedural borrowing conflicts.
Using a variant of the LU-decomposition to encode matrix rank constraints for SAT and SMT solvers.
Varisat can now directly output and trim LRAT proofs.
Inroducing a CDCL SAT solver written in Rust.
Factoring ROCA weak RSA keys without using Coppersmith’s method.
Write-up of the polygon renderer used for the Mega Drive demo “Overdrive 2”.