A new upper bound for Max-2-SAT: A graph-theoretic approach. (English) Zbl 1173.68539

Raible, Daniel; Fernau, Henning

Ochmański, Edward (ed.) et al., Mathematical foundations of computer science 2008. 33rd international symposium, MFCS 2008, Toruń Poland, August 25–29, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-85237-7/pbk). Lecture Notes in Computer Science 5162, 551-562 (2008).

Summary: In MaxSat, we ask for an assignment which satisfies the maximum number of clauses for a Boolean formula in CNF. We present an algorithm yielding a run-time upper bound of \({\mathcal{O}}^*({2^{\frac{K}{6.2158}}})\) for Max-2-Sat (each clause contains at most 2 literals), where \(K\) is the number of clauses. The run-time has been achieved by using heuristic priorities on the choice of the variable on which we branch. The implementation of these heuristic priorities is rather simple, though they have a significant effect on the run-time. Also the analysis uses a nonstandard measure.
For the entire collection see [Zbl 1154.68021].

MSC:

68Q25	Analysis of algorithms and problem complexity
68T20	Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Software:

MAX-2-SAT