Sciweavers

ICTAI
2008
IEEE

Let the Solver Deal with Redundancy

13 years 10 months ago
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.
Cédric Piette
Added 31 May 2010
Updated 31 May 2010
Type Conference
Year 2008
Where ICTAI
Authors Cédric Piette
Comments (0)