CONTEXT : Dagster is an ANU built High Performance Computing (HPC) Boolean SAT(isfiability) solver that presently implements CPU bound algorithms for the SAT problem.
PROJECT : Develop and implement new HPC algorithms for automatically learning/synthesizing decompositions of SAT and #SAT problems. For the context on this workstream, Dagster currently requires the user describe how a problem is decomposable. That design decision was justified for two reasons: (i) our primary objective has been to accelerate Boolean search in HPC environments, thus the details of how to schedule search activities, and communication between them, was our dominant concern historically, and (ii) in a range of applications a good decomposition is known a priori, and do not have to be discovered. For example, this is the case in Bounded Model Checking and AI planning, the decompositions are well known.
Nonetheless, we have encountered a number of case studies where a good non-naïve decomposition is not obvious. Moreover, although compositionality is a much studied topic in the SAT related science literature, the scenario of using distributed computing to find good decompositions is one that has not received attention by the SAT research community.
The project is to develop an HPC approach in Dagster to automatically find decompositions that enable us to accelerate, or scale, search in HPC environments. The availability of an HPC environment is a key and novel resource to contemplate in this setting.