3 ms·

This is my windmill tilting project. Pretty raw off the bench kind of stuff, but I'm interested to hear what kinds of things people would use this kind of thing

This is my windmill tilting project. Pretty raw off the bench kind of stuff, but I'm interested to hear what kinds of things people would use this kind of thing for or ways to make this more understandable to an audience not soaked in formalism.

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 ago
  Z3 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 ago
    I agree, and it's nice to have Python bindings for it.
- CoastalCoder 2y ago
  How 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 ago
    I 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 ago
      Sounds 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 ago
        You 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.
        modeless 2y ago
        But if there is a choice between breaking two soft constraints, how does it choose?
        nanolith 2y ago
        You can set weights for each soft constraint to control how easy they are to break.
0cf8612b2e1e 2y ago
I have used z3 for a job scheduling problem. I had a piece of equipment which can handle capacity X, jobs come in at known intervals and are available for given durations of varying lengths, some jobs come in multiple times, some jobs must be done above all others. Which jobs should be assigned to the equipment to maximize completed jobs while not missing the high priority entries? Numbers were such that you could only ever handle a fraction of the possible work. The throughout of a good allocation could be significantly higher than a naive one.
nextaccountic 2y ago
Nice work! So you wanted to avoid to work with epsilon-delta in the reals Question, do you use intuitionistic logic or classical logic? If you use intuitionistic logic, why not model smooth infinitesimal analysis? https://publish.uwo.ca/~jbell/invitation%20to%20SIA.pdf https://publish.uwo.ca/~jbell/invitation%20to%20SIA.pdf
- philzook 2y ago
  That's a an interesting suggestion! By design, I can swap out or export to nanoCoP-i https://leancop.de/nanocop-i/ https://leancop.de/nanocop-i/ , an intuitionistic prover, but I haven't had a good theory the play with. I was considering maybe an intuitionistic set theory, but this seems like a good case too.
  - nextaccountic 2y ago
    Ok so I want to link A Primer of Infinitesimal Analysis https://www.cambridge.org/core/books/primer-of-infinitesimal-analysis/B0EF33F73CAF97C180897D2FD0AD1B6E https://www.cambridge.org/core/books/primer-of-infinitesimal... this book is so so so good. It begins with nothing and eventually builds enough for Newton-style classical mechanics, made entirely of geometric arguments using infinitesimals, and being fully rigorous. Also has an appendix where it gives the construction using category theory Anyway so does this mean that Z3 can't be used to prove intuitonistic arguments? That's surprising to me. What exactly makes SMT tied to classical logic? edit: okay check out this https://dl.acm.org/doi/10.5555/1983702.1983729 https://dl.acm.org/doi/10.5555/1983702.1983729 the author used an embedding in order to represent intuitionistic formulas inside classical logic, so they could use Z3 anyway
    - philzook 2y ago
      Keep em coming! I think embedding intuitionistic logic into z3 is possible in some sense and perhaps even useful. I would a priori expect a prover built from the ground up like nanoCoP-i to deal with intuitionistic logic to be better, even if it is orders of magnitude less complex than z3. I don't think the concept of SMT is has to be tied to classical logic in some abstract sense, but the SMTlib standard is classical. And in the sense that an SMT solver is SAT solver (kind of as classical as you can get) bolted to theories. But seems reasonable to build some kind of framework bolting domain specific intuitionistic solvers to a intuitionistic fabric. See Itauto https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.9 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.I... https://gitlab.inria.fr/fbesson/itauto https://gitlab.inria.fr/fbesson/itauto which would be another interesting backend. Reusing tactics from other systems is maybe just a step too far for knuckledragger in terms of packaging and interfacing problems

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 ago
Z3 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 ago
  I agree, and it's nice to have Python bindings for it.
CoastalCoder 2y ago
How 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 ago
  I 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 ago
    Sounds 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 ago
      You 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.
      - modeless 2y ago
        But if there is a choice between breaking two soft constraints, how does it choose?
        nanolith 2y ago
        You can set weights for each soft constraint to control how easy they are to break.

0cf8612b2e1e 2y ago

I have used z3 for a job scheduling problem. I had a piece of equipment which can handle capacity X, jobs come in at known intervals and are available for given durations of varying lengths, some jobs come in multiple times, some jobs must be done above all others. Which jobs should be assigned to the equipment to maximize completed jobs while not missing the high priority entries? Numbers were such that you could only ever handle a fraction of the possible work. The throughout of a good allocation could be significantly higher than a naive one.

nextaccountic 2y ago

Nice work! So you wanted to avoid to work with epsilon-delta in the reals Question, do you use intuitionistic logic or classical logic? If you use intuitionistic logic, why not model smooth infinitesimal analysis? https://publish.uwo.ca/~jbell/invitation%20to%20SIA.pdf https://publish.uwo.ca/~jbell/invitation%20to%20SIA.pdf

philzook 2y ago
That's a an interesting suggestion! By design, I can swap out or export to nanoCoP-i https://leancop.de/nanocop-i/ https://leancop.de/nanocop-i/ , an intuitionistic prover, but I haven't had a good theory the play with. I was considering maybe an intuitionistic set theory, but this seems like a good case too.
- nextaccountic 2y ago
  Ok so I want to link A Primer of Infinitesimal Analysis https://www.cambridge.org/core/books/primer-of-infinitesimal-analysis/B0EF33F73CAF97C180897D2FD0AD1B6E https://www.cambridge.org/core/books/primer-of-infinitesimal... this book is so so so good. It begins with nothing and eventually builds enough for Newton-style classical mechanics, made entirely of geometric arguments using infinitesimals, and being fully rigorous. Also has an appendix where it gives the construction using category theory Anyway so does this mean that Z3 can't be used to prove intuitonistic arguments? That's surprising to me. What exactly makes SMT tied to classical logic? edit: okay check out this https://dl.acm.org/doi/10.5555/1983702.1983729 https://dl.acm.org/doi/10.5555/1983702.1983729 the author used an embedding in order to represent intuitionistic formulas inside classical logic, so they could use Z3 anyway
  - philzook 2y ago
    Keep em coming! I think embedding intuitionistic logic into z3 is possible in some sense and perhaps even useful. I would a priori expect a prover built from the ground up like nanoCoP-i to deal with intuitionistic logic to be better, even if it is orders of magnitude less complex than z3. I don't think the concept of SMT is has to be tied to classical logic in some abstract sense, but the SMTlib standard is classical. And in the sense that an SMT solver is SAT solver (kind of as classical as you can get) bolted to theories. But seems reasonable to build some kind of framework bolting domain specific intuitionistic solvers to a intuitionistic fabric. See Itauto https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.9 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.I... https://gitlab.inria.fr/fbesson/itauto https://gitlab.inria.fr/fbesson/itauto which would be another interesting backend. Reusing tactics from other systems is maybe just a step too far for knuckledragger in terms of packaging and interfacing problems