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.
1. A method for controlling an ensemble of a plurality of solvers, the method comprising performing by a master controller, distinct from each of the plurality of solvers, 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; and
for solving the second problem:
pruning a master graph at the master controller, the master graph comprising:
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 one or more non-original clauses that are learned and received from a respective solver from the plurality of solvers;
generating by the master controller a plurality of pruning messages derived from the one or more invalidated or removed original clauses, each pruning message being solver-specific and corresponding to a respective one of the plurality of solvers, comprising one or more learned clauses, and informing the respective solver to invalidate or remove the one or more learned clauses; and
transmitting by the master controller to each one of the plurality of solvers, the corresponding solver-specific pruning message.
2. The method of claim 1 , wherein each vertex group comprises:
a plurality of non-original vertices, each non-original vertex: (i) corresponding to a respective clause learned by a solver associated with the vertex group, and (ii) being reachable from at least one of the original vertices.
3. The method of claim 2 , wherein pruning the master graph comprises:
selecting one or more invalidated or removed original clauses;
identifying one or more original vertices corresponding to the selected one or more original clauses;
within each vertex group:
marking all non-original vertices that are reachable from the one or more identified original vertices;
collecting identifiers of learned clauses corresponding to the marked non-original vertices; and
removing the marked non-original vertices.
4. The method of claim 3 , wherein generating a pruning message corresponding to a particular solver comprises:
selecting the vertex group corresponding to the particular solver; and
listing in the pruning message the collected identifiers of the learned clauses as identifiers of clauses to be removed.
5. The method of claim 4 , wherein a particular vertex group comprises an undo edge originating from a first non-original vertex, and the method further comprises:
identifying a destination vertex that is reachable via the undo edge and that is not marked; and
listing in the pruning message a learned clause associated with the destination vertex as a clause to be restored.
6. The method of claim 5 , wherein:
the undo edge originating from the first non-original vertex terminates at a second vertex; and
the destination vertex comprises the second vertex.
7. The method of claim 5 , wherein:
the undo edge originating from the first non-original vertex terminates at a second vertex;
another undo edge originating from the second vertex terminates at a third vertex; and
the destination vertex is reachable from the third vertex.
8. The method of claim 3 , wherein selecting the one or more original clauses comprises a random selection.
9. The method of claim 3 , wherein selecting the one or more original clauses comprises a score-based selection, the method further comprising:
computing a score for each original clause using at least one of: number of literals in the clause, and number of vertices reachable from a vertex corresponding to the original clause.
10. The method of claim 1 , further comprising, prior to transmitting the pruning messages, determining that the ensemble has stopped, wherein the pruning message corresponding to each solver is transmitted prior to restart of the ensemble.
11. The method of claim 1 , wherein the controller is separate from each one of the plurality of solvers.
12. A system for controlling an ensemble of a plurality of solvers, the system comprising:
a first processor; and
a first memory in electrical communication with the first processor, the first memory comprising instructions which, when executed by a processing unit comprising at least one of the first processor and a second processor, and in electronic communication with a memory module comprising at least one of the first memory and a second memory, program the processing unit as a master controller, distinct from each of the plurality of solvers, to:
receive 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; and
to solve the second problem:
prune a master graph at the master controller, the master graph comprising:
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 one or more non-original clauses that are learned and received from a respective solver from the plurality of solvers;
generate by the master controller a plurality of pruning messages derived from the one or more invalidated or removed original clauses, each pruning message being solver specific and corresponding to a respective one of the plurality of solvers, comprising one or more learned clauses, and informing the respective solver to invalidate or remove the one or more learned clauses; and
transmit by the master controller to each one of the plurality of solvers, the corresponding solver-specific pruning message.
13. The system of claim 12 , wherein each vertex group comprises:
a plurality of non-original vertices, each non-original vertex: (i) corresponding to a respective clause learned by a solver associated with the vertex group, and (ii) being reachable from at least one of the original vertices.
14. The system of claim 13 , wherein to prune the master graph the controller is programmed to:
select one or more invalidated or removed original clauses;
identify one or more original vertices corresponding to the selected one or more original clauses;
within each vertex group:
mark all non-original vertices that are reachable from the one or more identified original vertices;
collect identifiers of learned clauses corresponding to the marked non-original vertices; and
remove the marked non-original vertices.
15. The system of claim 14 , wherein to generate a pruning message corresponding to a particular solver the controller is programmed to:
select the vertex group corresponding to the particular solver; and
list in the pruning message the collected identifiers of the learned clauses as identifiers of clauses to be removed.
16. The system of claim 15 , wherein:
a particular vertex group comprises an undo edge originating from a first non-original vertex; and
the controller is further programmed to:
identify a destination vertex that is reachable via the undo edge and that is not marked; and
list in the pruning message a learned clause associated with the destination vertex as a clause to be restored.
17. The system of claim 16 , wherein:
the undo edge originating from the first non-original vertex terminates at a second vertex; and
the destination vertex comprises the second vertex.
18. The system of claim 17 , wherein:
the undo edge originating from the first non-original vertex terminates at a second vertex;
another undo edge originating from the second vertex terminates at a third vertex; and
the destination vertex is reachable from the third vertex.
19. The system of claim 14 , wherein to select the one or more original clauses the controller is programmed to perform a random selection.
20. The system of claim 14 , wherein to select the one or more original clauses the controller is programmed to compute a score for each original clause using at least one of:
number of literals in the clause, and number of vertices reachable from a vertex corresponding to the original clause, to perform a score-based selection.
21. The system of claim 12 , wherein the controller is further programmed to, prior to transmitting the pruning messages:
determine that the ensemble has stopped; and
transmit the pruning message corresponding to each solver prior to restart of the ensemble.
22. The system of claim 12 , further comprising the plurality of solvers, wherein the controller is separate from each one of the plurality of solvers.