Discovering Subproblems in SAT and #SAT using HPC

Boolean SAT(isfiability) and the related “counting” #SAT problem can be slow to solve on a serial computer. Use distributed HPC to cut formulae up into smaller pieces, so that search can then be distributed usefully and efficiently.

Picture of Charles Gretton

12 Jun 2023

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.

You are on Aboriginal land.

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.

arrow-left bars search times