Towards a Generic CNF Simplifier for Minimising Structured Problem Hardness

Abstract

CNF simplifiers play a very important role in minimising structured problem hardness. Altough they can be used in an in-search process, most of them serve in a pre-search phase and rely on one form or another of resolution. Based on our understanding about problem structure, in the paper, we extend the single pre-search process to a multiple one in order to further simplify the hard structure in a problem. This extension boosts the performance of state-of-theart clause learning and lookahead based SAT solvers when solving both satisfiable and unsatisfiable instances of many real-world hard combinatorial problems.