White Rose University Consortium logo
University of Leeds logo University of Sheffield logo York University logo

Encoding The Lexicographic Ordering Constraint in Satisfiability Modulo Theories

Elgabou, Hani (2015) Encoding The Lexicographic Ordering Constraint in Satisfiability Modulo Theories. MSc by research thesis, University of York.

[img]
Preview
Text (MSc Thesis)
Encoding The Lexicographic Ordering Constraint in Satisfiability Modulo Theories.pdf
Available under License Creative Commons Attribution-Noncommercial-No Derivative Works 2.0 UK: England & Wales.

Download (491Kb) | Preview

Abstract

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

Item Type: Thesis (MSc by research)
Academic Units: The University of York > Computer Science (York)
Depositing User: mr Hani Elgabou
Date Deposited: 12 Oct 2015 12:26
Last Modified: 12 Oct 2015 12:26
URI: http://etheses.whiterose.ac.uk/id/eprint/10387

You do not need to contact us to get a copy of this thesis. Please use the 'Download' link(s) above to get a copy.
You can contact us about this thesis. If you need to make a general enquiry, please see the Contact us page.

Actions (repository staff only: login required)