Towards an Ecient Tableau Method for
Tommi A. Junttila, Ilkka Niemelä · 2000
Boolean circuits oer a natural, structured, and compact representation of Boolean functions for many application domains. In this paper a tableau method for solving satisability problems for Boolean cir- cuits is devised. The method employs a direct cut rule combined with de- terministic deduction rules. Simplication rules for circuits and a search heuristic attempting to minimize the search space are developed. Ex- periments in symbolic model checking domain indicate that the method is competitive against state-of-the-art satisability checking techniques and a promising basis for further work.