Dagster: Parallel Structured Search

Mark Alexander Burgess, Charles Gretton, Josh Milthorpe, Luke Croak, Thomas Willingham, Alwen Tiu

AAAI 2023 pp. 16404-16406

doi:10.1609/AAAI.V37I13.27060 /aaai/2023/burgess2023aaai-dagster/

Abstract

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).

PDF AAAI Semantic Scholar

Cite

Text

Burgess et al. "Dagster: Parallel Structured Search." AAAI Conference on Artificial Intelligence, 2023. doi:10.1609/AAAI.V37I13.27060

Markdown

[Burgess et al. "Dagster: Parallel Structured Search." AAAI Conference on Artificial Intelligence, 2023.](https://mlanthology.org/aaai/2023/burgess2023aaai-dagster/) doi:10.1609/AAAI.V37I13.27060

BibTeX

@inproceedings{burgess2023aaai-dagster,
  title     = {{Dagster: Parallel Structured Search}},
  author    = {Burgess, Mark Alexander and Gretton, Charles and Milthorpe, Josh and Croak, Luke and Willingham, Thomas and Tiu, Alwen},
  booktitle = {AAAI Conference on Artificial Intelligence},
  year      = {2023},
  pages     = {16404-16406},
  doi       = {10.1609/AAAI.V37I13.27060},
  url       = {https://mlanthology.org/aaai/2023/burgess2023aaai-dagster/}
}