Sciweavers

Share
CL
2000
Springer

Towards an Efficient Tableau Method for Boolean Circuit Satisfiability Checking

8 years 12 months ago
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.
Tommi A. Junttila, Ilkka Niemelä
Added 24 Aug 2010
Updated 24 Aug 2010
Type Conference
Year 2000
Where CL
Authors Tommi A. Junttila, Ilkka Niemelä
Comments (0)
books