| 摘要 |
PROBLEM TO BE SOLVED: To provide an improved method for image and pre-image calculation method, and an improved method for pruning search domains. SOLUTION: The method to practice image and pre-image calculation about system contains a step that expresses a system by finite state model, a step that indicates state set with bisection decision graph (BDD) and a step that practices a search algorithm based on satisfiability test(SAT). For that the SAT divides a search of whole solution space into sub-problems, and enumerates plural solutions existing in said solution space for raveling each sub problem, an image calculation based on BDD is used. And, a method for pruning search domains in a procedure of SAT contains a step that uses a constraints of BDD for implicit logical sum or logical product in a set of given BDD, a step that contains search domains in a case where variable allocation for segment satisfys implicit logical sum or logical product and a step that practices back tracking in a case where variable allocation for segment does not satisfy implicit logical sum or logical product.
|
