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.
Please help me write a proper abstract based on the patent claims. CLAIM: 1. A method for sharing clauses across an ensemble of a plurality of solvers, the method comprising performing by a sharing module the steps of: receiving from a first solver a first message comprising: (i) a first clause to be shared, and (ii) a first identifier corresponding to the first clause and associating the first clause with the first solver; determining that a second solver: (i) has not learned the first clause, and that (ii) the first clause corresponding to the first identifier was not transmitted to the second solver; transmitting the first clause and the corresponding first identifier to the second solver; and updating a database indicating that the first clause corresponding to the first identifier was transmitted to the second solver. 2. The method of claim 1, further comprising: determining that a third solver: (i) has not learned the first clause, and that (ii) the first clause corresponding to the first identifier was not transmitted to the third solver; transmitting the first clause and the corresponding first identifier to the third solver; and updating the database further, indicating that the first clause corresponding to the first identifier was transmitted to the third solver. 3. The method of claim 1, further comprising: determining that the first clause corresponding to the first identifier was invalidated; and transmitting a message to the second solver, informing the second solver that the first clause corresponding to the first identifier is invalidated. 4. The method of claim 1, further comprising: determining, after updating the database, that the second solver: (i) has learned a particular clause, and (ii) has assigned a second identifier corresponding to the particular clause and associating the particular clause with the second solver; determining that the particular clause corresponding to the second identifier is same as the first clause corresponding to the first identifier; and transmitting a second message to the second solver, informing the second solver that the first identifier corresponding to the first clause is invalidated. 5. The method of claim 1, further comprising: receiving from the second solver, after updating the database, a second message comprising: (i) a particular clause to be shared, and (ii) a second identifier corresponding to the particular clause and associating the particular clause with the second solver; determining that the particular clause corresponding to the second identifier is same as the first clause corresponding to the first identifier; and determining that the particular clause is not be transmitted to the first solver. 6. The method of claim 1, further comprising: receiving from a third solver a third message comprising: (i) a particular clause to be shared, and (ii) a third identifier corresponding to the particular clause and associating the particular clause with the third solver. 7. The method of claim 6, wherein the third message is received prior to transmitting the first clause corresponding to the first identifier to the second solver, the method further comprising: determining that the particular clause corresponding to the third identifier is same as the first clause corresponding to the first identifier; determining that the particular clause is not be transmitted to the first solver and the second solver; and determining that the first clause corresponding to the first identifier is not to be transmitted to the third solver. 8. The method of claim 7, further comprising: determining, after transmitting the first clause and the corresponding first identifier to the second solver, that the first clause corresponding to the first identifier was invalidated; and transmitting the particular clause and the corresponding third identifier to the first solver; and updating the database indicating that the particular clause corresponding to the third identifier was transmitted to the first solver. 9. The method of claim 6, further comprising: determining that the particular clause corresponding to the third identifier is different from the first clause corresponding to the first identifier; testing whether the particular clause is to be transmitted to the first solver and the second solver; and testing whether the first clause corresponding to the first identifier is to be transmitted to the third solver. 10. The method of claim 9, further comprising, at least one of: transmitting the particular clause and the corresponding third identifier to at least one of the first solver and the second solver; and transmitting the first clause and the corresponding first identifier to the third solver. 11. The method of claim 1, wherein determining that the second solver has not learned the first clause comprises using a hash-based comparison of the first clause and each clause learned by the second solver. 12. The method of claim 1, wherein the sharing module is separate from each one of the plurality of solvers. 13. A method for sharing clauses across an ensemble of a plurality of solvers, the method comprising performing by a sharing module the steps of: receiving from a first solver a first message comprising: (i) a first clause designated sharable by the first solver, (ii) a score designated to the first clause by the first solver; and (iii) a first identifier corresponding to the first clause and associating the first clause with the first solver; analyzing at least one of: (i) a characteristic of the first clause, and (ii) the designated score, to determine if the first clause is to be shared. 14. The method of claim 13, wherein analyzing the characteristic comprises at least one of: determining if a number of literals in the first clause is at most equal to a first limit on number of literals; and determining if a number of literals in the first clause is at least equal to a second limit on number of literals. 15. The method of claim 13, wherein analyzing the score comprises determining if the score is at least equal to a score threshold. 16. The method of claim 13, further comprising: determining that a second solver: (i) has not learned the first clause, and that (ii) the first clause corresponding to the first identifier was not transmitted to the second solver; transmitting the first clause and the corresponding first identifier to the second solver; and updating a database indicating that the first clause corresponding to the first identifier was transmitted to the second solver. 17-23. (canceled) 24. A system for sharing clauses across 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 sharing module to: receive from a first solver a first message comprising: (i) a first clause to be shared, and (ii) a first identifier corresponding to the first clause and associating the first clause with the first solver; determine that a second solver: (i) has not learned the first clause, and that (ii) the first clause corresponding to the first identifier was not transmitted to the second solver; transmit the first clause and the corresponding first identifier to the second solver; and update a database indicating that the first clause corresponding to the first identifier was transmitted to the second solver. 25. The system of claim 24, wherein the sharing module is further programmed to: determine that a third solver: (i) has not learned the first clause, and that (ii) the first clause corresponding to the first identifier was not transmitted to the third solver; transmit the first clause and the corresponding first identifier to the third solver; and update the database further, indicating that the first clause corresponding to the first identifier was transmitted to the third solver. 26. The system of claim 24, wherein the sharing module is further programmed to: determine that the first clause corresponding to the first identifier was invalidated; and transmit a message to the second solver, informing the second solver that the first clause corresponding to the first identifier is invalidated. 27. The system of claim 24, wherein the sharing module is further programmed to: determine, after updating the database, that the second solver: (i) has learned a particular clause, and (ii) has assigned a second identifier corresponding to the particular clause and associating the particular clause with the second solver; determine that the particular clause corresponding to the second identifier is same as the first clause corresponding to the first identifier; and transmit a second message to the second solver, informing the second solver that the first identifier corresponding to the first clause is invalidated. 28. The system of claim 24, wherein the sharing module is further programmed to: receive from the second solver, after updating the database, a second message comprising: (i) a particular clause to be shared, and (ii) a second identifier corresponding to the particular clause and associating the particular clause with the second solver; determine that the particular clause corresponding to the second identifier is same as the first clause corresponding to the first identifier; and determine that the particular clause is not be transmitted to the first solver. 29. The system of claim 24, wherein the sharing module is further programmed to: receive from a third solver a third message comprising: (i) a particular clause to be shared, and (ii) a third identifier corresponding to the particular clause and associating the particular clause with the third solver. 30. The system of claim 29, wherein: the third message is received prior to transmitting the first clause corresponding to the first identifier to the second solver; and the sharing module is further programmed to: determine that the particular clause corresponding to the third identifier is same as the first clause corresponding to the first identifier; determine that the particular clause is not be transmitted to the first solver and the second solver; and determine that the first clause corresponding to the first identifier is not to be transmitted to the third solver. 31. The system of claim 30, wherein the sharing module is further programmed to: determine, after transmitting the first clause and the corresponding first identifier to the second solver, that the first clause corresponding to the first identifier was invalidated; and transmit the particular clause and the corresponding third identifier to the first solver; and update the database indicating that the particular clause corresponding to the third identifier was transmitted to the first solver. 32. The system of claim 29, wherein the sharing module is further programmed to: determine that the particular clause corresponding to the third identifier is different from the first clause corresponding to the first identifier; test whether the particular clause is to be transmitted to the first solver and the second solver; and test whether the first clause corresponding to the first identifier is to be transmitted to the third solver. 33. The system of claim 32, wherein the sharing module is further programmed to, at least one of: transmit the particular clause and the corresponding third identifier to at least one of the first solver and the second solver; and transmit the first clause and the corresponding first identifier to the third solver. 34. The system of claim 24, wherein to determine that the second solver has not learned the first clause the sharing module is programmed to perform a hash-based comparison of the first clause and each clause learned by the second solver. 35. The system of claim 24, further comprising the plurality of solvers, wherein the sharing module is separate from each one of the plurality of solvers. 36. A system for sharing clauses across 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 sharing module to: receive from a first solver a first message comprising: (i) a first clause designated sharable by the first solver, (ii) a score designated to the first clause by the first solver; and (iii) a first identifier corresponding to the first clause and associating the first clause with the first solver; analyze at least one of: (i) a characteristic of the first clause, and (ii) the designated score, to determine if the first clause is to be shared. 37. The system of claim 36, wherein to analyze the characteristic the sharing module is programmed to, at least one of: determine if a number of literals in the first clause is at most equal to a first limit on number of literals; and determine if a number of literals in the first clause is at least equal to a second limit on number of literals. 38. The system of claim 36, wherein to analyze the score the sharing module is programmed to determine if the score is at least equal to a score threshold. 39. The system of claim 36, wherein the sharing module is further programmed to: determine that a second solver: (i) has not learned the first clause, and that (ii) the first clause corresponding to the first identifier was not transmitted to the second solver; transmit the first clause and the corresponding first identifier to the second solver; and update a database indicating that the first clause corresponding to the first identifier was transmitted to the second solver. 40-46. (canceled)