Dagster: Parallel Structured Search


  • Mark Alexander Burgess Australian National University
  • Charles Gretton Australian National University
  • Josh Milthorpe Australian National University
  • Luke Croak Australian National University
  • Thomas Willingham Australian National University
  • Alwen Tiu Australian National University




SAT, High-Performance Computing, Decomposition


We demonstrate Dagster, a system that implements a new approach to scheduling interdependent (Boolean) SAT search activities in high-performance computing (HPC) environments. Our system 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 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 demonstrate Dagster using a new Graph Maximal Determinant combinatorial case study. This demonstration paper presents a new case study, and is adjunct to the longer accepted manuscript at the Pacific Rim International Conference on Artificial Intelligence (2022).




How to Cite

Burgess, M. A., Gretton, C., Milthorpe, J., Croak, L., Willingham, T., & Tiu, A. (2023). Dagster: Parallel Structured Search. Proceedings of the AAAI Conference on Artificial Intelligence, 37(13), 16404-16406. https://doi.org/10.1609/aaai.v37i13.27060