Exploring the Use of Shatter for AllSAT Through Ramsey-Type Problems

TL;DR

This paper investigates the application of Shatter for symmetry breaking in AllSAT problems related to Ramsey theory, highlighting its drawbacks and proposing strategies to mitigate issues like model blow-up and incomplete solutions.

Contribution

It identifies key challenges in using Shatter for AllSAT in Ramsey problems and offers practical strategies to improve its effectiveness and reliability.

Findings

Shatter can cause a blow-up in the number of models.

Naive use of Shatter may lead to incomplete sets of solutions.

Proposed strategies help mitigate these issues in symmetry breaking.

Abstract

In the context of SAT solvers, Shatter is a popular tool for symmetry breaking on CNF formulas. Nevertheless, little has been said about its use in the context of AllSAT problems: problems where we are interested in listing all the models of a Boolean formula. AllSAT has gained much popularity in recent years due to its many applications in domains like model checking, data mining, etc. One example of a particularly transparent application of AllSAT to other fields of computer science is computational Ramsey theory. In this paper we study the effect of incorporating Shatter to the workflow of using Boolean formulas to generate all possible edge colorings of a graph avoiding prescribed monochromatic subgraphs. Generating complete sets of colorings is an important building block in computational Ramsey theory. We identify two drawbacks in the na\"ive use of Shatter to break the symmetries of Boolean formulas encoding Ramsey-type problems for graphs: a "blow-up" in the number of models and the generation of incomplete sets of colorings. The issues presented in this work are not intended to discourage the use of Shatter as a preprocessing tool for AllSAT problems in combinatorial computing but to help researchers properly use this tool by avoiding these potential pitfalls. To this end, we provide strategies and additional tools to cope with the negative effects of using Shatter for AllSAT. While the specific application addressed in this paper is that of Ramsey-type problems, the analysis we carry out applies to many other areas in which highly-symmetrical Boolean formulas arise and we wish to find all of their models.