最坏情况下Min-2SAT问题的上界

摘要

最坏情况下MaxSAT问题上界的研究已成为一个热门的研究领域.与MaxSAT问题相对的是MinSAT问题,在求解某些组合优化问题时,将其转化为MinSAT问题比转化为MaxSAT问题有着更快的速度,因此对MinSAT问题进行研究.针对Min-2SAT问题提出算法MinSATAlg,该算法首先利用化简算法Simplify对公式进行化简,然后通过分支树的方法对不同情况的子句进行分支.从子句数目的角度分析算法的时间复杂度并证明Min-2SAT问题可在O(1.134 3m)时间内求解,对于每个变量至多出现在3个2-子句中的情况,得到最坏情况下的上界为O(1.122 5n),其中n为变量的数目.%The rigorous theoretical analyses of algorithms for solving the upper bounds of maximum satisfiability ( MaxSAT) problems have been proposed in research literature. The opposite problem of MaxSAT is the minimum satisfiability (MinSAT) problem. Solving some combinatorial optimization problems by reducing them to MinSAT form may be substantially faster than reducing them to MaxSAT form, so the MinSAT problem was researched in this paper. An algorithm (MinSATAlg) was presented for the minimum two-satisfiability (Min-2SAT) problem. In this paper, first, the simplification algorithm Simplify was used for simplification of formulas. Secondly, the branching tree method was used for branching on different kinds of clauses. It was proven that this algorithm can solve the Min-2SAT problem in 0 (1. 134 3m), regarding the number of clauses as parameters. The upper bound in the worst case was derived as 0(1. 122 5"), where n is the number of variables in an input formula for a particular case of Min-2SAT in which each variable appears in three 2-clauses at most.