zbMATH — the first resource for mathematics

New bounds for MAX-SAT by clause learning. (English) Zbl 1188.68272
Diekert, Volker (ed.) et al., Computer science – theory and applications. Second international symposium on computer science in Russia, CSR 2007, Ekaterinburg, Russia, September 3–7, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-74509-9/pbk). Lecture Notes in Computer Science 4649, 194-204 (2007).
Summary: To solve a problem on a given CNF formula \(F\), a splitting algorithm recursively calls for \(F[v]\) and \(F[\lnot v]\) for a variable \(v\). Obviously, after the first call an algorithm obtains some information on the structure of the formula that can be used in the second call. We use this idea to design new surprisingly simple algorithms for the MAX-SAT problem. Namely, we show that MAX-SAT for formulas with constant clause density can be solved in time \(c ^{n }\), where \(c < 2\) is a constant and \(n\) is the number of variables, and within polynomial space (the only known such algorithm by Dantsin and Wolpert uses exponential space). We also prove that MAX-2-SAT can be solved in time \(2^{m/5.88}\), where \(m\) is the number of clauses (this improves the bound \(2^{m/5.769}\) proved independently by Kneis et al. and by Scott and Sorkin).
For the entire collection see [Zbl 1135.68001].

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68Q25 Analysis of algorithms and problem complexity
68Q32 Computational learning theory
Chaff; MAX-2-SAT; SATO
Full Text: DOI