A new data structure for sat-based static learning with impact on test generation

摘要

In this paper we analyze learning techniques based on the Boolean satisfiability method and find that static indirect A-implications and the super gate extraction approach are useful for increasing the precision of low complexity learning procedures. We propose a new data structure for the complete implication graph that allows efficient processing of the static indirect A-implications. We show that by deriving and performing the static indirect A-implications, some hard-to-detect static indirect implications can be easily found during static learning. In addition, the static indirect A-implications can be used to perform (without spare operations) some dynamic indirect implications during branch and bound search and dynamic learning. In this way, the new data structure of the complete implication graph increases efficiency and precision of both static and dynamic learning as well as branch and bound search. We utilize this data structure in development of an implicit static learning procedure. Experimental results for static learning and redundancy identification confirm their efficiency and precision. Further experimental work shows a positive impact of low complexity static learning on the efficiency and robustness of even combinatorial test generation. We expect that the contribution of the new data structure will be more visible when the super gate extraction approach is also implemented.