About some UP-based polynomial fragments of SAT - Université d'Artois Accéder directement au contenu
Article Dans Une Revue Annals of Mathematics and Artificial Intelligence Année : 2017

About some UP-based polynomial fragments of SAT

Résumé

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.
Fichier non déposé

Dates et versions

hal-03300429 , version 1 (27-07-2021)

Identifiants

  • HAL Id : hal-03300429 , version 1

Citer

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, 2017, 79 (1), pp.25-44. ⟨hal-03300429⟩
13 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More