Systems and methods for solving unrestricted incremental constraint problems

1. A method for controlling an ensemble of a plurality of solvers, the method comprising performing by a controller the steps of:

receiving from each one of the plurality of solvers notifications of clauses learned by the respective solvers, and generating, using the received notifications, a master graph 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, using the second vertex and the undo edge, a vertex corresponding to a single clause that was discarded by at least one of the plurality of solvers and that is to be restored; and

transmitting a command to the first solver comprising a signal to restore the single clause, wherein, prior to receiving the command the first solver is associated with a set of clauses, and retains the set of clauses after receiving the command.

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 6 , wherein the relationship specifies one of:

the third clause subsumes the first clause;

the third clause satisfies the first clause; and

the third clause implies that if the third clause is satisfied the second clause is satisfied, wherein the third clause is not derived from the first clause.

8. The method of claim 6 , further comprising, prior to transmitting the command to the first solver:

identifying the third vertex for removal; and

in response, identifying via the successor edge, the second vertex for removal.

9. The method of claim 1 , wherein:

identifying the vertex corresponding to a 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.

10. The method of claim 9 , wherein the command further comprises a signal to invalidate the first clause.

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

12. The method of claim 11 , wherein the first clause comprises a learned clause reachable from a first original clause corresponding to a first original vertex, the method further comprising:

selecting a second original vertex corresponding to a second original clause for temporary invalidation, wherein: (i) the first clause was not derived from the second original clause, and (ii) the second clause is reachable from both the second original clause and the first clause; and

determining, prior to the transmitting step, that the second clause is invalid.

13. The method of claim 11 , wherein the first clause comprises a learned clause reachable from a first original clause corresponding to a first original vertex, the method further comprising:

receiving from a second solver of the plurality of solvers, a second message:

describing that the second solver at least in part learned: (i) a fifth clause from the first original clause, and (ii) the second clause from both the second original clause and the fifth clause, and retained the fifth clause from a data structure maintained by the second solver; and

identifying a second unique identifier associating the second clause described in the second message with the second solver;

creating a fifth vertex corresponding to the fifth clause, and associating the fifth vertex with the second solver;

adding a sixth vertex corresponding to the second clause described in the second message, and associating the sixth vertex with the second solver using the second unique identifier; and

forming a successor edge from the fifth vertex to the sixth vertex without adding an undo edge from the sixth vertex to the fifth vertex.

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

15. 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 controller to:

receive from each one of the plurality of solvers notifications of clauses learned by the respective solvers, and generate, using the received notifications, a master graph by, wherein to generate the master graph the controller is programmed to:

create a first vertex corresponding to a first clause, and associating the first vertex with a first solver of the plurality of solvers;

add a second vertex corresponding to a second clause, and associating the second vertex with the first solver; and

establish an undo edge from the second vertex to the first vertex;

identify, using the second vertex and the undo edge, a vertex corresponding to a single clause that was discarded by at least one of the plurality of solvers and that is to be restored; and

transmit a command to the first solver comprising a signal to restore the single clause, wherein, prior to receiving the command the first solver is associated with a set of clauses, and retains the set of clauses after receiving the command.

16. The system of claim 15 , wherein the command further comprises a signal to invalidate the second clause.

17. The system of claim 15 , wherein the controller is programmed to transmit the command while the first solver is running.

18. The system of claim 15 , wherein the controller is programmed to transmit the command when the first solver has stopped running, before the first solver starts running again.

19. The system of claim 15 , wherein:

the vertex corresponding to the clause to be restored comprises the first vertex; and

the clause to be restored comprises the first clause.

20. The system of claim 15 , wherein:

the second clause is a dummy clause; and

the controller is further programmed to:

receive 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;

add a third vertex corresponding to the third clause, and associating the third vertex with the first solver; and

form a successor edge from the third vertex to the second vertex.

21. The system of claim 20 , wherein the relationship specifies one of:

the third clause subsumes the first clause;

the third clause satisfies the first clause; and

the third clause implies that if the third clause is satisfied the second clause is satisfied, wherein the third clause is not derived from the first clause.

22. The system of claim 20 , wherein the controller is further programmed to, prior to transmitting the command to the first solver:

identify the third vertex for removal; and

in response, identify via the successor edge, the second vertex for removal.

23. The system of claim 15 , wherein to identify the vertex corresponding to a clause to be restored, the controller is programmed to:

(i) identify, using the undo edge, the first vertex; and

(ii) identify, 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.

24. The system of claim 23 , wherein the command further comprises a signal to invalidate the first clause.

25. The system of claim 15 , wherein the controller is further programmed to:

receive 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

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

26. The system of claim 25 , wherein:

the first clause comprises a learned clause reachable from a first original clause corresponding to a first original vertex; and

the controller is further programmed to:

select a second original vertex corresponding to a second original clause for temporary invalidation, wherein: (i) the first clause was not derived from the second original clause, and (ii) the second clause is reachable from both the second original clause and the first clause; and

determine, prior to the transmitting step, that the second clause is invalid.

27. The system of claim 25 , wherein:

the first clause comprises a learned clause reachable from a first original clause corresponding to a first original vertex; and

the controller is further programmed to:

receive from a second solver of the plurality of solvers, a second message: (a) describing that the second solver at least in part learned: (i) a fifth clause from the first original clause, and (ii) the second clause from both the second original clause and the fifth clause, and retained the fifth clause from a data structure maintained by the second solver; and (b) identifying a second unique identifier associating the second clause described in the second message with the second solver;

create a fifth vertex corresponding to the fifth clause, and associating the fifth vertex with the second solver;

add a sixth vertex corresponding to the second clause described in the second message, and associating the sixth vertex with the second solver using the second unique identifier; and

form a successor edge from the fifth vertex to the sixth vertex without adding an undo edge from the sixth vertex to the fifth vertex.

28. The system of claim 15 , further comprising the plurality of solvers, wherein the controller is separate from each one of the plurality of solvers.