Paper Info
Title
Exploring the Use of Shatter for AllSAT Through Ramsey-Type Problems.
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. 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. We identify two drawbacks in the naive use of Shatter to break the symmetries of Boolean formulas encoding Ramsey-type problems for graphs.
Year
Venue
DocType
2018
THIRTY-SECOND AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE / THIRTIETH INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE / EIGHTH AAAI SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCE
Conference
Volume
Citations 
PageRank 
abs/1711.06362
0
0.34
References 
Authors
11
1
Name
Order
Citations
PageRank
David E. Narváez100.68