Systems and methods for solving unrestricted incremental constraint problems
AssigneeQUALCOMM Incorporated
InventorsJames Ezick, Thomas Henretty, Chanseok Oh, Jonathan Springer
Life of this patent
Estimating the term…
Abstract
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.
Claims21
A processor-implemented method for controlling an ensemble of a plurality of processor-implemented solvers, the method comprising performing by a controller the steps of:
- receiving, from a user, an instruction indicating invalidation or removal of one or more original clauses from a set of original clauses defining a first problem to be solved by the ensemble of the plurality of processor-implemented solvers, wherein a modified set of original clauses, derived by the invalidation or removal of the one or more original clauses, defines a second, different problem to be solved by the ensemble;
- generating, by a controller, a master graph comprising an aggregation of local graphs, each local graph being separate from other local graphs and corresponding to one of the plurality of solvers by:
- creating a first vertex corresponding to a first clause, and associating the first vertex with a first solver of the plurality of solvers;
- adding a second vertex corresponding to a second clause, and associating the second vertex with the first solver;
- and
- establishing an undo edge from the second vertex to the first vertex;
- identifying, by the controller, using the second vertex and the undo edge, a vertex corresponding to a clause to be restored;
- and
- transmitting, by the controller, a command to the first solver comprising a signal to restore the clause to be restored.
A processor-implemented method for controlling an ensemble of a plurality of processor-implemented solvers, the method comprising performing by a controller the steps of:
- receiving, from a user, an instruction indicating invalidation or removal of one or more original clauses from a set of original clauses defining a first problem to be solved by the ensemble, wherein a modified set of original clauses, derived by the invalidation or removal of the one or more original clauses, defines a second, different problem to be solved by the ensemble;
- pruning, by the controller, a master graph comprising an aggregation of local graphs, each local graph being separate from other local graphs and corresponding to one of the plurality of solvers, the master graph including:
- a plurality of original vertices, each original vertex corresponding to a respective original clause;
- and
- a plurality of vertex groups, each vertex group being associated with a respective solver from the plurality of solvers;
- generating, by the controller, a plurality of pruning messages, each pruning message corresponding to a respective one of the plurality of solvers;
- and
- transmitting, by the controller, to each one of the plurality of solvers, the corresponding pruning message.
Dependencies are inferred from the claim text.