The MX Project
Modelling and Solving Search Problems with Logic
Home | MXG | MXG Examples and Instances | MXC
Recent News
  • Article in Faculty Newsletter [November 18 2008]
  • Internships: We have Undergrad Research Assistant and Programmer positions available. Part-time or as a co-op term are possible. Contact David Mitchell or Eugenia Ternovska by email.
  • Internships: Graduate Student and Post-Doctoral MITACS internships are available, from 4 to 8 months duration, to work on several parts of the project.
Project Overview

The main goals of the MX project are to develop theoretical foundations for languages and systems for modelling and solving combinatorial search and optimization problems, and to build and demonstrate practical systems based on these foundations.

Computationally hard search and optimization problems are ubiquitous in science, engineering and business. Examples include drug design, protein folding, phylogeny reconstruction, hardware and software design, test generation and verification, planning, timetabling, scheduling and on and on. In rare cases, practical application-specific software exists, but most often development of successful methods requires hiring specialists, and often significant time and expense, to apply one or more computational approaches. Typical examples are mathematical programming (i.e., integer-linear programming, ILP), constraint logic programming (CLP), and development of custom-refined implementations of methods such as simulated annealing, branch-and-bound, reduction to SAT, etc.

One goal of the MX project is to provide another practical technology for solving these problems, but one which would require considerably less specialized expertise on the part of the user, thus making technology for solving such problems accessible to a wider variety of users. In this approach, the user gives a precise specification of their search (or optimization) problem in a declarative modelling language. A solver then takes this specification, together with an instance of the problem, and produces a solution to the problem (if there is one).

Other languages and systems are in development with roughly similar goals and approach (e.g., Essence, Answer Set Programming). The MX project is distinguished by being based on a theoretical foundation in mathematical logic - in particular descriptive complexity theory - and by the project philosophy that practical tools should be build on top of sound theoretical foundations, and formal tools developed based on practical needs.

In our approach, search problems are formalized as model expansion, which is the logical task of expanding a given structure by new relations. Formally, the user is axiomatizing their problem, formalized as model expansion, in some extension of classical logic. In an applied setting, the actual language the user works with may be different syntactically from, though equivalent to, such a logic. For example, a language tailored to mainstream IT workers could be an extension of SQL.

By choosing the logic involved, the framework can be parameterized to capture various complexity classes, including NP. Second-order quantifiers can be used to concisely model problems at higher complexity levels. First-order quantifiers can be used freely for modelling convenience, without affecting the complexity level which is determined by the second-order quantifiers. Adding inductive definitions (as in ID-logic) contributes to the convenience of knowledge representation by adding recursion and recursion through negation, but does not change the main complexity properties.

At present, our focus is on problems in the complexity class NP. For this case, the modelling language is based on classical first order logic (FO), and the default mechanism for constructing a solver is by ``grounding'': given a specification and instance, produce a formula of propositional logic that describes the solutions, and pass this to an engine that solves the propositional satisfiability problem (SAT solver). A prototype grounder/solver, called MXG, has demonstrated the feasibility of this approach for FO (with some extensions), and grounding to SAT, and also to SAT extended with cardinality constraints. (Fast SAT solvers are available off-the-shelf, and are a standard tool in, for example, electronic design and verification. For SAT+Card, we use our own solver MXC.))

In current work, we have developed a new, improved, grounder, and are actively pursuing several directions, all of which have theoretical and practical components:

  • Adding arithmetic and other constraints to our langauge
  • Extending our method and tools from search to optimization
  • Developing more effective grounding techniques
  • Developing techniques for ``partial grounding'', to exploit solvers for richer languages than SAT, such as SMT and ILP solvers.
Current Project Team
  • Faculty: Eugenia Ternovska, David Mitchell.
  • Post-Docs: Gulay Unel.
  • PhD Students: Amir Avani, Shahab Tasharrofi.
  • MSc Students: Brendan Guild, Sia Bolourani.
Alumni, Collaborators, and other Contributors
Alphabetically (and certainly with some missing): David Bregman (Undergrad RA 2005-, developer of MXC), Arvind Gupta (SFU Faculty), Faraz Hach (MSc 2007), Antonina Kolokolova (Post-Doc 2005-2007, now at Memorial), Yongmei Liu (Post-Doc 2006, now at HKUT), Toni Mancini (Visitor 2007, University of Rome, La Sapienza), Raheleh Mohebali (MSc 2007, now at Nokia), Nhan Nguyen (Undergrad RA 2006/7, now at UBC), Murray Patterson (MSc 2006), Nikolay Pelov (Post-Doc 2005, now at Mission Critical), Stella Chui (Undergrad Summer Intern 2006, from U of Toronto).
Partial List of Papers
  • Declarative programming of search problems with built-in arithmetic. Eugenia Ternovska, David G. Mitchell and Brendan Guild LaSh 2008.
  • Expressive Power and Abstraction in Essence. David G. Mitchell, Eugenia Ternovksa, Constraints, 8(3). (A preliminary version appeared as Technical Report: TR 2007-19.)
  • Model expansion and the expressiveness of FO(ID) and other logics. Antonina Kolokolova, Yongmei Liu, David G. Mitchell, and Eugenia Ternovska, SFU Computing Science Technical Report: TR 2007-29, December 2007.
  • Faster Phylogenetic Inference with MXG. David G. Mitchell, Faraz Hach, Raheleh Mohebali, LPAR-2007.
  • Grounding for Model Expansion with Inductive Definitions. Murray Patterson, Yongmei Liu, Eugenia Ternovska, Arvind Gupta, IJCAI'07.
    • A logic of non-monotone inductive definitions. Eugenia Ternovska, Marc Denecker, ACM Transactions in Computational Logic (TOCL).
  • Constraint Programming with Unrestricted Quantification. David G. Mitchell, Eugenia Ternovska, CP-05 Workshop on Quantification in Constraint Programming.
  • Reducing Inductive Definitions to Propositional Satisfiability. Nikolay Pelov, Eugenia Ternovska, ICLP-05.
  • A Framework for Solving NP-hard Search Problems. David G. Mitchell, Eugenia Ternovska, AAAI'05.
  • A logic of non-monotone inductive definitions and its modularity properties. Eugenia Ternovska, Marc Denecker, LPNMR.
Partial List of Talks
  • Declarative Programming for Search Problems with Built-in Arithmetic
  • Modelling Languages, Model Expansion and MXG
  • An MX-Based Front End for SAT
  • Talk on Complexity of MX and Related Tasks
  • Slides for invited talks at Microsoft Research and  Newton Institute, Cambridge, UK
Some Photos
Old News: