Klasa Scheduling do logicznego spełnialności [redukcja Wielomian-time]

Question

mam pewne teoretyczne i praktyczne problemy/Nie mam pojęcia, na razie, w jaki sposób zarządzać Oto ona:

tworzę SAT solver stanie znaleźć model, gdy istnieje, i udowodnienie sprzeczności, gdy nie jest tak w przypadku problemów z C za pomocą algorytmów genetycznych.

SAT-Problem wygląda w zasadzie jak tego rodzaju problemu: Moim celem jest, aby korzystać z tej solver do znalezienia rozwiązania w wielu różnych NP-completes problemów. Zasadniczo tłumaczę różne problemy na SAT, rozwiązuję SAT z moim solver, a następnie przekształcam roztwór w rozwiązanie akceptowalne dla pierwotnego problemu.

Udało mi się już rozwiązać problem N * N Sudoku i N-queens, ale oto mój nowy cel: zredukować problem z planowaniem zajęć do SAT, ale nie mam pojęcia, jak sformalizować problem z planowaniem zajęć w aby łatwo przekształcić go w SAT po.

Celem jest oczywiście, w ciągu kilku miesięcy, aby wygenerować obraz harmonogramu jak ten:

Znalazłem source-code który jest w stanie rozwiązać ten klasy harmonogram ale bez redukcji do SAT niestety:/

Znalazłem również kilka artykułów na temat planowania w ogóle (na przykład http://www.cs.rochester.edu/users/faculty/kautz/papers/kautz-satplan06.pdf).

Używane w tym artykule planning domain definition language wydaje się jednak zbyt ogólne, aby mogło stanowić problem z szeregowaniem klas. :/

Czy ktoś ma pomysł, jak efektywnie sformalizować harmonogramowanie klasy, aby zredukować go do SAT i późniejszego, przekształcić rozwiązanie SAT (jeśli istnieje^^) w harmonogram klas?

zasadzie jestem otwarty na wszelkie propozycje, ja na razie nie mam pojęcia, w jaki sposób przedstawia, jak zmniejszyć ten problem, w jaki sposób przekształcić SAT-roztwór do harmonogramu ...

---

Kolejne pytanie: Class Scheduling to Boolean satisfiability [Polynomial-time reduction] part 2

Answer 1

Mam zamiar najpierw sformalizować problem, a następnie próbować zmniejszyć go do SAT.

Definiowanie problemu klasy szeregowania jako:

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

nieformalnie: Wejście to zestaw grup, każda grupa jest zestaw (otwarte) odstępach, w postaci (x, y)
(M pewne stałe, które opisuje „koniec tygodnia”)

Wyjście: true wtedy i tylko wtedy, gdy istnieje pewien zestaw:

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

Nieformalnie: wartość prawda, wtedy i tylko wtedy, gdy istnieje przyporządkowanie przedziałów tak, że przecięcie między każdą parą przedziałów jest puste.

---

Redukcja do SAT:

Zdefiniuj zmienną logiczną dla każdego przedziału, V_ij
W oparciu o nią, określić wzór:

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)) 

nieformalnie, F1 jest spełniony wtedy i tylko jeśli przynajmniej jeden z przedziałów dla każdej klasy jest "spełniony"

Zdefiniuj Smaller(x,y) = true tylko i wyłącznie if x <= y
Użyjemy go, aby upewnić się, że odstępy nie zachodzą na siebie.
Należy pamiętać, że jeśli chcemy, aby upewnić się (X1, Y1) i (X2, Y2) nie pokrywają się, musimy:

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

Ponieważ wejście gwarantuje x1<=y1, x2<=y2, to sprowadza się do:

y1<= x2 OR y2 <= x1 

i korzystania nasi mniejsi oraz logiczne klauzule:

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

a teraz definiować nowe klauzule do obsługi z nim:

Dla każdej pary grup a, b, a przedziały C, D w nich (C na A, D w punkcie b)

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

nieformalnie, jeśli jeden z przedziałów B i D nie jest używana - klauzuli jest zadowolony i skończymy. W przeciwnym razie, oba są używane, i musimy zapewnić, że nie ma nakładania się między tymi dwoma interwałami.
Gwarantuje to, że jeśli oba c, d są "wybrane" - nie zachodzą na siebie i jest to prawdą dla każdej pary przedziałów.

teraz z naszej końcowego wzoru:

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

Ten wzór zapewnia nas:

1. dla każdej klasy, a przynajmniej jeden przedział dobiera się
2. Dla każdego z dwóch przedziałach C, D - jeśli wybrane są zarówno c jak i d, nie nakładają się one.

Mała uwaga: Ta formuła pozwala wybrać więcej niż 1 interwał z każdej klasy, ale jeśli istnieje rozwiązanie z niektórymi interwałami t> 1, można łatwo usunąć t-1 z nich bez zmiany poprawności rozwiązania .

Na koniec wybranymi interwałami są zmienne binarne V_ij, które zdefiniowaliśmy.

---

przykład:

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

zdefiniować F:

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

zdefiniować 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) 

Teraz można pokazać nasze końcowego wzoru:

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) 

Powyższe jest spełnione, gdy:

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

A oznaczającym harmonogramie: Algebra = (4,6); Calculus = (1,4), zgodnie z potrzebami.

---

(1) można łatwo obliczyć jako stałą do formuły, istnieje wielomianowa liczba takich stałych.