Solving difficult SAT instances using greedy clique decomposition

Abstract

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.

Keywords

• Solving
• difficult
• instances
• using
• greedy
• clique
• decomposition