Don't-Care Computation using k-clause Approximation

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 express- ible 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 infor- mation in cases where earlier approaches are pro- hibitively costly.