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 facilitating communication between a solver and a controller, the method comprising:
integrating an application program interface (API) with a solver configured to solve Boolean satisfiability (SAT) problems, the API being configured to receive a SAT instance representing a SAT problem to be solved and an incremental update to the SAT problem to be solved, the API comprising:
a first transmit function to notify from the solver to the controller, a clause learned by the solver and one or more antecedent clauses of the learned clause, the learned clause being a logical consequence of at least one of the one or more antecedent clauses;
a receive function to receive by the solver from the controller at least one of: (i) one or more clauses to be added to a solver database, and (ii) one or more clauses to be removed from the solver database.
2. The method of claim 1 , wherein the first transmit function is further configured to notify the controller, by the solver, another clause modified by the learned clause.
3. The method of claim 1 , further comprising invoking the first transmit function by the solver when a learnt clauses buffer reaches a limit on number of learnt clauses.
4. The method of claim 1 , further comprising processing by the solver one or more received clauses while the solver is running.
5. The method of claim 1 , further comprising processing by the solver one or more received clauses after the solver has stopped running, before the solver starts running again.
6. The method of claim 1 , wherein the API further comprises:
a second transmit function to notify to the controller a clause to be shared by the controller with one or more other solvers.
7. The method of claim 6 , further comprising invoking the second transmit function by the solver when a sharable clauses buffer reaches a limit on number of clauses to be shared.
8. An interface system for facilitating communication between a solver and a controller, comprising:
a memory module comprising instructions which, when executed by a processor configured as a solver configured to solve Boolean satisfiability (SAT) problems, provide an application program interface (API) to the solver, the API being configured to receive a SAT instance representing a SAT problem to be solved and an incremental update to the SAT problem to be solved, the API comprising:
a first transmit function to notify from the solver to the controller, a clause learned by the solver and one or more antecedents clauses of the learned clause, the learned clause being a logical consequence of at least one of the one or more antecedent clauses;
a receive function to receive by the solver from the controller at least one of: (i) one or more clauses to be added to a solver database, and (ii) one or more clauses to be removed from the solver database.
9. The system of claim 8 , wherein the first transmit function is further configured to notify the controller, by the solver, another clause modified by the learned clause.
10. The system of claim 8 , further comprising a solver configured to invoke the first transmit function when a learnt clauses buffer reaches a limit on number of learnt clauses.
11. The system of claim 8 , further comprising a solver configured to process one or more received clauses while the solver is running.
12. The system of claim 8 , further comprising a solver configured to process one or more received clauses after the solver has stopped running, before the solver starts running again.
13. The system of claim 8 , wherein the API further comprises:
a second transmit function to notify to the controller a clause to be shared by the controller with one or more other solvers.
14. The system of claim 13 , further comprising a solver configured to invoke the second transmit function when a sharable clauses buffer reaches a limit on number of clauses to be shared.