We propose a method for local search of Boolean relatio s relating variables of a CNF formula. The method is to branch on small subsets of the set of CNF variables and to analyze 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 of the formal verification domain.