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.
::: spoiler 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.
10 Comments
edinbruh@feddit.it · 9 pts · 4d
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 · 2 pts · 4d
Based on my other comment, do you have any in mind that would be more appropriate?
edinbruh@feddit.it · 4 pts · 4d
I think a "constraint propagation" based solver should work well. So you can try using minizinc and play with the solvers it gives you. Using gecode and heuristics it can get very fast (try using relax_and_reconstruct, together with restart_luby and indomain_random, to obtain a simple LNS. Or you can use Google's OR tools solver, that is based on ILP and is very fast, and can run multithreaded.
You can also go fully ILP, and model your problem in ampl, and try some free (e.g. glpk) or commercial (e.g. gurobi) ILP solver.
I doubt it helps, but there's always SMT solvers (e.g. cvc5), which I don't think can be faster but is surely easier to model than a pure SAT. And there's also ASP solvers like clingo (clasp+gringo), that are purely logic based and implement common-sense-reasoning.
edinbruh@feddit.it · 1 pts · 1d
Well? How did it go?
jjj@piefed.blahaj.zone · 2 pts · 21h
Nice timing, I just finished it!
I was able to adjust the bit mask format to be easier to work with by hand and got it most of the way, then used the SAT solver to quickly finish the rest when I got stuck.
edinbruh@feddit.it · 1 pts · 15h
Nice
duckythescientist@sh.itjust.works · 4 pts · 4d
I'm just excited that Z3 has a parallel mode now. Last time I was using it much, it was only single core.
ColbysBrush@fedinsfw.app · 3 pts · 4d
What, specifically, are you trying to solve?
jjj@piefed.blahaj.zone · 5 pts · 4d
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.
::: spoiler EDIT
I ultimately switched to a slightly different approach. It turns out the xor part of the mask isn't very useful since the combinations I need aren't super complicated. The trouble was that an operation could only trigger for a power of 2 of opcodes, so I added a secondary mask to each operation:
Base mask: still
[01_]x8\Secondary mask:
[01_x]x8 (x means both 0 and 1)For the secondary mask, 1 matches only if the current bit or the one to the left is true (left of the leftmost is the rightmost). 0 is the same but with nand in stead of or. x, requiring both, only matches if exactly one matches.
Using 1 or 0 multiplies the number of matching opcodes by 3/4 (or a more complicated fraction if their areas of influence overlap), which allows much more freedom.
Due to restrictions in the game and my "hard"ware, I'm only able to use
[1_x]for the secondary mask, since a nand gate doesn't respond right to being hooked up to a bunch of toggleable and inputs but xor/or gates do (xor is just as fast in game). :::MadhuGururajan@programming.dev · 2 pts · 2d
I think you're trying to solve a NP Complete problem (Boolean Satisfiability) via brute force. It's expected you will hit this wall. Try to use heuristics/guess work.