多文字可满足SAT问题的相变点上界

摘要

可满足(SAT)问题是指:是否存在一组布尔变元赋值,使得随机合取范式(CNF)公式中每个子句至少有1个文字为真。多文字可满足SAT问题是指:是否存在一组布尔变元赋值,使得随机CNF公式中每个子句至少有2个文字为真。此问题仍然是一个NP难问题。定义约束密度α为CNF公式子句数与变元数之比,对该问题的相变点上界α*进行了研究。如果α>α*,则多文字可满足SAT问题高概率不可满足。通过一阶矩一个简单的推断,可以证明α*=-ln 2/ln(1-(k+1)/2 k),当k=3时,α*=1。利用Kirousis等人的局部最大值技术,提升了多文字可满足3-SAT问题的相变点上界α*=0.7193。最后,选择了大量数据进行实验验证,结果表明,理论结果与实验结果相吻合。