Принцип разделения знаков для задачи пропозициональной выполнимости

В 1980 г. Мониен и Шпекенмейер и (независимо) Данцин, доказали, что выполнимость пропозициональной формулы в КНФ может быть проверена менее, чем за $2^N$ шагов (где $N$ – число переменных). Позднее было получено большое число других верхних оценок для задачи пропозициональной выполнимости и ее подзадач. Говорят, что формула в КНФ находится в КНФ-($1,\infty$), если каждый положительный литерал входит в неё не более одного раза. Формулы КНФ-($1,\infty$) были впервые изучены Г. Люкхардтом в 1984 году. В этой статье доказывается ряд новых верхних оценок для задачи выполнимости формул в КНФ-($1,\infty$). Для этого вводится новый принцип разделения знаков. Приводятся использующие его алгоритмы, работающие время порядка $1.1939^K$ и $1.0644^L$ соответственно (где $K$ – число дизъюнкций в формуле, $L$ – ее длина), а также алгоритм для формул в КНФ-($1,\infty$), дизъюнкции которых ограничены по длине. Библ. – 14 назв.