|
|
|
|
|
|
by _0ffh
1115 days ago
|
|
|
I wrote a bespoke backtracking solver for a specific class of problems. Would love to use Z3 or something, but frankly, I wouldn't know how to systematically translate problem instances to solver constraints. It's essentially a kind of very complex job-shop scheduling problem with lots of dynamic inter-dependencies. Many of the problems are hard to even solve without dead-locking, while we also naturally strive to minimize overall processing time. Where would I find ressources to help me get a grip on my specific problem [1]? Could I reasonably hope that Z3 or another general solver might be faster than a moderately well designed bespoke solver in a compiled language? (My solver combines a bunch of greedy heuristics with a backtracker in case it runs into a dead-lock, which is often.) [1] Rough problem outline: Input goods must be transformed through a complex series of assembly/machining/processing lines to output goods; each line transforms one or two inputs into an (intermediary or end-) product; an assembly line produces it's product in a fixed number of time units and cannot be stopped or delayed; finished intermediary products arrive at the end of an assembly line, which must be cleared by then; there are a limited number of temporary storage spaces where intermediary products can be moved to/from in a fixed number of time units; some assembly lines must wait for two intermediary products to be completed to start a job combining them into another intermediary or end product; end products must then be moved to their destinations. |
|
|
I’m no SMT expert, but the way I’ve done it is to make some representation in Python Z3, and then write some function or class that generates those. I was solving MLB eliminations (more complex than it sounds) and I think I used arrays of ints for number of wins. So I’d pull MLB data, turn that into schedule objects which turned themselves into z3 constraints.