Reducing hard SAT instances to polynomial ones

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 polynomialtime and thus easy-to-solve ones.

• Type: Conference
• Year: 2007
• Where: IRI
• Authors: Olivier Fourdrinoy, Éric Grégoire, Bertrand Mazure, Lakhdar Sais
• Keywords: Information Retrieval, IRI 2007, Propositional Reasoning, Reasoning Paradigms Thanks, Satisfiability Checking Procedures