Skip to Main content Skip to Navigation
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

https://hal-univ-artois.archives-ouvertes.fr/hal-03300429
Contributor : Fabien Delorme <>
Submitted on : Tuesday, July 27, 2021 - 10:19:00 AM
Last modification on : Thursday, September 9, 2021 - 3:10:29 PM

Identifiers

  • HAL Id : hal-03300429, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

6