Computing Unavoidable Subgraphs Using SAT Solvers Cuong Chau ACL2 Seminar Nov. 9, 2015 Abstract: Symmetry-breaking methods have been highly crucial for solving Boolean satisfiability problems (SAT) with large numbers of symmetries. However, existing state-of-the-art symmetry-breaking methods are not powerful enough to help SAT solvers successfully solving hard graph-related problems, such as computing Ramsey number R(4, 5). Yet, lots of symmetries are not broken by the existing symmetry-breaking methods. Our goal is to develop a new method for breaking symmetries of SAT encodings of graph-related problems using "isolators", i.e., propositional formulas that help to avoid examining isomorphic graphs. Ideally, we want to construct "perfect isolators" (i.e., isolators that break all symmetries) with reasonable sizes. Our approach is to construct a perfect isolator incrementally: start with some initial isolator and iteratively extend the isolator with one clause per step until it is perfect. In this talk, I will illustrate that an initial isolator constructed from "unavoidable subgraphs" is a good candidate. More specifically, I will focus on answering the following three questions: 1. What is an unavoidable subgraph? 2. How to efficiently compute unavoidable subgraphs of a given complete graph? 3. How to derive an isolator from unavoidable subgraphs?