Классовое планирование для булевой выполнимости [Полиномиальное сокращение времени]

У меня есть теоретическая/практическая проблема, и я пока не знаю, как это сделать. Вот она:

Я создаю SAT solver, способный найти модель, когда она существует, и доказать противоречие, если это не так на CNF проблемы на C с использованием генетических алгоритмов.

SAT-проблема выглядит в основном такой проблемой: enter image description here Моя цель - использовать этот решатель для поиска решений во множестве различных NP-завершает проблемы. В основном, я переводил различные проблемы в SAT, решает SAT с моим решателем, а затем преобразовываю решение в решение, приемлемое для исходной проблемы.

Мне уже удалось выполнить N * N Sudoku, а также проблемы N-queens, но вот моя новая цель: уменьшить проблему планирования классов до SAT, но я понятия не имею, как формализовать задачу планирования класса для упорядочения чтобы легко преобразовать его в SAT после.

Цель состоит в том, чтобы через несколько месяцев создать график расписания, подобный этому:

enter image description here

Я нашел этот исходный код, который может решить расписание классов, но без каких-либо сокращений к SAT, к сожалению:/

Я также нашел некоторые статьи о планировании вообще (http://www.cs.rochester.edu/users/faculty/kautz/papers/kautz-satplan06.pdf, например).

Но планирование языка определения домена, используемый в этой статье, кажется слишком общим для меня, чтобы представлять проблему планирования класса.:/

Есть ли у кого-то идея о том, как эффективно формализовать планирование классов, чтобы уменьшить его до SAT и после, преобразовать решение SAT (если оно существует ^^) в расписание классов?

Я в принципе открыт для любых предложений, я пока не знаю, как представить, как уменьшить проблему, как преобразовать SAT-решение в расписание...

Следующий вопрос: Расписание классов для булевой выполнимости [Часть 2].

Ответы

Ответ 1

Я попытаюсь сначала формализовать проблему, а затем попытаюсь свести ее к SAT.

Определите задачу планирования класса как:

Input = { S1,S2,....,Sn | Si = {(x_i1, y_i1), (x_i2, y_i2) , ... , (x_ik, y_ik) | 0 <= x_ij < y_ij <= M } }

Неформально: ввод представляет собой набор классов, каждый класс представляет собой набор (открытых) интервалов в виде (x, y)
(M - некоторая константа, которая описывает "конец недели" )

Вывод: True тогда и только тогда, когда существует некоторый набор:

R = { (x_1j1, y_1j1) , ..., (x_njn, y_njn) | for each a,b: (x_aja,y_aja) INTERSECTION (x_bjb,y_bjb) = {} }

Неформально: истинно тогда и только тогда, когда существует некоторое распределение интервалов, так что пересечение каждой пары интервалов пусто.

Сокращение до SAT:

Определить логическую переменную для каждого интервала, V_ij На основании этого определим формулу:

F1 = (V_11 OR V_12 OR ... OR V_1(k_1)) AND .... AND (V_n1 OR V_n2 OR ... OR V_n(k_n))

Неформально F1 выполняется тогда и только тогда, когда "по крайней мере один из интервалов для каждого класса" удовлетворен "

Определите Smaller(x,y) = true, если и только if x <= y 1
Мы будем использовать его, чтобы гарантировать, что интервалы не перекрываются.
Обратите внимание: если мы хотим убедиться, что (x1, y1) и (x2, y2) не перекрываются, нам нужно:

x1 <= y1 <= x2 <= y2 OR  x2 <= y2 <= x1 <= y1

Так как вход гарантирует x1<=y1, x2<=y2, он сводится к:

y1<= x2 OR y2 <= x1

И используя наши Меньшие и булевские предложения:

Smaller(y1,x2) OR Smaller(y2,x1)

Теперь давайте определим новые предложения для обработки с ним:

Для каждой пары классов a, b и интервалов c, d в них (c в a, d в b)

G_{c,d} = (Not(V_ac) OR Not(V_bd) OR Smaller(y_ac,x_bd) OR Smaller(y_bd,x_ac))

Неформально, если один из интервалов b или d не используется - предложение выполняется, и мы закончили. В противном случае оба используются, и мы должны обеспечить, чтобы между этими двумя интервалами не было перекрытия.
Это гарантирует, что если оба c, d "выбраны" - они не перекрываются, и это верно для каждой пары интервалов.

Теперь сформулируем нашу окончательную формулу:

F = F1 AND {G_{c,d} | for each c,d}

Эта формула гарантирует нам:

  • Для каждого класса выбирается хотя бы один интервал
  • Для каждого из двух интервалов c, d - если выбраны оба c и d, они не перекрываются.

Небольшое примечание: эта формула позволяет выбрать более одного интервала из каждого класса, но если есть решение с некоторыми t > 1 интервалами, вы можете легко удалить t-1 из них без изменения правильности решения.

В конце выбранные интервалы являются определяемыми нами булевыми переменными V_ij.

Пример:

Alebgra = {(1,3),(3,5),(4,6)} Calculus = {(1,4),(2,5)}

Определите F:

F1 = (V1,1 OR V1,2 OR V1,3) AND (V2,1 OR V2,2)

Определите G:

G{A1,C1} = Not(V1,1) OR Not(V2,1) OR  4 <= 1 OR 3 <= 1 //clause for A(1,3) C(1,4)
         = Not(V1,1) OR Not(V2,1) OR false = 
         = Not(V1,1) OR Not(V2,1)
G{A1,C2} = Not(V1,1) OR Not(V2,2) OR  3 <= 2 OR 5 <= 1 // clause for A(1,3) C(2,5)
         = Not(V1,1) OR Not(V2,2) OR false = 
         = Not(V1,1) OR Not(V2,2)
G{A2,C1} = Not(V1,2) OR Not(V2,1) OR  5 <= 1 OR 4 <= 3 //clause for A(3,5) C(1,4)
         = Not(V1,2) OR Not(V2,1) OR false = 
         = Not(V1,2) OR Not(V2,1)
G{A2,C2} = Not(V1,2) OR Not(V2,2) OR  5 <= 2 OR 5 <= 3 // clause for A(3,5) C(2,5)
         = Not(V1,2) OR Not(V2,2) OR false = 
         = Not(V1,2) OR Not(V2,2)
G{A3,C1} = Not(V1,3) OR Not(V2,1) OR  4 <= 4 OR 6 <= 1 //clause for A(4,6) C(1,4)
         = Not(V1,3) OR Not(V2,1) OR true= 
         = true
G{A3,C2} = Not(V1,3) OR Not(V2,2) OR  6 <= 2 OR 5 <= 4 // clause for A(4,6) C(2,5)
         = Not(V1,3) OR Not(V2,2) OR false = 
         = Not(V1,3) OR Not(V2,2)

Теперь мы можем показать нашу окончательную формулу:

    F = (V1,1 OR V1,2 OR V1,3) AND (V2,1 OR V2,2) 
        AND  Not(V1,1) OR Not(V2,1) AND Not(V1,1) OR Not(V2,2)
        AND  Not(V1,2) OR Not(V2,1) AND Not(V1,2) OR Not(V2,2)
        AND  true AND Not(V1,3) OR Not(V2,2)

Вышесказанное выполняется только тогда, когда:

V1,1 = false
V1,2 = false
V1,3 = true
V2,1 = true
V2,2 = false

И это означает расписание: Алгебра = (4,6); Исчисление = (1,4), если требуется.

(1) можно легко вычислить как константу в формуле, существует многочленное число таких констант.