PROGRAM, CONSTRAINT SATISFACTION PROBLEM SOLVING DEVICE AND CONSTRAINT SATISFACTION PROBLEM SOLVING METHOD

摘要

PROBLEM TO BE SOLVED: To quickly determine whether a solution exists or not and to quickly analyze and display a cause by which any solution cannot be obtained.;SOLUTION: A relaxation literal E1 is generated for a hard constraint 1. A relaxation literal E2 is generated for a hard constraint 2. Similarly, a unique relaxation literal is assigned to each hard constraint. A CNF encoder 104 encodes these constraints into CNF clauses. The relaxation literals act on CNF in a CNF clause relaxation unit 108. A SAT solver 105 receives clauses or temporary clauses generated by the CNF encoder 104 and the CNF clause relaxation unit 108 to obtain a satisfaction solution. A relaxation literal minimization unit 106 updates an upper bound or a lower bound and, for next solving, inputs results to the SAT solver as CNF clauses or temporary clauses. If a minimum satisfaction solution minimizing the number of relaxation literal true values can be obtained after repeating this operation, a hard constraint name corresponding to a relaxation literal corresponding to the minimum satisfaction solution is outputted by a cause output unit 107 as a cause of failure in satisfaction.;SELECTED DRAWING: Figure 9;COPYRIGHT: (C)2019,JPO&INPIT