R-Solve™

Learn more about our powerful automated reasoning technology »

Systems and Methods for Solving Unrestricted Incremental Constraint Problems



Publication Source: Patent US10402747B2

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.
Google Scholar    Article

System And Method for Configuration of an Ensemble Solver



Publication Source: Patent US9684865B1

In a system for enabling configuration of an ensemble of several solvers, such that the ensemble can efficiently solve a constraint problem, for each one of several candidate configurations, an array of scores is computed. The array corresponds to a statistical parameter related to a problem solution, and the computation is based on, at least in part, a set of features associated with the problem. One candidate configuration is assigned to a solver, and based on the array of scores associated with that candidate configuration the same or a different candidate configuration is assigned to a another solver. A system for dynamically reconfiguring an ensemble of solvers obtains runtime data from several solvers, and a new configuration is determined by applying a machine learning and/or heuristic analysis procedure to the runtime data. The configuration of a solver may be updated according to the new configuration while that solver is running.
Google Scholar    Article

Systems and Methods for Planning a Solution to a Dynamically Changing Problem



Publication Source: Patent US8892483B1

A plan representing a final solution to a problem is obtained efficiently, if the problem changes while being solved, by identifying the solution elements not affected by the change, and by reusing those solution elements.
Google Scholar    Article

Extreme SAT-based Constraint Solving with R-Solve



Publication Source: The IEEE Conference on High Performance Extreme Computing (HPEC), Waltham, MA, USA, IEEE, September, 2014

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.
Google Scholar    Article

Systems, Methods, and Apparatus for Distributed Decision Processing



Publication Source: Patent US8688619B1

Methods, apparatus, and computer software product for making a decision based on the semantics of formal logic are provided. In an exemplary embodiment, two custom computing apparatuses are used to resolve the satisfiability of a logical formula and provide an example. In this embodiment, the two custom computing apparatuses operate in concert to explore the space of possible satisfying examples. This Abstract is provided for the sole purpose of complying with the Abstract requirement rules. This Abstract is submitted with the explicit understanding that it will not be used to interpret or to limit the scope or the meaning of the claims.
Google Scholar    Article

1 2