Définitoin du problème SAT

SAT signifie Satisfaisabilité. Le problème k-SAT consiste à déterminer si une formule booléenne composée de m clauses, chacune contenant exactement k littéraux (variables ou leur négation), est satisfaisable. Pour k ≥ 3, il a été prouvé que k-SAT est NP-complet. Cependant, le cas particulier 2-SAT (où chaque clause contient au plus deux littéraux) admet une solution en temps polynomial.

Approche algorithmique pour le 2-SAT

L'idée principale consiste à construire un graphe d'implication. Pour chaque variable booléenne xi, on crée deux nœuds : i représentant xi = VRAI et i + n représentant xi = FAUX. Chaque clause est transformée en implications logiques :

• La clause (a ∨ b) devient (¬a → b) et (¬b → a).
• La clause (a ∧ b) équivaut à (a → b) et (b → a).
• Un littéral forcé a peut être modélisé par l'implication (¬a → a).

On obtient ainsi un graphe orienté. Une solution existe si et seulement si aucune variable xi n'est dans la même composante fortement connexe (CFC) que sa négation ¬xi.

Pour construire une affectation valide, on calcule les CFC avec l'algorithme de Tarjan. Dans le DAG condansé (graphe des CFC), on choisit pour chaque variable la valeur dont le nœud correspondant a un ordre topologique plus élevé. Cela garantit la consistance des implications.

La complexité totale est en O(n + m).

Exemple 1 : Problème modèle 2-SAT

#include <iostream>
#include <vector>
#include <stack>

const int MAX_N = 2000005;

std::vector<int> adj[MAX_N];
int low[MAX_N], disc[MAX_N], comp_id[MAX_N];
bool on_stack[MAX_N];
std::stack<int> stk;
int timer = 0, num_comp = 0;

void tarjan(int u) {
    low[u] = disc[u] = ++timer;
    stk.push(u);
    on_stack[u] = true;
    for (int v : adj[u]) {
        if (!disc[v]) {
            tarjan(v);
            low[u] = std::min(low[u], low[v]);
        } else if (on_stack[v]) {
            low[u] = std::min(low[u], disc[v]);
        }
    }
    if (low[u] == disc[u]) {
        num_comp++;
        int w;
        do {
            w = stk.top();
            stk.pop();
            on_stack[w] = false;
            comp_id[w] = num_comp;
        } while (w != u);
    }
}

int main() {
    int n_vars, n_clauses;
    std::cin >> n_vars >> n_clauses;
    for (int i = 0; i < n_clauses; i++) {
        int a, b, va, vb;
        std::cin >> a >> va >> b >> vb;
        // a XOR va = 1 signifie ¬a si va=0, a si va=1
        int from_a = a + (1 - va) * n_vars;
        int to_b = b + vb * n_vars;
        int from_b = b + (1 - vb) * n_vars;
        int to_a = a + va * n_vars;
        adj[from_a].push_back(to_b);
        adj[from_b].push_back(to_a);
    }
    for (int i = 1; i <= 2 * n_vars; i++) {
        if (!disc[i]) tarjan(i);
    }
    for (int i = 1; i <= n_vars; i++) {
        if (comp_id[i] == comp_id[i + n_vars]) {
            std::cout << "IMPOSSIBLE\n";
            return 0;
        }
    }
    std::cout << "POSSIBLE\n";
    for (int i = 1; i <= n_vars; i++) {
        std::cout << (comp_id[i] > comp_id[i + n_vars] ? '1' : '0') << " ";
    }
    std::cout << '\n';
    return 0;
}

Exemple 2 : Problème du banquet complet (满汉全席)

#include <iostream>
#include <vector>
#include <stack>
#include <cstring>

const int MAXN = 405;

std::vector<int> graph[MAXN];
int low[MAXN], dft[MAXN], comp[MAXN];
bool in_stack[MAXN];
std::stack<int> s;
int timer, comp_cnt;

void dfs(int u) {
    low[u] = dft[u] = ++timer;
    s.push(u);
    in_stack[u] = true;
    for (int v : graph[u]) {
        if (!dft[v]) {
            dfs(v);
            low[u] = std::min(low[u], low[v]);
        } else if (in_stack[v]) {
            low[u] = std::min(low[u], dft[v]);
        }
    }
    if (low[u] == dft[u]) {
        comp_cnt++;
        int w;
        do {
            w = s.top();
            s.pop();
            in_stack[w] = false;
            comp[w] = comp_cnt;
        } while (w != u);
    }
}

