Opturion CPX -- MiniZinc Challenge 2015 ======================================= Opturion CPX is a constraint solver for discrete optimisation or satisfaction problems developed by Opturion Pty Ltd. It is based on the CPX solver originally developed as part of the G12 project at NICTA. Opturion CPX uses the lazy clause generation technique, which combines both CP and SAT solving techniques. By using this approach CPX can provide state of the art solutions to a number of hard combinatorial problems. Like CP, CPX allows a problem to be mapped to a compact representation, rather than generating a SAT representation (which can become huge, especially when dealing with integer variables and constraints). Like SAT, it learns from failure and can automatically focus the search on the ``bottlenecks'' of a problem. An important feature of CPX is that it only generates propositional variables needed for search, so large variable domains do not necessarily slow down the search or proof of optimality. CPX's default search selects variables according to a combination of domain size and activity count. It bisects the domain of the selected variables. The default search uses failure based Luby-style restarts. For optimization problems, the default search is preceded by a probing phase in which random probes of the search tree are used to initialise the variable activity counts. For further information, see the Opturion CPX webpage at .