SYSTEMS AND METHODS FOR SOLVING UNRESTRICTED INCREMENTAL CONSTRAINT PROBLEMS

摘要

We present the architecture of a high-performance constraint solver R-Solve that extends the gains made in SAT performance over the past fifteen years on static decision problems to problems that require on-the-fly adaptation, solution space exploration and optimization. R-Solve facilitates collaborative parallel solving and provides an efficient system for unrestricted incremental solving via Smart Repair. R-Solve can address problems in dynamic planning and constrained optimization involving complex logical and arithmetic constraints.