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.