Have an option to use a SAT solver

jamesrayman / Polycube

A solver of polycube packing puzzles

MIT License

4 stars 0 forks source link

Have an option to use a SAT solver #18

Open jamesrayman opened 3 years ago

jamesrayman commented 3 years ago

I can't believe I didn't think of this earlier.

jamesrayman commented 3 years ago

Actually I can believe it. The z3 solver does terrible. Maybe I'll try swapping it out for Glucose, but it seems like using an exact cover solver is a better approach.

jamesrayman commented 3 years ago

Yeah I should really give this another go

jamesrayman commented 3 years ago

Solvers to interface:

[x] z3
[ ] Glucose
[ ] MiniSat
[ ] CryptoMiniSat

Exact cover to CNF conversion methods:

[x] Pairing
[ ] Bitwise
[ ] Ladder