is it though? You can't express some basic loop in propositional logic, right?
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.
But getting a really fast solver requires multiple strategies that don't work well together (so they have to work semi-independently). This leads to other problems related to managing shared resources like how much you should let different strategies cache information at the expense of how much other strategies can cache information. Tuning all of these trade-offs is exceedingly difficult to do well since it depends a lot on the types of problems that you need to solve.
This is an annual battle I engage in. The software sucks.
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...
https://github.com/Z3Prover/z3/blob/master/examples/dotnet/P...
The examples are in C#, but easy to adapt to other languages. I found them quite useful to write a program for symbolic execution in F# that calls Z3 to simplify conditionals, here is its interface to Z3:
https://github.com/constructum/asm-symbolic-execution/blob/m...
The bindings are perhaps a bit cumbersome, but rather easy to understand and work very well. Once you appropriately wrap what you need, you can forget about the bindings as well as avoiding SMT-LIB completely.
- 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 < other.end and other.start < self.end
def no_overlapping_shifts(constraint_factory: ConstraintFactory):
return (constraint_factory.for_each(Shift)
.join(Shift,
Joiners.equal(lambda shift: shift.employee))
.filter(lambda a, b: a.overlaps(b))
.penalize(HardSoftScore.ONE_HARD)
.as_constraint('Overlapping Shift'))
On the other hand, I remember for my acceptance (which wasn't too the ECE program) I had to pick classes before I could confirm going to UMD? I don't remember why but I remember panicking because here I am, a high schooler still, picking college classes that would set my next 4 years. I was even more terrified when my first ever class not only was I late because it was in the back of a basement, but the instructor made some comment about it not being the right class for engineers or something. It was, though. You fix this and other problems: 1. I started using the UMD provided schedule planner and some 3rd party ones, with multiple backups for when they'd fill up 2. I made an app that showed most buildings' floor plans completely offline. No more wandering around during stressful times. 3. I did try and make a tree of classes using prerequisite days scraped from the SoC, but it wasn't a regular expression so I gave up immediately.
The blogger like CMSC430 and I agree it was a good class though I had a different professor.
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).
I made a repo many years ago with a bunch of grab bag solutions for comparisons [1]; from dumb brute force to DLX (Knuth's Dancing Links) and a multithreaded bitwise backtracking algorithm. And one where I just hardcoded the answers because all the counts up to 27 are known.
So I'm all for just jumping to the existing known solutions, but it seems like the OP is having fun while they learn a little bit. They seem to just be a college freshman.