Parallelising Lazy Clause Generation with Trail Sharing

We investigate the effectiveness of splitting the search space in parallelising the state-of-the-art CP-SAT solver. One of the key barriers to effective search-space splitting in learning solvers is the generated sub-problems are not independent, leading to substantial communication-related overhead, substantial redundant work, or both. Our contributions attempt to mitigate this issue: job reassignment; and trail sharing. Jobs (sub-trees) are reassigned to new workers if the clause database of the currently assigned worker appears ill-suited to the region of the search-space, when doing so workers can share some of the state from their local trail. We argue a trail prefix can be viewed as a lossy compressed representation of much of the relevant information a worker has learnt about a job, this information can be exploited by the next worker assigned the same subtree to avoid some redundant work. We show these approaches complement standard portfolio and clause-sharing approaches, improving CP-SAT’s performance on MiniZinc challenge benchmarks with a moderate number of worker threads. To enable these approaches, we also introduce “Buffered Work Stealing,” which can be parameterised to emulate the two main existing approaches to search-space splitting in the literature: Work Stealing and Embarassingly Parallel Search, as well as an intermediate configuration between these two extremes that slightly outperforms both.