Publication at Faculty of Mathematics and Physics |
2007
Abstract
We are dealing with solving difficult SAT instances in this paper. We propose a method for preprocessing SAT instances (CNF formulas) by using consistency techniques known from constraint programming methodology and by using our own consistency technique based on clique decomposition of a graph representing conflicts in the input formula.