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