| 摘要 |
PROBLEM TO BE SOLVED: To reduce SAT calculation time.SOLUTION: A calculation processing part M assigns a boolean value to a variable x1 included in a Boolean expression that is expressed in a conjunctive normal form, and gives notice of the assigned boolean value to calculation processing parts C1, C2 and Cn that operate the Boolean expression including the variable x1, and then, the calculation processing parts C1, C2 and Cn after receiving the notice of the boolean value store the boolean value in first-level ques cq11, cq21 and cqn1, and calculate each boolean value of other variables included in the Boolean expression, on the basis of the boolean value. Even when any of the calculation processing parts has not finished calculating each boolean value of other variables, the calculation processing part M assigns the boolean value to a variable x3 included in the Boolean expression, and gives notice of the assigned boolean value to the calculation processing parts C1, C2 and Cn that operate the Boolean expression including the variable x3, and then, the calculation processing parts C1, C2 and Cn after receiving the notice of the boolean value store the boolean value in second-level ques cq12, cq22 and cqn2, and calculate each boolean value of other variables included in the Boolean expression, on the basis of the boolean value. |
