2-SAT

SAT (problema de satisfacibilidad booleana) es el problema de asignar valores booleanos a variables de modo que se satisfaga una fórmula booleana dada. La fórmula booleana suele darse en CNF (forma normal conjuntiva), que es una conjunción de varias cláusulas, donde cada cláusula es una disyunción de literales (variables o negaciones de variables). 2-SAT (2-satisfacibilidad) es una restricción del problema SAT: en 2-SAT cada cláusula tiene exactamente dos literales. Aquí hay un ejemplo de un problema 2-SAT de este tipo. Encontrar una asignación de $a, b, c$ tal que la siguiente fórmula sea verdadera:

$(a \lor \lnot b) \land (\lnot a \lor b) \land (\lnot a \lor \lnot b) \land (a \lor \lnot c)$

SAT es NP-completo; no se conoce una solución eficiente. Sin embargo, 2-SAT se puede resolver de forma eficiente en $O(n + m)$ , donde $n$ es la cantidad de variables y $m$ es la cantidad de cláusulas.

Algoritmo:

Primero hay que convertir el problema a otra forma, la llamada forma normal implicativa. Nótese que la expresión $a \lor b$ es equivalente a $\lnot a \Rightarrow b \land \lnot b \Rightarrow a$ (si una de las dos variables es falsa, entonces la otra debe ser verdadera).

Ahora construimos un grafo dirigido de estas implicaciones: para cada variable $x$ habrá dos vértices $v_x$ y $v_{\lnot x}$ . Las aristas corresponderán a las implicaciones.

Veamos el ejemplo en forma 2-CNF:

$(a \lor \lnot b) \land (\lnot a \lor b) \land (\lnot a \lor \lnot b) \land (a \lor \lnot c)$

El grafo orientado contendrá los siguientes vértices y aristas:

$\begin{array}{cccc} \neg a \Rightarrow \neg b & a \Rightarrow b & a \Rightarrow \neg b & \neg a \Rightarrow \neg c \\ b \Rightarrow a & \neg b \Rightarrow \neg a & b \Rightarrow \neg a & c \Rightarrow a \end{array}$

Se puede ver el grafo de implicaciones en la siguiente imagen:

Vale la pena prestar atención a la propiedad del grafo de implicaciones: si hay una arista $a \Rightarrow b$ , entonces también hay una arista $\lnot b \Rightarrow \lnot a$ .

También nótese que, si $x$ es alcanzable desde $\lnot x$ , y $\lnot x$ es alcanzable desde $x$ , entonces el problema no tiene solución. Cualquier valor que elijamos para la variable $x$ terminará siempre en una contradicción: si a $x$ se le asigna $\text{true}$ , entonces la implicación nos dice que $\lnot x$ también debería ser $\text{true}$ , y viceversa. Resulta que esta condición no solo es necesaria, sino también suficiente. Lo demostraremos en unos párrafos más abajo. Primero recordemos que, si un vértice es alcanzable desde un segundo, y el segundo es alcanzable desde el primero, entonces esos dos vértices están en la misma componente fuertemente conexa. Por lo tanto, podemos formular el criterio de existencia de una solución como sigue:

Para que este problema 2-SAT tenga solución, es necesario y suficiente que, para cualquier variable $x$ , los vértices $x$ y $\lnot x$ estén en componentes fuertemente conexas distintas del grafo de implicaciones.

Este criterio se puede verificar en tiempo $O(n + m)$ hallando todas las componentes fuertemente conexas.

La siguiente imagen muestra todas las componentes fuertemente conexas del ejemplo. Como se puede comprobar fácilmente, ninguna de las cuatro componentes contiene un vértice $x$ y su negación $\lnot x$ ; por lo tanto, el ejemplo tiene solución. En los párrafos siguientes veremos cómo computar una asignación válida, pero solo a modo de demostración se da la solución $a = \text{false}$ , $b = \text{false}$ , $c = \text{false}$ .

Ahora construimos el algoritmo para encontrar la solución del problema 2-SAT bajo el supuesto de que la solución existe.

Nótese que, a pesar de que la solución existe, puede ocurrir que $\lnot x$ sea alcanzable desde $x$ en el grafo de implicaciones, o que (pero no simultáneamente) $x$ sea alcanzable desde $\lnot x$ . En ese caso, la elección de $\text{true}$ o de $\text{false}$ para $x$ conducirá a una contradicción, mientras que la elección de la otra no lo hará. Veamos cómo elegir un valor de modo que no generemos una contradicción.

Ordenemos las componentes fuertemente conexas en orden topológico (es decir, $\text{comp}[v] \le \text{comp}[u]$ si hay un camino de $v$ a $u$ ) y sea $\text{comp}[v]$ el índice de la componente fuertemente conexa a la que pertenece el vértice $v$ . Entonces, si $\text{comp}[x] < \text{comp}[\lnot x]$ asignamos a $x$ el valor $\text{false}$ , y $\text{true}$ en caso contrario.

Demostremos que con esta asignación de las variables no llegamos a una contradicción. Supongamos que a $x$ se le asigna $\text{true}$ . El otro caso se puede demostrar de forma similar.

