On a related note, anyone have any advice for getting started with something like Z3?
Accidentally writing a SAT solver
11–20 of 41 posts
Re: Accidentally writing a SAT solver
#12[stub for offtopicness]
sorry this is not fast
Re: Accidentally writing a SAT solver
#13> As a result, in order to determine if a formula is satisfiable, first convert it to conjunctive normal form, then convert the new formula into a course catalog.
I know this is a consequence of NP-completeness and so on and so forth, but I also find it a funny and charming way to phrase it. Once we've solved the fundamental problem (what courses to take), we're able to solve simple specializations and derivatives (boolean satisfiability).
Re: Accidentally writing a SAT solver
#14Interesting post, but I’m not sure this really speaks to what goes into actually writing what would be considered a “fast” SAT solver. It seems more like a post about how SAT pops up in a lot of places if you look at them right. For the state of the art in what constitutes fast solvers, the annual SAT competition papers are quite interesting to read if you’re interested in the techniques people come up with to make t…
One would assume there are some low-hanging fruits that make up the bulk of the speed-ups, but maybe it’s really a huge pile of small incremental improvements?
Re: Accidentally writing a SAT solver
#15Interesting post, but I’m not sure this really speaks to what goes into actually writing what would be considered a “fast” SAT solver. It seems more like a post about how SAT pops up in a lot of places if you look at them right. For the state of the art in what constitutes fast solvers, the annual SAT competition papers are quite interesting to read if you’re interested in the techniques people come up with to make t…
SAT turns up everywhere because it's almost universal kind of problem. Since it is NP complete, everything in NP can be transformed into an instance of SAT. Since P is a subset of NP, everything in P can be also be turned into an instance of SAT. Nobody knows if things in PSPACE can be, though.
> Since P is a subset of NP, everything in P can be also be turned into an instance of SAT.
This statement is kind of trivial. The same is true for any language (other than the empty language and the language containing all strings). The reduction is (1) hardcode the values of one string, y, that is in the language and another string, z, that is not in the language (2) solve the problem on the given input x in polynomial time poly(x) (3) return y if x is to be accepted and z otherwise.
The total running time is at most poly(x)+O(|y|+|z|) which is still poly(x) since |y| and |z| are hardcoded constant values.
Re: Accidentally writing a SAT solver
#16On a related note, anyone have any advice for getting started with something like Z3?
It really helps to have a hard problem to solve in the first place. Try scheduling all the classes in a university timetable into available classrooms, subject to constraints like maximum seating and not double booking an instructor. Now try to add constraints like “art classes must be in a studio.” Then to make it really fun, “no more than one fourth of the Electrical Engineering classes may be taught outside of the EE building.”
Re: Accidentally writing a SAT solver
#17On a related note, anyone have any advice for getting started with something like Z3?
I find both z3 native syntax (smt 2, lispish) and z3py hard to use.
Here's an alternative syntax that uses python3 types. Works by transpiling to smt 2.
https://gist.github.com/adsharma/45fbb065a8fe793030e8360daeb...
https://github.com/py2many/py2many/blob/main/tests/cases/dem...
Re: Accidentally writing a SAT solver
#18On a related note, anyone have any advice for getting started with something like Z3?
I wish I had something to offer, but I think there is little available but grit. The solvers are magical in what they can do, but structuring a problem into the DSL is an exercise in pain. Seemingly few available public examples of patterns you can crib.
Re: Accidentally writing a SAT solver
#19On a related note, anyone have any advice for getting started with something like Z3?
I wish I had something to offer, but I think there is little available but grit. The solvers are magical in what they can do, but structuring a problem into the DSL is an exercise in pain. Seemingly few available public examples of patterns you can crib.
[deleted]
Re: Accidentally writing a SAT solver
#20On a related note, anyone have any advice for getting started with something like Z3?
For constraint programming solvers, you need to define a model (i.e. what are the variables that the solver can change). Typically, a good model naturally enforces hard constraints. For instance, consider the employee scheduling problem, where you have a list of shifts that need to be assigned a single employee. Two possible models for it are:
- Use a boolean variable that is true if and only if a particular employee is assigned to a particular shift. For 2 shifts (A, B) and 2 employees (Amy, Beth), the variables would be Amy_A, Amy_B, Beth_A, Beth_B
- Use an int variable, where each employee is mapped to a number. For 2 shifts (A, B) and 3 employees (Amy, Beth, Carl), the variables would be A, B (which will have value 0 for Amy, 1 for Beth, 2 for Carl).
Using an int variable is usually better, since it automatically encodes the "each shift must have exactly one employee constraint" which would otherwise need to be added. That being said, sometimes the boolean model is used so a SAT solver can be used instead of a Integer Linear Programming Solver.
Typically, for theorem based solvers (such as Z3 or OR Tools), you add a group of similar constraints in a loop where you iterate through relevant variables. For instance, to add constraints for overlapping shifts, you would have a directory mapping each shift to the shifts its overlaps, and add a not equals constraint for each pair (since if they are equal, they have the same employee, and employees usually are unable to be at two places at the same time).
for shift in shift_vars:
for overlapping_shift in overlapping_shifts[shift]:
solver.add(shift != overlapping_shift)
@planning_entity
@dataclass
class Shift:
employee: Annotated[Employee, PlanningVariable]
start: datetime
end: datetime
def overlaps(self, other: 'Shift') -> bool:
return self.start