Systems and methods for solving unrestricted incremental constraint problems

Patent metadata

Field	Value
Publication number	US-11899740-B2
Application number	US-202017113814-A
Country	US
Kind code	B2
Filing date	Dec 7, 2020
Priority date	Jun 3, 2014
Publication date	Feb 13, 2024
Grant date	Feb 13, 2024

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.

First claim

Accordingly, we claim:

1. 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.

2. The method of claim 1 , wherein the command further comprises a signal to invalidate the second clause.

3. The method of claim 1 , wherein the controller transmits the command while the first solver is running.

4. The method of claim 1 , wherein the controller transmits the command when the first solver has stopped running, before the first solver starts running again.

5. The method of claim 1 , wherein:
the vertex corresponding to the clause to be restored comprises the first vertex; and
the clause to be restored comprises the first clause.

6. The method of claim 1 , wherein the second clause is a dummy clause, the method further comprising:
receiving from the first solver, prior to adding the second vertex, a message describing: (i) that the first solver identified a third clause, (ii) a relationship between the first clause and the third clause, and (ii) that the first solver removed the first clause from a data structure maintained by the first solver;
adding a third vertex corresponding to the third clause, and associating the third vertex with the first solver; and
forming a successor edge from the third vertex to the second vertex.

7. The method of claim 1 , wherein:
identifying the vertex corresponding to the clause to be restored comprises:
(i) identifying, using the undo edge, the first vertex; and
(ii) identifying, using an undo edge from the first vertex, a fourth vertex that corresponds to a fourth clause and is associated with the first solver; and

the clause to be restored comprises the fourth clause.

8. The method of claim 1 , further comprising:
receiving from the first solver, prior to adding the second vertex, a first message:
(i) describing that the first solver at least in part learned the second clause from the first clause and removed the first clause from a data structure maintained by the first solver; and
(ii) identifying a first unique identifier associating the second clause described in the first message with the first solver; and

forming a successor edge from the first vertex to the second vertex.

9. The method of claim 1 , wherein the controller is separate from each one of the plurality of solvers.

10. The method of claim 1 , in which the transmitting is triggered by the identifying of the vertex corresponding to the clause to be restored.

11. 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.

12. The method of claim 11 , 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.

13. The method of claim 12 , wherein pruning the master graph comprises:
selecting one or more 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.

14. The method of claim 13 , 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.

15. The method of claim 14 , 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.

16. The method of claim 15 , wherein:
the undo edge originating from the first non-original vertex terminates at a second vertex; and
the destination vertex comprises the second vertex.

17. The method of claim 15 , 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.

18. The method of claim 13 , wherein selecting the one or more original clauses comprises a random selection.

19. The method of claim 13 , 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.

20. The method of claim 11 , further comprising, prior to transmitting the pruning messages, determining that the ensemble has stopped, w

Assignees

• Qualcomm Inc

Inventors

• Ezick James
• Henretty Thomas
• Oh Chanseok
• Springer Jonathan

Classifications

• G06F17/11 Primary

  for solving equations {, e.g. nonlinear equations, general mathematical optimization problems (optimization specially adapted for a specific administrative, business or logistic context G06Q10/04)} · CPC title

• G06F9/54

  Interprogram communication · CPC title

• G06N5/022

  Knowledge engineering; Knowledge acquisition · CPC title

• G06N7/00

  Computing arrangements based on specific mathematical models · CPC title

• G06N7/01

  Probabilistic graphical models, e.g. probabilistic networks · CPC title