Linear 3SAT: версия 3SAT в линейном времени

Это относительно простая задача динамического программирования. Я опишу решение, не обращая внимания на довольно простые проблемы индексации вокруг любой границы.

После m-го шага у нас есть набор возможных значений переменных (m-10, m-9, ..., m+10), которые до сих пор могли быть решениями, каждое из которых связано с набором значений для всех предыдущих переменных. что приводит к решениям уравнений 1..m.

Для m+1-го шага мы берем каждый член этого набора возможных решений, игнорируем m-10-е значение и рассматриваем каждую возможность для m+11-го значения. Если m+1-е уравнение истинно, мы добавляем его к следующему набору решений, указывая на нашу историю, только если этот шаблон решения еще не был добавлен.

Это подготавливает нас к m+2-му шагу.

Требуется n шагов, на каждом из которых может быть рассмотрено около 2 миллионов возможных случаев, так что это линейно.

(Забавная задача. Измените этот алгоритм так, чтобы он не просто находил решение, а подсчитывал количество возможных решений.)

Я думаю, что вы можете просто использовать брутфорс в полигоне. Разделите список предложений на две части. Исчерпывающий поиск по переменным, которые находятся по обе стороны от разделения. Их не более 30, так что 2 ^ 30 = O (1) настроек, которые нужно попробовать. Как только эти переменные установлены, вы можете рекурсивно решать обе стороны, каждая из которых является независимым экземпляром SAT с n/2 переменными.