SHF: Small: IsoLator: Avoiding Isomorphic Graphs Effectively

点击翻译按钮获取中文摘要

Over the last two decades, the speed and capacity of Satisfiability (SAT) solvers has improved by several orders of magnitude, which enabled the verification and analysis of larger and more complex real world systems. However, a weaknesses of contemporary SAT solvers is their limited ability to obviate needless exploration of isomorphic parts of the search space. This research investigates an approach to significantly improve the performance of SAT solvers when applied to problems of graph theory. The approach taken in this project focuses on breaking all symmetries of SAT encodings of graph-related problems. The key new concept is the notion of isolators: propositional formulas that avoid evaluating multiple graphs in an isomorphism class. The project investigates several foundational questions: (1) how to construct perfect isolators which break all symmetries? (2) whether perfect isolators that are polynomial in the size of the corresponding graph problem exist? and (3) how perfect isolators boost SAT solver performance on hard graph-related problems?