4 ms·

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.