Lock-free state merging in parallelized constraint satisfaction problem solvers

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.

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.