The problem under discussion is to check whether a given combinational network implements a system of incompletely specified Boolean functions. SAT-based procedure is discussed that formulates the overall problem as conventional conjunctive normal form (CNF) on the basis of unary encoding of multiple-output cubes the Boolean functions are specified on and testing whether the combinational network implements them using a SAT-solver. The novel method is proposed that speeds up the SAT-based procedure due to grouping of multiple-output cubes and solving several independent SAT problems.
展开▼