void solve() {
    int n, m;
    std::cin >> n >> m;
    for (int i = 0; i <= 2 * n; i++) graph[i].clear();
    std::memset(dft, 0, sizeof(dft));
    timer = comp_cnt = 0;
    while (!s.empty()) s.pop();

    for (int i = 0; i < m; i++) {
        int a, b;
        char ca, cb;
        std::cin >> a >> ca >> b >> cb;
        int from_a = (ca == 'h') ? a + n : a;
        int to_b = (cb == 'h') ? b + n : b;
        int from_b = (cb == 'h') ? b : b + n;
        int to_a = (ca == 'h') ? a : a + n;
        graph[from_a].push_back(to_b);
        graph[from_b].push_back(to_a);
    }
    for (int i = 1; i <= 2 * n; i++) {
        if (!dft[i]) dfs(i);
    }
    for (int i = 1; i <= n; i++) {
        if (comp[i] == comp[i + n]) {
            std::cout << "BAD\n";
            return;
        }
    }
    std::cout << "GOOD\n";
}

int main() {
    int T;
    std::cin >> T;
    while (T--) solve();
    return 0;
}

Exemple 3 : Problème du jeu (游戏)

#include <iostream>
#include <vector>
#include <cstring>

const int MAXN = 50005;

int n, m, d;
std::string base_config;
std::vector<int> var_options; // Variables avec configuration 'x'
std::vector<std::tuple<int, char, int, char>> constraints;

std::vector<int> adj[2 * MAXN];
int low[2 * MAXN], disc[2 * MAXN], comp[2 * MAXN];
bool in_stack[2 * MAXN];
std::vector<int> stack;
int timer, comp_cnt;

void tarjan(int u) {
    low[u] = disc[u] = ++timer;
    stack.push_back(u);
    in_stack[u] = true;
    for (int v : adj[u]) {
        if (!disc[v]) {
            tarjan(v);
            low[u] = std::min(low[u], low[v]);
        } else if (in_stack[v]) {
            low[u] = std::min(low[u], disc[v]);
        }
    }
    if (low[u] == disc[u]) {
        comp_cnt++;
        int w;
        do {
            w = stack.back();
            stack.pop_back();
            in_stack[w] = false;
            comp[w] = comp_cnt;
        } while (w != u);
    }
}

bool check() {
    for (int i = 0; i <= 2 * n; i++) {
        adj[i].clear();
        disc[i] = low[i] = 0;
    }
    stack.clear();
    timer = comp_cnt = 0;
    std::memset(in_stack, 0, sizeof(in_stack));

    for (auto [a, ca, b, cb] : constraints) {
        if (base_config[a-1] == ca) continue;
        if (base_config[b-1] == cb) {
            // Forcer ¬a
            int node_a = (ca == 'c') ? a + n : a;
            adj[node_a].push_back((ca == 'c') ? a : a + n);
            continue;
        }
        int from_a = (ca == 'c') ? a + n : a;
        int to_b = (cb == 'c') ? b + n : b;
        int from_b = (cb == 'c') ? b : b + n;
        int to_a = (ca == 'c') ? a : a + n;
        adj[from_a].push_back(to_b);
        adj[from_b].push_back(to_a);
    }

    for (int i = 1; i <= 2 * n; i++) {
        if (!disc[i]) tarjan(i);
    }
    for (int i = 1; i <= n; i++) {
        if (comp[i] == comp[i + n]) return false;
    }
    // Construire solution
    for (int i = 1; i <= n; i++) {
        char chosen = (comp[i] < comp[i + n]) ? 'A' : 'B';
        if (base_config[i-1] == 'c') chosen = 'B';
        else if (base_config[i-1] == 'b') chosen = 'A';
        else chosen = (chosen == 'A') ? 'b' : 'c';
        std::cout << chosen;
    }
    std::cout << '\n';
    return true;
}

void search(int idx) {
    if (idx == var_options.size()) {
        if (check()) exit(0);
        return;
    }
    int pos = var_options[idx];
    base_config[pos-1] = 'a';
    search(idx + 1);
    base_config[pos-1] = 'b';
    search(idx + 1);
}

int main() {
    std::cin >> n >> d >> base_config >> m;
    for (int i = 0; i < n; i++) {
        if (base_config[i] == 'x') var_options.push_back(i+1);
    }
    for (int i = 0; i < m; i++) {
        int a, b;
        char ca, cb;
        std::cin >> a >> ca >> b >> cb;
        constraints.emplace_back(a, ca, b, cb);
    }
    search(0);
    std::cout << "-1\n";
    return 0;
}