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

Я попытаюсь сначала формализовать проблему, а затем попытаться свести ее к 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 - некоторая константа, описывающая «конец недели»)

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

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 ¹
Мы будем использовать его, чтобы гарантировать, что интервалы не перекрываются.
Обратите внимание, что если мы хотим убедиться, что (x1, y1) и (x2, y2) не перекрываются, нам нужно:

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

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

y1<= x2 OR y2 <= x1

И используя наши предложения Smaller и boolean:

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}

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

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

Небольшое примечание: эта формула позволяет выбрать более 1 интервала из каждого класса, но если есть решение с некоторыми интервалами 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

А это означает расписание: Algebra = (4,6); Исчисление = (1,4) по желанию.

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