The aim of this work develop and evaluate techniques for modelling combinatorial decision and optimisation problems (such as those often modelled as finite-domain constraint satisfaction problems) in SMT.

Here are some papers on this work and some of the problem instances we used in the papers:

• Anomalies in SMT Solving: Difficulties in Modelling Combinatorial Problems.
  Alan M Frisch and Miquel Palahi. In Proc. of the Thirteenth International Workshop on Constraint Modelling and Reformulation, pages 97-110, September 2014. Problem instances for the four anomalies in the paper:     anomaly1.tar.gz     anomaly2.tar.gz     anomaly3.tar.gz     anomaly4.tar.gz
• Encoding the Lexicographic Ordering Constraint in Satisfiability Modulo Theories.
  Hani A Elgabou, MSc by Research Thesis, Department of Computer Science, University of York. May 2015.
  

• Encoding the Lexicographic Ordering Constraint in SAT Modulo Theories.
  Hani A Elgabou and Alan M Frisch. In Proc.of the Thirteenth International Workshop on Constraint Modelling and Reformulation, pages 85-96, Sept 2014.


• Feasibility of Building Better Traincrew Rosters with Complete Solvers.
  Alan M Frisch and Miquel Palahi. In Proc. of the Fourteenth International Workshop on Constraint Modelling and Reformulation, August 2015. Problem instances from the paper encoded as WSimply data files:   Instance A   Instance B   Instance C   Instance D

• Comparing SAT and SMT Encodings of the All-Different Global Cardinality Constraint.
  Charles Turner, MEng Thesis, Department of Computer Science, University of York. May 2014.

This web-page is maintained by Alan Frisch, and was last changed on 4 February 2016.