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 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 equivalentliteral identification in a preprocessor engine for a SATsolver. The experiments show that the proposed technique is useful for solving real-world instances of the formal verification domain.

• Type: Conference
• Year: 2003
• Where: DATE
• Authors: Yakov Novikov
• Keywords: DATE 2003, Hardware, Relations Relating Variables, Unit Propagation, Unit Propagation Procedure