Title :
Reducing hard SAT instances to polynomial ones
Author :
Fourdrinoy, Olivier ; Grégoire, Éric ; Mazure, Bertrand ; Sais, Lakhdar
Author_Institution :
Univ. d´´Artois, Lens
Abstract :
This last decade, propositional reasoning and search has been one of the hottest topics of research in the A.I. community, as the Boolean framework has been recognized as a powerful setting for many reasoning paradigms thanks to dramatic improvements of the efficiency of satisfiability checking procedures. SAT, namely checking whether a set of propositional clauses is satisfiable or not, is the technical core of this framework. In the paper, a new linear-time pre-treatment of SAT instances is introduced. Interestingly, it allows us to discover a new polynomial-time fragment of SAT that can be recognized in linear-time, and show that some benchmarks from international SAT competitions that were believed to be difficult ones, are actually polynomial-time and thus easy-to-solve ones.
Keywords :
computability; computational complexity; Boolean framework; linear time SAT pretreatment; polynomial-time fragment; propositional clauses; propositional reasoning; satisfiability checking procedure; Lenses; Optical propagation; Polynomials;
Conference_Titel :
Information Reuse and Integration, 2007. IRI 2007. IEEE International Conference on
Conference_Location :
Las Vegas, IL
Print_ISBN :
1-4244-1500-4
Electronic_ISBN :
1-4244-1500-4
DOI :
10.1109/IRI.2007.4296591