Constraint Satisfaction

The Constraint Satisfaction team focuses on research and development in the area of constraint satisfaction problems (CSPs). Our main asset is the constraint solver, a robust, general-purpose, state-of-the-art tool that has been used for more than a decade in modeling and solving many complex constraint problems.  The solver comprises three powerful search engines:

• GEC, a deterministic engine that performs systematic search with backtracking through arc consistent states.
• Stocs, a stochastic local search engine that relies on learning the high level parameters of the problem characteristics and uses a non-local escape algorithm.
• Mage, a powerful SAT solver that is developed by the Formal Verification team and that incorporates state-of-the-art algorithms such as two-literal watches and conflict analysis.

We have recently begun cooperation with ILOG's CP Optimizer's team.

The constraint solver is adept at handling:

• Up to hundreds of thousands of variables and constraints
• Variables with very large domains, including powerful representation and operations on those domains
• Conditional CSP with early conditional pruning
• Optimization by definition of a hierarchy of soft constraints (Borning Hierarchy), as well as by setting objective functions

Constraint applications

The constraint solver serves as the internal engine for IBM test generation tools for hardware verification, including GenesysPro, X-Gen, FPgen, and CacheLoader.  As such, it is the technological base for verification of virtually all IBM high-end  processors and systems:

• IBM iSeries, pSeries, and zSeries servers
• IBM Cell processor

Using our constraint solver, IBM’s hardware verification tools have reduced design and verification costs by more than $100M. External companies that licensed the test generator tools noted the powerful CSP engine capabilities as a key factor in the decision to license  the tools.

IBM has also used the constraint solver to model and solve complex problems in a variety of other fields. These include:

• Vehicle configuration.
• Workforce management.
• Floorplanning.
• Job scheduler and allocator for massively parallel processors.

Our department has long-standing expertise in CSP algorithms and modeling. Our aim is to provide value to IBM through the application of constraint solving to various domains and close interaction with the academic community. We work closely with our with IBM partners to find the best constraint or optimization model for their domain, and apply the best heuristics when solving this model.