Towards an Efficient Tableau Method for Boolean Circuit Satisfiability Checking

Boolean circuits offer a natural, structured, and compact representation of Boolean functions for many application domains. In this paper a tableau method for solving satisfiability problems for Boolean circuits is devised. The method employs a direct cut rule combined with deterministic deduction rules. Simplification rules for circuits and a search heuristic attempting to minimize the search space are developed. Experiments in symbolic model checking domain indicate that the method is competitive against state-of-the-art satisfiability checking techniques and a promising basis for further work.

• Type: Conference
• Year: 2000
• Where: CL
• Authors: Tommi A. Junttila, Ilkka Niemelä
• Keywords: Automated Reasoning, Boolean Circuits, Boolean Functions, CL 2000, Satisfiability Checking Techniques