Dagster: Parallel Structured Search with Case Studies

We describe Dagster, a system that implements a new approach to scheduling interdependent (Boolean) SAT search activities in high-performance computing (HPC) environments. This system allows practitioners to solve challenging problems by efficiently distributing search effort across computing cores in a customizable way. Our solver takes as input a set of disjunctive clauses (i.e., DIMACS CNF) and a labelled directed acyclic graph (DAG) structure describing how the clauses are decomposed into a set of interrelated search problems. Component problems are solved using standard systematic backtracking search, which may optionally be coupled to (stochastic dynamic) local search and/or clause-strengthening processes. We show the performance of Dagster in combinatorial case study examples, particularly the model counting of Costas arrays, and in finding solutions to large Pentomino tiling problems. We also use Dagster to exhibit a novel workflow for Bounded Model Checking of network protocols where we perform independent searches at different problem fidelities, in parallel. Low fidelity solutions trigger further independent searches for refined solutions in higher fidelity models.