Let the Solver Deal with Redundancy

Handling redundancy in propositional reasoning and search is an active path of theoretical research. For instance, the complexity of some redundancy-related problems for CNF formulae and for their 2-SAT and Horn SAT fragments have been recently studied. However, this issue is not actually addressed in practice in modern SAT solvers, and is most of the time just ignored. Dealing with redundancy in CNF formulae while preserving the performance of SAT solvers is clearly an important challenge. In this paper, a self-adaptative process is proposed to manage redundant clauses, enabling redundant information to be discriminated and to keep only the one that proves useful during the search.