Don’t-Care Computation using k-clause Approximation
Kenneth L. McMillan · 2005
Computation of the satisfiability and observability care sets for a sub-circuit in a Boolean network is essentially a problem of quantifier elimination in propositional logic. In this paper, we introduce a method of approximate quantifier elimination that computes the strongest over-approximation expressible using clauses of a given length. The method uses a Boolean satisfiability solver in a machine-learning framework. Experiments using the SIS system show that the method can produce useful care set information in cases where earlier approaches are prohibitively costly.