5 ms·
Nice work. Some things that I think work well for SMT solvers: 1. Bounded model checking for source code. 2. Finding solutions to constraint problems. 3. De
by nanolith 2y ago
Nice work.
Some things that I think work well for SMT solvers:
1. Bounded model checking for source code.
2. Finding solutions to constraint problems.
3. Design rule checking for hardware layout and logic gates.
Recently, I built a simple scheduling system using Z3. My wife is a librarian supervisor, and she's been spending hours each week creating schedules by hand. But, with a little Z3, one can enumerate the constraints and let it find a viable example. If the example doesn't work, add more constraints until it does.
- philzook 2y agoZ3 is a marvel. Even if this project is of no interest to a person, Z3 might be. I have intentionally, literally, used z3 data structures to make that transition easier should one find something intriguing here over top of what z3 offers.
- nanolith 2y agoI agree, and it's nice to have Python bindings for it.
- CoastalCoder 2y agoHow very cool! Can you give an example of the kinds of constraints that need to get tweaked? And do you have to tweak them in Z3 each time? Disclaimer: I know almost nothing about Z3. I'm just picturing you trying to convince her that something like datalog has a learning curve that she'll Totally Be Glad she Powered Through, and she'll Thank you Later for Talking he Into It :)
- nanolith 2y agoI wrote a simple DSL that she can use. She knows some HTML and basic scripting, so as long as the rules are easy to express and she has good examples, she can tweak the rules herself. I just hacked up a little shallow embedding via lex/yacc, using the C API. It's not pretty, but it was put together quickly to solve a problem. As for typical constraints, there needs to be people on certain desks at certain times. People have to take breaks between N and M hours after starting. People have off-desk time that they use to perform other tasks that must be managed and must be contiguous. People have different numbers of hours they have to work, and a finite amount of time that they are allowed to be on a particular desk on a given day or week.
- modeless 2y agoSounds like it would be easy to make a set of unsatisfiable constraints. How is that handled in Z3? Can you assign priorities to constraints or something?
- nanolith 2y agoYou can set soft and hard constraints. Soft constraints can be broken if the system is unsatisfiable otherwise. For instance, by default, this config sets a soft constraint that two people must be at the desk, and a hard constraint that no more than two people and at least one person must be at the desk. Likewise, there is a soft constraint that desk time must be contiguous, and a hard constraint that desk time must be at least so long to prevent continual splitting.