SHF: Small: IsoLator: Avoiding Isomorphic Graphs Effectively

SHF：小：IsoLator：有效避免同构图

• 批准号: 1526760
• 负责人: Marienus Heule
• 金额: $ 50万
• 依托单位: University of Texas at Austin
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-07-01 至 2019-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1526760&HistoricalAwards=false
• 关键词: SHF; Small; IsoLator; Avoiding; Isomorphic

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?

在过去的二十年里，可满足性（SAT）求解器的速度和能力已经提高了几个数量级，这使得更大和更复杂的真实的世界系统的验证和分析。然而，当代SAT求解器的一个弱点是它们的能力有限，无法避免对搜索空间的同构部分进行不必要的探索。本研究探讨了一种方法，显着提高SAT求解器的性能时，适用于图论问题。在这个项目中采取的方法侧重于打破所有对称性的SAT编码的图形相关的问题。关键的新概念是隔离器的概念：避免在同构类中评估多个图的命题公式。该项目研究了几个基本问题：（1）如何构造打破所有对称性的完美隔离器？(2)是否存在完美的隔离器，多项式的大小相应的图的问题？以及（3）完美隔离器如何提高SAT求解器在与硬图相关的问题上的性能？

项目成果

Strong Extension-Free Proof Systems

• DOI: 10.1007/s10817-019-09516-0
• 发表时间: 2020-03-01
• 期刊: JOURNAL OF AUTOMATED REASONING
• 作者: Heule, Marijn J. H.;Kiesl, Benjamin;Biere, Armin
• 通讯作者: Biere, Armin