软件学报

作者：符祖峰，许道云

单位：符祖峰，贵州大学 计算机科学与技术学院, 贵州 贵阳 550025;安顺学院 电子与信息工程学院, 贵州 安顺 56100011,许道云，贵州大学 计算机科学与技术学院, 贵州 贵阳 55002502

关键词：d-正则(k,s)-CNF公式;SAT问题;NP完全性

基金：国家自然科学基金（61762019，61862051）

研究具有正则结构的SAT问题是否是NP完全问题，具有重要的理论价值.（k，s）-CNF公式类和正则（k，s）-CNF公式类已被证明存在一个临界函数f（k），使得当s ≤ f（k）时，所有实例都可满足；当s ≥ f（k）+1时，对应的SAT问题是NP完全问题.研究具有更强正则约束的d-正则（k，s）-SAT问题，其要求实例中每个变元的正负出现次数之差不超过给定的自然数d.通过设计一种多项式时间的归约方法，证明d-正则（k，s）-SAT问题存在一个临界函数f（k，d），使得当s ≤ f（k，d）时，所有实例都可满足；当s ≥ f（k，d）+1时，d-正则（k，s）-SAT问题是NP完全问题.这种多项式时间的归约变换方法通过添加新的变元和新的子句，可以更改公式的子句约束密度，并约束每个变元正负出现次数的差值.这进一步说明，只用子句约束密度不足以刻画CNF公式结构的特点，对临界函数f（k，d）的研究有助于在更强正则约束条件下构造难解实例.

来源：2020年第4期

《软件学报》期刊编辑部

查看软件学报杂志2020年第4期