Stream: show and tell

Topic: rocsat -- a CDCL SAT solver in Roc

Matthieu Pizenberg (Aug 24 2026 at 10:03):

I wanted a reference SAT solver in Roc before re-implementing PubGrub dependency resolution for testing, so I’ve been writing it with agents: https://github.com/mpizenberg/rocsat

Here comes the agent description: It’s an ordinary CDCL — two-watched literals, 1-UIP learning, VSIDS, Luby restarts, clause deletion — plus DRAT proofs and a small incremental API with assumptions. About 2,900 lines of Roc on the new compiler. Performance is roughly MiniSat-class: on twenty SAT Competition 2025 instances at a 10 s timeout it solved 3, the same as MiniSat, against Kissat's 5 and CaDiCaL's 6.

Most of the effort went into finding shapes the compiler keeps in place rather than into the algorithm. Three open performance issues came out of it:

• roc#10848 — a list field in a record is copied on every write when the record is threaded through calls. The hot functions take lists and return them in tuples because of this; propagate has 13 parameters and returns a 13-tuple.
• roc#10849 — List.update copies the inner list, so List(List(_)) is quadratic. Watch lists became one flat List(U32) with hand-managed offsets.
• roc#10851 — a two-line helper in a hot loop isn't inlined and costs about 7x.

Plus one compiler crash, roc#10847. Each was easy to work around once found; the catch is that they're invisible without a benchmark, so the repo keeps a timing canary with a hard ceiling to notice a future nightly flipping one of these shapes.

Enjoy!

Anton (Aug 24 2026 at 12:37):

2,900 lines of Roc

Nice :)

Lukas Juhrich (Aug 25 2026 at 23:14):

This is impressive!

Last updated: Sep 03 2026 at 15:16 UTC