Primero demostramos que el vértice $x$ no puede alcanzar el vértice $\lnot x$ . Como asignamos $\text{true}$ , tiene que valer que el índice de la componente fuertemente conexa de $x$ es mayor que el índice de la componente de $\lnot x$ . Esto significa que $\lnot x$ está a la izquierda de la componente que contiene a $x$ , y este último vértice no puede alcanzar al primero.

En segundo lugar demostramos que no existe una variable $y$ tal que los vértices $y$ y $\lnot y$ sean ambos alcanzables desde $x$ en el grafo de implicaciones. Esto causaría una contradicción, porque $x = \text{true}$ implica que $y = \text{true}$ y $\lnot y = \text{true}$ . Lo demostramos por contradicción. Supongamos que $y$ y $\lnot y$ son ambos alcanzables desde $x$ ; entonces, por la propiedad del grafo de implicaciones, $\lnot x$ es alcanzable tanto desde $y$ como desde $\lnot y$ . Por transitividad, esto implica que $\lnot x$ es alcanzable desde $x$ , lo cual contradice el supuesto.

Así, hemos construido un algoritmo que encuentra los valores requeridos de las variables bajo el supuesto de que, para cualquier variable $x$ , los vértices $x$ y $\lnot x$ están en componentes fuertemente conexas distintas. Lo anterior demuestra la corrección de este algoritmo. En consecuencia, al mismo tiempo demostramos el criterio de existencia de una solución enunciado arriba.

Implementación:

Ahora podemos implementar el algoritmo completo. Primero construimos el grafo de implicaciones y hallamos todas las componentes fuertemente conexas. Esto se puede lograr con el algoritmo de Kosaraju en tiempo $O(n + m)$ . En el segundo recorrido del grafo, el algoritmo de Kosaraju visita las componentes fuertemente conexas en orden topológico; por lo tanto, es fácil computar $\text{comp}[v]$ para cada vértice $v$ .

Después podemos elegir la asignación de $x$ comparando $\text{comp}[x]$ y $\text{comp}[\lnot x]$ . Si $\text{comp}[x] = \text{comp}[\lnot x]$ devolvemos $\text{false}$ para indicar que no existe una asignación válida que satisfaga el problema 2-SAT.

A continuación está la implementación de la solución del problema 2-SAT para el grafo de implicaciones ya construido $adj$ y el grafo transpuesto $adj^{\intercal}$ (en el que se invierte la dirección de cada arista). En el grafo, los vértices con índices $2k$ y $2k+1$ son los dos vértices correspondientes a la variable $k$ , y $2k+1$ corresponde a la variable negada.


struct TwoSatSolver {
    int n_vars;
    int n_vertices;
    vector<vector<int>> adj, adj_t;
    vector<bool> used;
    vector<int> order, comp;
    vector<bool> assignment;

    TwoSatSolver(int _n_vars) : n_vars(_n_vars), n_vertices(2 * n_vars), adj(n_vertices), adj_t(n_vertices), used(n_vertices), order(), comp(n_vertices, -1), assignment(n_vars) {
        order.reserve(n_vertices);
    }
    void dfs1(int v) {
        used[v] = true;
        for (int u : adj[v]) {
            if (!used[u])
                dfs1(u);
        }
        order.push_back(v);
    }

    void dfs2(int v, int cl) {
        comp[v] = cl;
        for (int u : adj_t[v]) {
            if (comp[u] == -1)
                dfs2(u, cl);
        }
    }

    bool solve_2SAT() {
        order.clear();
        used.assign(n_vertices, false);
        for (int i = 0; i < n_vertices; ++i) {
            if (!used[i])
                dfs1(i);
        }

        comp.assign(n_vertices, -1);
        for (int i = 0, j = 0; i < n_vertices; ++i) {
            int v = order[n_vertices - i - 1];
            if (comp[v] == -1)
                dfs2(v, j++);
        }

        assignment.assign(n_vars, false);
        for (int i = 0; i < n_vertices; i += 2) {
            if (comp[i] == comp[i + 1])
                return false;
            assignment[i / 2] = comp[i] > comp[i + 1];
        }
        return true;
    }

    void add_disjunction(int a, bool na, int b, bool nb) {
        // na y nb indican si a y b deben negarse
        a = 2 * a ^ na;
        b = 2 * b ^ nb;
        int neg_a = a ^ 1;
        int neg_b = b ^ 1;
        adj[neg_a].push_back(b);
        adj[neg_b].push_back(a);
        adj_t[b].push_back(neg_a);
        adj_t[a].push_back(neg_b);
    }

    static void example_usage() {
        TwoSatSolver solver(3); // a, b, c
        solver.add_disjunction(0, false, 1, true);  //     a  v  no b
        solver.add_disjunction(0, true, 1, true);   // no a  v  no b
        solver.add_disjunction(1, false, 2, false); //     b  v      c
        solver.add_disjunction(0, false, 0, false); //     a  v      a
        assert(solver.solve_2SAT() == true);
        auto expected = vector<bool>{{true, false, true}};
        assert(solver.assignment == expected);
    }
};

2-SAT

Algoritmo:

Implementación:

Problemas de práctica