DEVICE AND METHOD FOR DECIDING SATISFIABILITY OF LOGICAL EXPRESSION

摘要

PROBLEM TO BE SOLVED: To provide the device and method for deciding the satisfiability of the logical expression which can solve the satisfiability decision problem of the logical expression fast by performing a process A and a process B fast. SOLUTION: Element circuits 3 are arranged in a two-dimensional array consisting of variables 1 in the row direction and sum terms 2 in the column direction, the element circuits 3, sum term property circuits 4, and a tantologous and valid/invalid circuit 5 are used to perform the process A for simplifying the logical expression according to values assigned to subsets of a variable set and then deciding whether the simplified logical expression is 1 or 0. Then the element circuits 3, sum term property circuits 4, variable property circuits 6, and a variable selecting circuit 7 are used to perform the process B for selecting a variable to be assigned next from a variable set to which a value is not assigned yet according to the properties of the simplified logical expression unless the simplified logical expression is 1 or 0. Then the function of the element circuits 3 can be changed according to a sum product type logical expression given as a problem.