Encoding The Lexicographic Ordering Constraint in Satisfiability Modulo Theories

In this thesis we present nine different SMT encodings for the Lexicographic Ordering Constraint Lex, These constraints are helpful in breaking some kinds of symmetries in decision problems. The encodings are drawn from the constraint solving literature or is a variant of such. This thesis aims to serve as a single source for all known to date encodings for the lexicographic ordering constraint.

For the purpose of benchmarking, the encodings are translated into an SMT suitable form. We have done this using two methods, the first is by directly translating the encodings into SMT using C# code. The second starts by rewriting the encodings in MiniZinc language, flattening them into FlatZinc instances, then using a tool called fzn2smt to translate them to SMT. We evaluated the encodings on a suite of instances of the Social Golfer problem and the Balanced Incomplete Block Design problem, both are well known for their highly symmetric models. We tried to run inference capability tests using unsatisfiable instances of Lex between two long vectors, also by trying to find all solutions for instances of the BIBD problem. We used the SMT solvers Yices2 and Z3 to benchmark the encodings.

Our results show that what we called the Recursive OR encoding performed better than all the other encoding on most of the instances, but it was notably worse on other instances. This behaviour is roughly shared by some of the other encodings, it shows that different encodings perform differently on different problems. The results also show that, in many cases, not having any symmetry braking using either of the nine encodings performed surprisingly better