Program, constraint satisfaction problem solving device, constraint satisfaction problem solving method

摘要

To rapidly judge the existence / nonexistence of a solution and causes why a solution can not be obtained at high speed and display it.A relaxation literal E 1 is generated for a hard constraint 1. Relaxation literal E 2 is generated for hard constraint 2. Likewise, relaxation literals specific to each hard constraint are allocated. The CNF encoder 104 encodes these constraints into CNF clauses. The relaxation literal acts on the CNF at the CNF section relaxation section 108. The SAT solver 105 obtains a satisfying solution by inputting a node or provisional clause generated by the CNF encoder 104 and the CNF clause relaxing unit 108. Relaxation literal minimizer 106 updates the upper bound or lower bound and inputs it as a CNF clause or provisional clause to the SAT solver for next solution. After this operation is repeated, if the minimum satisfiable solution that minimizes the relaxation literal true value number is obtained, the hard constraint name corresponding to the relaxation literal corresponding to the minimum satisfied solution is judged to be a reason for not satisfying in the cause output unit 107 Output.(FIG.