About some UP-based polynomial fragments of SAT

详细信息    查看全文

• 作者：Balasim Al-Saedi ; Olivier Fourdrinoy…
• 关键词：SAT ; Unit Propagation ; Polynomial classes ; Quad ; UP ; Horn
• 刊名：Annals of Mathematics and Artificial Intelligence
• 出版年：2017
• 出版时间：March 2017
• 年：2017
• 卷：79
• 期：1-3
• 页码：25-44
• 全文大小：
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence (incl. Robotics); Mathematics, general; Computer Science, general; Complex Systems;
• 出版者：Springer International Publishing
• ISSN：1573-7470
• 卷排序：79

文摘

This paper explores several polynomial fragments of SAT that are based on the unit propagation (UP) mechanism. As a first case study, one Tovey’s polynomial fragment of SAT is extended through the use of UP. Then, we answer an open question about connections between the so-called UP-Horn class (and other UP-based polynomial variants) and Dalal’s polynomial Quad class. Finally, we introduce an extended UP-based pre-processing procedure that allows us to prove that some series of benchmarks from the SAT competitions are polynomial ones. Moreover, our experimentations show that this pre-processing can speed-up the satisfiability check of other instances.