SAT: Some Constraints

In this post, I present four constraints that I have implemented for my satisfiability package SugarRush. It is based on PySAT [1]. 

Parity

This constraint is much much better to use than the method used in sat: disjunction operator. 

Naive / general way, with disjunction (for 10 elements):

Nof variables: 1096

Nof clauses: 3195

Special purpose encoding of parity constraint (for 10 elements):

Nof variables: 19

Nof clauses: 36

And of course it solves much faster.

Less / Leq

A natural question is: why is the t returned separately from the rest of the constraint? The reason is that this way, one can easily encode such constraints as "a is either less than b, or less than c", or "a is less than either b or c, but not both". An example usage here is to constrain two intervals to be non-overlapping:

Plus

Element

[1] Ignatiev, Alexey, Antonio Morgado, and Joao Marques-Silva. "PySAT: A Python toolkit for prototyping with SAT oracles." International Conference on Theory and Applications of Satisfiability Testing. Springer, Cham, 2018.