Dagster is 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. The performance of Dagster has been measured in combinatorial case study examples, particularly the model counting of Costas arrays, and in finding solutions to large Pentomino tiling problems. You can download those case studies with the tool. 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 solutio s in higher fidelity models.