Skip to main content

Constraint Satisfaction (Octopus)

Stocs

Stocs is a stochastic constraint solver that implements Simulated Variable-Range Hopping (SVRH) as its basic algorithm. It performs extended neighborhood search, where the size of the neighborhood and other parameters of the problem's topography are learned dynamically. Stocs is a fully modular, constraint-based, stochastic local search solver, meaning that different types of constraints and solution strategies can be defined and added by the user on the fly. In addition, Stocs supports SIL (which stands for Stocs Input Language) as its textual input language. SIL supports the definition of constraints through expressions, including logical, arithmetic, set, and bitwise expressions. Stocs is used in production by FP-Gen, ACS (see link to stimuli generators, below), and the Vehicle Configuration project.

Contact: Yehuda Naveh (naveh@il.ibm.com)

Optimatch

Optimatch, developed jointly with the Mathematical Sciences department at Watson, provides a scheduling tool to assign highly-skilled employees to high-end jobs within large organizations. Given the constantly increasing number of such jobs and stringent business requirements, decisions must be made quickly, optimally, and in a dynamic environment. Our tool is based on the novel Constraint Programming (CP) technology. This technology allows much more flexibility in defining workforce-related constraints than traditional OR methods. It also provides strong pruning abilities, which imply a much faster search for a satisfying solution.

Contact: Yossi Richter (richter@il.ibm.com)

Circuit Design

Together with the Haifa Development Lab, we develop a tool that will be able to place and route up to 800 instances of custom designed macros. The tool sets pin placement, macro placement, and wire routing, using CP techniques and specialized CSP solving algorithms. The DCCD tool considers wire length limitation (implied by timing constraints and the given technology), wire route constraints, no overlap rules, bus continuity constraints, and more.

Contact: Michael Veksler (Veksler@il.ibm.com)

Stimuli Generation for Hardware Verification

This is the main activity of the Verification and Analytics department. The department develops a wide range of tools for stimuli generation for functional verification of high-end hardware designs. All tools are based on CSP technology. Essentially, each tool models the hardware verification problem as a set of constraints over variables describing the hardware, and then uses GEC and/or Stocs to solve the resulting CSP. Constraints in this domain come from the hardware specification, user requirements, and expert knowledge. For more information see: http://www.haifa.il.ibm.com/projects/verification/octopus/csp.html

Contact: Yehuda Naveh (naveh@il.ibm.com)