HIGH-SPEED DECISION DEVICE FOR SATISFIABILITY DECISION PROBLEM

摘要

PURPOSE:To efficiently find a solution fast by classifying the satisfiability decision problem having various properties into three kinds of 1CNF, 2CNF, and nCNF (N=3) as to the high-speed decision device which decides the satisfiability decision problem at a high speed. CONSTITUTION:This device is equipped with a CNF analysis part 2 which analyzes the satisfiability decision problems represented as AND of plural given sum terms and classifies it into 1CNF where there is variable in a sum term, 2CNF where there are two variables in sum terms, and nCNF where the number of variables in the sum terms is larger than 3, a 1CNF process part 3 which determines the value of the variable of the classified 1CNF, a 2CNF process part 4 which determines the values of the variables of the classified 2CNF, and an nCNF process part 5 which determines the values of the variables of the determined nCNF. Then it is decided that there is a solution when the values of the variables to be supplemented are found by those 1CNF process part 3, 2CNF process part 4, and nCNF process part 5.