20. Primena SAT rešavača u rešavanju CSP problema nad konačnim domenima. Pseudo-Bulovska ograničenja i ograničenja kardinalnosti. Linearna ograničenja.

Šta je CSP problem?

Problem sa promenljivama, njihovim domenima i ograničenjima. Traži se dodela vrednosti koja zadovoljava sva ograničenja.

Kako SAT rešavač rešava CSP problem?

Promenljive i ograničenja CSP problema kodiraju se iskaznom formulom u KNF, a zatim se koristi SAT rešavač.

Kako se kodira promenljiva x sa domenom {1, 2, 3}?

Uvode se Bulovske promenljive x₁, x₂ i x₃, gde xᵢ znači da x ima vrednost i.

Kako se izražava da promenljiva ima bar jednu vrednost?

Disjunkcijom svih mogućih vrednosti, npr. x₁ ∨ x₂ ∨ x₃.

Kako se izražava da promenljiva ima najviše jednu vrednost?

Za svaki par različitih vrednosti dodaje se ¬xᵢ ∨ ¬xⱼ.

Šta su pseudo-Bulovska ograničenja?

Linearne nejednakosti ili jednakosti nad Bulovskim promenljivama, npr. 2x + 3y ≤ 4.

Šta su ograničenja kardinalnosti?

Ograničenja broja tačnih literala: najmanje k, najviše k ili tačno k.

Kako se linearna ograničenja rešavaju SAT rešavačem?

Kodiraju se pomoću Bulovskih promenljivih i klauza, po potrebi uz pomoćne promenljive.

Mini-zadatak: Kako zapisati da najviše jedna od p i q može biti tačna?

¬p ∨ ¬q. Ekvivalentno pseudo-Bulovsko ograničenje je p + q ≤ 1.