Local search for Boolean relations on the basis of unit propagation

We propose a method for local search of Boolean relations relating variables of a CNF (conjunctive normal form) formula. The method is to branch on small subsets of the set of CNF variables and to analyze the results of unit propagation. By taking into account variable value assignments, deduced during the unit propagation procedure, the method is able to justify any relation represented by a Boolean expression. The proposed technique is based on bitwise logical operations over ternary vectors. We implement a restricted version of the method, used for unit clause derivation and equivalent-literal identification, in a preprocessor engine for a SAT-solver. The experiments show that the proposed technique is useful for solving real-world instances in the formal verification domain.