Abstract:

The difficulty of solving Boolean formulae is mainly decided by the key literals. If the key literals or subset of formulas could be found, they  would be tractable to solve the formula. The principle of the warning propagation was studied, and it was found that the decision part variables of high probability were important for solving the Boolean formulae. It was also found that if the warning message had consistency between the clause and variable, the variable could decide the clause satisfiability, while other variables did not contribute to satisfiability of the clause. Furthermore, it was proved that the part variables were the subset of the key literals when the warning propagation was convergent, which showed that the warning propagation could be used to find the key literals for the formulae. Finally, the massage passing algorithm to find the key literals was given by the warning propagation characterization.
 

Key words: message passing, warning propagation algorithm, analysis of principle, key literal