Exploring the Use of Shatter for AllSAT Through Ramsey-Type Problems
  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.
