Lock-free state merging in parallelized constraint satisfaction problem solvers

• US 7,543,266 B2
• Filed: 11/20/2006
• Issued: 06/02/2009
• Est. Priority Date: 11/20/2006
• Status: Active Grant

• Current Assignee: Microsoft Technology Licensing LLC (Microsoft Corporation)
• Original Assignee: Microsoft Corporation
• Inventors: Brown, Allen L. Jr.
• Primary Examiner(s): Chiang; Jack
• Assistant Examiner(s): Doan; Nghia M
• Application Number:
  US11/602,092
• Publication Number:
  US 20080120490A1
• Time in Patent Office: 925 Days
• Field of Search: 716 1- 18, 703 13- 22, 706 10- 11, 706/19, 706/26
• US Class Current: 716/101
• CPC Class Codes: G06F 8/3135 Unification or backtracking
• CPC Class Codes: G06F 8/314 Parallel programming languages G06F8/313 takes precedence
• CPC Class Codes: G06F 9/5061 Partitioning or combining of resources
• CPC Class Codes: G06N 20/10 using kernel methods, e.g. support vector machines [SVM]
• CPC Class Codes: G06N 3/08 Learning methods
• CPC Class Codes: G06N 5/01 Dynamic search techniques; Heuristics; Dynamic trees; Branch-and-bound
• CPC Class Codes: G06N 5/048 Fuzzy inferencing
• CPC Class Codes: G06N 7/01 Probabilistic graphical models, e.g. probabilistic networks

Abstract

Solver state merging in parallel constraint satisfaction problem (CSP) solvers. Solver state during processing of a computational thread of parallel CSP solvers is represented as a set of support graphs. The support graphs are merged in a pairwise fashion, yielding a new conflict-free graph. The merge process is free of cycles, conflicts are removed, and thread processing is lock-free. The architecture can be applied, generally, in any CSP solver (e.g., a Boolean SAT solver) having certain formal properties. A system is provided that facilitates solver processing, the system comprising a bookkeeping component for representing input solver state of a computational thread as a set of graphs, and a merge component for pairwise merging of at least two input graphs of the set of graphs into a merged graph that represents final state of the computational thread.

Claims

1. A computer-implemented system that facilitates constraint solver processing, comprising:

a bookkeeping component for representing input solver state of a computational thread as a set of graphs, the input solver state received from parallel solvers operating on the computational thread;

a merge component for pairwise merging of at least two input graphs of the set of graphs into a merged graph that represents final state of the computational thread;

a propagation component for constraint propagation to generate completeness in the merged graph, wherein the propagation component facilitates non-chronological backtracking as part of the constraint propagation to directly change an earlier assumption without changing an intermediate assumption and the propagation component facilitates adding more than one learned constraint during constraint propagation of the merged graph for the parallel solvers, which are parallel SAT solvers, wherein the representing input set of support graphs to be merged by the merge component are conflict-free support graphs.

2. The system of claim 1, wherein the bookkeeping component receives the input solver state from parallel Boolean satisfiability (SAT) solvers operating on the computational thread.

3. The system of claim 1, wherein the bookkeeping component receives the input solver state from parallel constraint satisfaction problem (CSP) solvers operating on the computational thread.

4. The system of claim 3, wherein the CSP solvers are defined according to a lattice of valuations A and a set of values D, where D and A are the same set.

5. The system of claim 1, wherein the merge component merges the input solver state into the merged graph in a lock-free manner.

6. The system of claim 1, further comprising a learning and reasoning component for inferring a variable assignment based on a guess during a constraint propagation process.

7. The system of claim 1, wherein the input solver state is from two parallel SAT solvers operating on the computational thread, and the merge component facilitates adding n new and distinct literals to each of n copies of an L-complete, K-consistent deduction graph, where n is a positive integer.

8. A computer-implemented method of constraint solver processing, comprising:

representing input solver state of a computational thread as a set of support graphs;

receiving the support graphs associated with solver state of parallel solvers, the solver state associated with processing of the computational thread;

paring a support graph from each of the parallel solvers for merging of nodes having same literal;

pairwise merging the support graphs into a merged graph that represents final state of the computational thread;

solving completeness of the merged graph by propagating constraints utilizing non-chronological backtracking as part of the constraint propagation to directly change an earlier assumption without changing an intermediate assumption;

adding more than one learned constraint during constraint propagation of the merged graph for the parallel solvers, which are parallel SAT solvers; and

processing conflicting literals of the merged graph to make the merged graph conflict-free.

9. The method of claim 8, further comprising paring down the support graphs for the pairwise merging according to nodes having same literals.

10. The method of claim 8, further comprising manipulating the support graphs of the respective parallel solvers simultaneously.

11. The method of claim 8, further comprising eliminating a conflicting literal from a set of conflicting literals and designating remaining conflicting literals of the set as assumptions for a new deduction graph.

12. The method of claim 8, wherein the parallel solvers are Boolean SAT solvers.

13. A computer-implemented solver system, comprising:

computer-implemented means for representing input solver state of a computational thread as a set of support graphs;

computer-implemented means for receiving the support graphs from parallel CSP solvers, the support graphs representative of parallel solver state associated with processing of the computational thread;

computer-implemented means for paring support graphs from each of the parallel CSP solvers;

computer-implemented means for pairwise merging the support graphs into a merged graph;

computer-implemented means for eliminating conflicts in the merged graph to output a conflict-free merged graph that represents final state of the computational thread;

computer-implemented means for solving completeness of the merged graph by propagating constraints utilizing non-chronological backtracking as part of the constraint propagation to directly change an earlier assumption without changing an intermediate assumption; and

computer-implemented means for adding more than one learned constraint during constraint propagation of the merged graph for the parallel solvers, which are parallel SAT solvers.