Skip to Main content Skip to Navigation
New interface
Journal articles

About some UP-based polynomial fragments of SAT

Abstract : 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.
Document type :
Journal articles
Complete list of metadata
Contributor : Fabien DELORME Connect in order to contact the contributor
Submitted on : Tuesday, July 27, 2021 - 10:19:00 AM
Last modification on : Wednesday, November 3, 2021 - 9:19:40 AM


  • HAL Id : hal-03300429, version 1



Balasim Al-Saedi, Olivier Fourdrinoy, Éric Grégoire, Bertrand Mazure, Lakhdar Saïs. About some UP-based polynomial fragments of SAT. Annals of Mathematics and Artificial Intelligence (AMAI), 2017, 79 (1), pp.25-44. ⟨hal-03300429⟩



Record views