To solve a problem on a given CNF formula F a splitting algorithm recursively calls for F[v] and F[¬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 2m/5.88, where m is the number of clauses (this improves the bound 2m/5,769 proved independently by Kneis et al. and by Scott and Sorkin).

Язык оригиналаанглийский
Название основной публикацииComputer Science - Theory and Applications - Second International Symposium on Computer Science in Russia, CSR 2007, Proceedings
Страницы194-204
Число страниц11
СостояниеОпубликовано - 24 дек 2007
Событие2nd International Symposium on Computer Science in Russia, CSR 2007 - Ekaterinburg, Российская Федерация
Продолжительность: 3 сен 20077 сен 2007

Серия публикаций

НазваниеLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Том4649 LNCS
ISSN (печатное издание)0302-9743
ISSN (электронное издание)1611-3349

конференция

конференция2nd International Symposium on Computer Science in Russia, CSR 2007
Страна/TерриторияРоссийская Федерация
ГородEkaterinburg
Период3/09/077/09/07

    Предметные области Scopus

  • Теоретические компьютерные науки
  • Компьютерные науки (все)

ID: 49825111