MULTIVALUED CNF DATA STRUCTURE AND MULTIVALUED CNF CONFIGURATION PROGRAM

摘要

PROBLEM TO BE SOLVED: To solve such problems that, though a difficulty level of a satisfiability (SAT) problem is changed according to a structure of a formula to be an object, there is no method for stably constituting an SAT of high difficulty level, and that values that the SAT deals with are true and false, binary values, and there is no CNF (Conjunctive Normal Form) SAT dealing with multi-valued variables such as ternary values or more.;SOLUTION: A multivalued CNF that is constrained such that variables behave like multivalued variables is configured.;COPYRIGHT: (C)2012,JPO&INPIT