Zadovoljivost jednakosti

Dat je skup od \(n\) jednačina oblika a == b ili a != b. Ispitati da li je taj skup jednačina zadovoljiv ili nije. Skup jednačina je zadovoljiv ukoliko je moguće dodeliti vrednosti promenljivama tako da sve jednačine budu zadovoljene. Ukoliko takva dodela ne postoji, onda je skup jednačina nezadovoljiv.

Opis ulaza

Sa standardnog ulaza se učitava ceo broj \(n\) (\(1 \leq n \leq 350\)), a zatim i \(n\) jednačina oblika <var1> == <var2> ili <var1> != <var2>. Ime promenljive <var> je iz skupa malih slova engleske abecede \(\{a, b, \ldots, z\}\) (\(|\{a, b, \ldots, z\}| = 26\)).

Opis izlaza

Na standardni izlaz ispisati SAT ukoliko je skup jednačina zadovoljiv, inače ispisati UNSAT.

Primer 1

Ulaz

3
a == b
b == c
a != c

Izlaz

UNSAT

Objašnjenje

Iz prve dve jednačine a, b i c moraju uzeti istu vrednost. Tada nije zadovoljena poslednja jednačina a != c.

Primer 2

Ulaz

4
a == b
b == c
a == c
d != e

Izlaz

SAT

Objašnjenje

Iz prve tri jednačine \(a\), \(b\) i \(c\) moraju uzeti istu vrednost. Iz poslednje jednačine \(d\) i \(e\) moraju biti različiti. Zbog toga postoji dodela tako da su sve jednačine zadovoljene. Na primer, to može biti \(a := 1\), \(b := 1\), \(c := 1\), \(d := 2\) i \(e := 3\).

Rešenje

Opis glavnog rešenja

Naivno rešenje problema zadovoljivosti jednakosti bi zahtevalo ispitivanje svih mogućih dodela vrednosti promenljivama, što je eksponencijalne složenosti. Međutim, možemo efikasno rešiti problem koristeći strukturu disjunktnih skupova (Union-Find). Najpre ćemo proći kroz sve jednačine i spojiti promenljive koje su povezane jednakostima (==). Nakon toga, proći ćemo kroz sve jednačine koje izražavaju nejednakosti (!=) i proveriti da li su promenljive koje su povezane nejednakostima u istom skupu. Ako jesu, onda je skup jednačina nezadovoljiv. Ako ni za jednu nejednakost ne postoji takva situacija, onda je skup jednačina zadovoljiv.

Složenost ovog rešenja je linearna u odnosu na broj jednačina, tj. \(O(n)\), ako pretpostavimo da su operacija nad disjunktnim skupovima skoro konstantne složenosti.

#include <iostream>
#include <string>
#include <vector>
#include <tuple>

using namespace std;

#define N (26)

vector<int> parent;
vector<int> rang;

void UF_init(int n) 
{
    parent.resize(n);
    rang.resize(n);

    for (int i = 0; i < n; i++) {
        parent[i] = i;
        rang[i] = 0;
    }
}

int UF_find(int x) 
{
    while (x != parent[x]) {
        parent[x] = parent[parent[x]];
        x = parent[x];
    }

    return x;
}

void UF_union(int x, int y) 
{
    int fx = UF_find(x);
    int fy = UF_find(y);

    if (fx == fy) return;

    if (rang[fx] < rang[fy]) {
        parent[fx] = fy;
    } else if (rang[fy] < rang[fx]) {
        parent[fy] = fx;
    } else {
        parent[fx] = fy;
        rang[fy]++;
    }
}

int main() 
{
    int n; cin >> n;

    vector<tuple<int, char, int>> equations(n);

    for (int i = 0; i < n; i++) {
        char x, y; string op;
        cin >> x >> op >> y;

        if (op == "==") {
            equations[i] = make_tuple(x - 'a', '=', y - 'a');
        } else {
            equations[i] = make_tuple(x - 'a', '!', y - 'a');
        }
    }

    UF_init(N);

    for (int i = 0; i < n; i++) {
        auto [x, op, y] = equations[i];
        if (op == '=') {
            UF_union(x, y);
        }
    }

    for (int i = 0; i < n; i++) {
        auto [x, op, y] = equations[i];
        if (op == '!') {
            auto fx = UF_find(x);
            auto fy = UF_find(y);
            if (fx == fy) {
                cout << "UNSAT" << endl;
                return 0;
            }
        }
    }

    cout << "SAT" << endl;

    return 0;
}