一种产生可满足性难解实例的模型

A model to generate hard satisfiable instances

在d-k-CSP模型的基础上,给出了产生可满足性难解实例的两种方法。利用概率论分析了d-k-CSP模型在这两种方法下解的平均个数和解的分布情况,并用数值实验对两种方法产生的可满足性实例的求解难度进行了对比分析。结果表明:强迫有解实例和非强迫有解实例的求解难度相当,但产生强迫有解实例的方法更简单有效。

Based on the model d-k-CSP,two methods for generating hard satisfiable instances are proposed.The expected number of solutions and distribution of solutions with respect to the two methods under model d-k-CSP are analyzed by the probability theory,and a series of experimental studies are carried out to analyze the hardness of satisfiable instances generated by the two methods.The results show that the forced and unforced satisfiable instances have a similar hardness,but the method for the generating forced satisfiable instances is easier than that for generating unforced satisfiable instances.