Extreme SAT-based Constraint Solving with R-Solve

We present the architecture of R-Solve, a highperformance constraint solver 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 brings together a modern, open SAT solver, HPC ideas in ensemble and collaborative parallel solving and a novel set of extensions supporting, for the first time, an efficient system for unrestricted incremental solving.

Publications

For more information about Reservoir products or to purchase, please