LOCK-FREE STATE MERGING IN PARALLELIZED CONSTRAINT SATISFACTION PROBLEM SOLVERS

摘要

Parallel CSP (constraint satisfaction problem) solver state merges in the solver (solver state merging). The solver state during the process of parallel threads CSP solver of the calculation is represented by a series of support graph (support graph). Support graphs are calculated graphs (conflict-free graph) no new conflicts by merging pairs. The merge process has no cycles (cycle), conflict is removed, there is a thread handle lock (lock-free). This architecture is generally any type attribute (formal property) having any CSP solver can be applied in (for example, a Boolean SAT solver). And that the system is easily provide solver process, the system swelling component representing an input state of a calculation solver thread as a set of graphs (bookkeeping component) and the series of calculations to merge with at least two pairs of the graph graph of thread The inclusion of the final status of the merge component for calculating the merged graph representation (merge component).