Constraint Solver
Overview
Our constraint solver consists of three components: GEC, a systematic solver; Stocs, a stochastic local search solver, and Mage, a SAT solver.
GEC is a systematic, MAC-based solver. It has strong support for operations on large number domains, for conditional variables, and for a hierarchy of soft constraints, in addition to the problem's hard constraints.
Stocs is a local-search solver based on the Simulated Variable-Range Hopping algorithm. It incorporates dynamic learning of the problem domain into the solving process.
Mage is a SAT solver based on modern ideas such as two-literal watches and conflict analysis, and implements a set of powerful heuristics. It is especially suitable for large, real world (non-random) problems. Mage is developed by HRL's Formal Verification group.
One of the major strengths of our team is the combination of the three complementary types of solvers that we have at our disposal. We also cooperate with the ILOG team, and have experience using CPLEX and CP Optimizer. Determining which approach to take when trying to solve a new problem is a significant challenge. Our team has accumulated significant experience and knowledge while modeling a large variety of problems and through experimenting with all three approaches. For many problems, a combined, or 'hybrid' approach proves to be the most suitable. More background information is available on the general benefits and drawbacks of each of the approaches.
In addition to our solver, we develop ClassMate, a modern object-based, constraint based, ontology modeling platform. ClassMate is particularly valuable in cases where the problem domain is rich and complex. In such cases it allows a rapid development of a domain-specific modeling language (using ClassMate's meta-language constructs), which in turn allows for a fast and accurate modeling of the user's problem.
Contact: Wesam Ibraheem (wesam@il.ibm.com)