xor_ for more than 2 parameters

[dreinon]

Hello! I would like to add a couple of constraints for my tasks to be scheduled between two points. I'm using the following sintax: for j in availability: av_list.append(ps.and_([ps.TaskStartAfterLax(students_tasks[-1], j[0]), ps.TaskEndBeforeLax(students_tasks[-1], j[1])])) But then, only one of those and constraints will be applied. I'm using or operator like this: `constraints.append(ps.or(av_list))` But the solver takes forever and doesn't find a solution.

Since I lastly had another logic problem and this problem made the solver take forever, I'm thinking this way of acting migth be product of a logic error here too.

Since only one of those and statements have to be true, I'm thinking that the correct operator to use to group all the and statements would be xor_, but I tried and got an error saying that xor can only be used with two constraints.

Any help with this, please? Thanks in advance!

[tpaviot]

This is an interesting issue. The Xor z3 operator takes only two parameters, that's why the xor_ ProcessScheduler operator takes 2 parameters as well. Expressing Xor(a,b,c) is quite easy to understand (one and one of the three booleans a, b, c, is True, the other are False), but difficult to express in of boolean operations. I see two solutions:

• develop the expression Xor(a, b, c) so that built-in functions or_, xor_, and_ can be used. See https://math.stackexchange.com/questions/2480640/boolean-expression-of-3-input-xor-gate

• in terms of the z3 semantics, your problem is a PbEq constraint: in a list of n statements, only 1 can be True. What I could do is to create an optional constrain that may or may not apply under certain conditions. It's a bit more work.

[dreinon]

Thanks for answering!

What I think we could do is to make both if you liked.

I will work today in making a xor method for multiple arguments, which I'll share when I get it done, but it would also be nice if you could write that function in terms of z3. I think it makes more sense to use that since all constraints are made in terms of z3 too.

Thank you Thomas!

[dreinon]

Hi Thomas, I have looked into the first option, and apparently, there's no way to implement that one and only one constraint of a list of constraints is true, since apparently a chain of xors A_1 xor A_2 xor ... xor A_n is true whenever an uneven number of variables are true, and false whenever an even number of vairables are true.

[tpaviot]

Thank you for the feedback. I do think there's no other way than adding an optional flag to a constraint so that it is possible to define optional constraints. After that, it is possible to do anything with these optional constraints (conditional constraint, one among many, etc.), exactly the same that I already did for the optional tasks.

[tpaviot]

BTW, can you access the dev branch using git? If I need you to test something, it would be easier

[dreinon]

Yes, I have forked the master branch to add the new unit test, is that fine? Also kind of new to git haha

[tpaviot]

Perfect for the unit tests, thank you. The more unit tests bound the library, the better.

I've been working on the OptionalConstraint issue, I pushed a related branch to the repo

[tpaviot]

Using the code under branch_name optional_constraint, here is how you can formulate your problem:

# build the av_list using an optional flag set to True
# then force to apply only one of these constrainst:
cstr = ps.ForceApplyNOptionalConstraints(av_list, 1)

This is equivalent to a xor for a list.

[dreinon]

Awesome!!! Let me try it out! Thanks Thomas

[dreinon]

Working like charm!