|Home | MXG | MXG Examples and Instances | MXC|
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:
Current Project Team
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
Partial List of Talks