System and method for configuration of an ensemble solver

Patent metadata

Field	Value
Publication number	US-9684865-B1
Application number	US-201313910467-A
Country	US
Kind code	B1
Filing date	Jun 5, 2013
Priority date	Jun 5, 2012
Publication date	Jun 20, 2017
Grant date	Jun 20, 2017

Abstract

In a system for enabling configuration of an ensemble of several solvers, such that the ensemble can efficiently solve a constraint problem, for each one of several candidate configurations, an array of scores is computed. The array corresponds to a statistical parameter related to a problem solution, and the computation is based on, at least in part, a set of features associated with the problem. One candidate configuration is assigned to a solver, and based on the array of scores associated with that candidate configuration the same or a different candidate configuration is assigned to a another solver. A system for dynamically reconfiguring an ensemble of solvers obtains runtime data from several solvers, and a new configuration is determined by applying a machine learning and/or heuristic analysis procedure to the runtime data. The configuration of a solver may be updated according to the new configuration while that solver is running.

First claim

Accordingly, we claim:

1. A method for assigning a set of configurations to an ensemble comprising a plurality of solvers, the method comprising:
for each candidate configuration in a plurality of candidate configurations, computing by a processor, based on, at least in part, a first set of features stored in memory, an array of aggregate scores, the array corresponding to a statistical parameter corresponding to a solution to the problem, and the first set of features being associated with a problem to be solved by the ensemble;
assigning by the processor to a first solver in the plurality of solvers a first candidate configuration selected from the plurality of candidate configurations, based on, at least in part, the computed arrays of aggregate scores, wherein each solver in the plurality of solvers is adapted to receive a constraint on a variable and to assign a value to the variable.

2. The method of claim 1 , wherein computing the array of aggregate scores comprises applying by the processor, a machine learning (ML) procedure to the first set of features.

3. The method of claim 1 , further comprising assigning to a second solver in the plurality of solvers a second candidate configuration selected from the plurality of candidate configurations, the selection of the second candidate configuration being based on, at least in part, the computed arrays of aggregate scores.

4. The method of claim 3 , wherein the second candidate configuration is same as the first candidate configuration.

5. The method of claim 3 , further comprising selecting a set of candidate configurations from the plurality of candidate configurations based on, at least in part, the computed arrays of aggregate scores, wherein the set of candidate configurations comprises the first candidate configuration and the second candidate configuration.

6. The method of claim 1 , wherein:
each candidate configuration comprises a set of configuration parameters, a value for each configuration parameter being selectable from at least one option; and
for each candidate configuration, the computation of an aggregate score in the array comprises assigning an option score to each configuration parameter based on, at least in part, an option designated to the configuration parameter.

7. The method of claim 6 , further comprising generating by the processor the plurality of candidate configurations by:
designating a first option to a first configuration parameter of the first candidate configuration; and
designating a second option to the first configuration parameter of another candidate configuration.

8. The method of claim 6 , wherein the aggregate score comprises a linear summation of the option scores assigned to the configuration parameters.

9. The method of claim 6 , wherein a configuration parameter from the set of configuration parameters is selected from the group consisting of a restart frequency, a decision heuristic, a use of conflict clause minimization, a number of conflict clauses to generate from each conflict, use of database compaction, a decay rate for a decision heuristic score, a frequency of sharing information between two solvers of the ensemble, selection indicative of information to be shared between the two solvers, and size of information to be shared between two solvers.

10. The method of claim 6 , wherein a configuration parameter from the set of configuration parameters comprises a combination parameter that comprises a combination of at least two of a restart frequency, a decision heuristic, a use of conflict clause minimization, a number of conflict clauses to generate from each conflict, use of database compaction, a decay rate for a decision heuristic score, a frequency of sharing information between two solvers of the ensemble, selection indicative of information to be shared between the two solvers, and size of information to be shared between two solvers.

11. The method of claim 1 , wherein:
the array of aggregate scores computed for the first candidate configuration comprises a first aggregate score and a second aggregate score; and
the second aggregate score is based on, at least in part, a distribution range associated with the statistical parameter.

12. The method of claim 11 , wherein the second aggregate score represents a value for assigning a copy of the first candidate configuration to a solver in the ensemble.

13. The method of claim 11 , further comprising assigning to a second solver in the plurality of solvers the first candidate configuration based on, at least in part, the second aggregate score in the array of scores.

14. The method of claim 13 , wherein the plurality of solvers in the ensemble comprises a plurality of Boolean satisfiability solvers, the method further comprising assigning to the first and second solvers first and second seeds, respectively, the second seed being different than the first seed.

15. The method of claim 11 , further comprising assigning to a second solver in the plurality of solvers a second candidate configuration that is both: (i) different than the first candidate configuration, and (ii) selected from the plurality of candidate configurations based on, at least in part, the second aggregate score in the array of scores computed for the first candidate configuration.

16. The method of claim 1 , wherein computing the array of aggregate scores comprises analyzing: (i) the plurality of candidate solver configurations, (ii) a second set of features, (iii) training data associating the plurality of candidate solver configurations and the second set of features, and (iv) the first set of features.

17. The method of claim 1 , wherein the problem to be solved comprises a constraint satisfaction problem.

18. The method of claim 1 , further comprising: deriving by the processor the first set of features associated with the problem to be solved, derivation being based on at least one of: (i) specification of the problem, and (ii) runtime data received from at least one solver.

19. The method of claim 1 , wherein the statistical parameter comprises an expected time required to find the solution to the problem.

20. The method of claim 1 , further comprising:
receiving in memory, from at least a subset of solvers in the ensemble, runtime data associated with the set of configurations assigned to the ensemble;
updating an aggregate score in an array of aggregate scores associated with the first candidate configuration that is assigned to the first solver, by applying, by the processor, at least one of a heuristic analysis procedure and another machine learning procedure to the runtime data.

21. The method of claim 20 , further comprising:
updating, based on the updated aggregate score, a score for an option designated to a configuration parameter of the first candidate configuration;
updating, based on the updated score of the option, an option score for another candidate configuration in which a corresponding configuration parameter is also designated the option designated to the configuration parameter of the first candidate configuration; and
updating an aggregate score for the other candidate configuration based on, at least in part, the updated option score for the other candidate configuration.

22. A system for assigning a set of configurations to an ensemble comprising a plurality of solvers, the system comprising:
a memory; and
a processor in electronic communication with the memory, wherein the processor is configured to:
for each c

Assignees

• Reservoir Labs Inc
• Significs And Elements Llc

Inventors

• Ezick James
• Springer Jonathan
• Vasilache Nicolas T

Classifications

• G06N5/01

  Dynamic search techniques; Heuristics; Dynamic trees; Branch-and-bound · CPC title

• G06N5/02 Primary

  Knowledge representation; Symbolic representation · CPC title

• G06N99/005

  Physics · mapped topic

• G06N20/20 Primary

  Ensemble learning · CPC title

• G06N20/00 Primary

  Machine learning · CPC title