this post was submitted on 20 Sep 2026
55 points (98.2% liked)

Programmer Humor

33288 readers
835 users here now

Welcome to Programmer Humor!

This is a place where you can post jokes, memes, humor, etc. related to programming!

For sharing awful code theres also Programming Horror.

Rules

founded 3 years ago
MODERATORS
 

It turns out you can make a really fast instruction decoder in Scrap Mechanic if only you can figure out a special bit mask for each ALU operation. It turns out this is really frickity fucking hard to do by hand so I told a SAT solver to do it and it was fine until I asked for all the combinations I wanted and then... This.

out.dimacs is 36MB

c CNF file written by RustSAT  
p cnf 217953 1366264  

Also dimacs uses "c" for comments lol (it's just a huge file of numbers).

Also also it turns out using 100% of all 24 cores on a laptop for 8 hours makes for some heat issues so I had to limit each core to 50% utilization so it will take twice as long yay.

UPDATE: it's been 18 hours and the best it's got it 3.925%. If I linearly extrapolate, it will take 400-500 hours ≈ 2.5-3 weeks.

UPDATE 2: I've turned it off, as I don't have more than a weekend to just leave my laptop sitting around.

top 5 comments
sorted by: hot top controversial new old
[–] edinbruh@feddit.it 5 points 12 hours ago (1 children)

Maybe you should play with heuristics to get a good enough solution quickly. Or change solver to something more appropriate for what you are modelling

[–] jjj@piefed.blahaj.zone 1 points 4 hours ago* (last edited 4 hours ago)

Based on my other comment, do you have any in mind that would be more appropriate?

[–] ColbysBrush@fedinsfw.app 2 points 11 hours ago (1 children)

What, specifically, are you trying to solve?

[–] jjj@piefed.blahaj.zone 2 points 4 hours ago

For each operation my CPU's ALU can do, I need to find a bit mask that turns it on only for the desired set of 8 bit opcodes. The bit mask is of the form [01_].[01_][01_][01_][01_][01_][01_][01_][01_] where 0 and 1 mean the bit has to match and _ means it doesn't matter. The bit before the . is the xor of all the other bits in the opcode.

The solver has to figure out both which opcodes represent each instruction and what bit masks are needed to give them the desired operations.

I'm just excited that Z3 has a parallel mode now. Last time I was using it much, it was only single core.