Two-Satisfiability
(graph/two_sat.hpp)

View this file on GitHub
Last update: 2026-06-21 02:34:20+09:00
Include: #include "graph/two_sat.hpp"

Overview

m1une::graph::TwoSat solves boolean formulas whose clauses contain at most two literals. It converts every clause to implications and checks strongly connected components.

The implementation stores implications in a flat edge list and builds compact CSR graphs when solving. Both SCC passes are iterative, so large formulas do not depend on the process recursion limit.

Literal Convention

The expression:

add_clause(i, f, j, g)

adds the clause:

(variable i == f) OR (variable j == g)

For example, add_clause(0, true, 1, false) means $x_0 \lor \lnot x_1$.

Construction

TwoSat(): creates a formula with zero variables.
TwoSat(int n): creates a formula with variables 0 through n - 1.

Methods

Method	Description	Complexity
`int size()`	Returns the number of variables.	$O(1)$
`bool empty()`	Returns whether there are no variables.	$O(1)$
`void reserve(size_t clauses)`	Reserves implication-edge storage for approximately `clauses` ordinary clauses.	$O(M)$
`void add_clause(i, f, j, g)`	Adds `(x_i == f) OR (x_j == g)`.	Amortized $O(1)$
`void add_implication(i, f, j, g)`	Adds `(x_i == f) => (x_j == g)`.	Amortized $O(1)$
`void set_value(i, value)`	Forces `x_i` to equal `value`.	Amortized $O(1)$
`void add_equal(i, j)`	Forces `x_i == x_j`.	Amortized $O(1)$
`void add_not_equal(i, j)`	Forces `x_i != x_j`.	Amortized $O(1)$
`bool satisfiable()`	Solves the current formula and returns whether an assignment exists.	$O(N + M)$
`const vector<bool>& answer()`	Returns one satisfying assignment. Call only after a successful `satisfiable()`.	$O(1)$
`bool value(int i)`	Returns the assigned value of variable `i`.	$O(1)$

Here $M$ is the number of implication edges, which is twice the number of ordinary clauses. Calling satisfiable() again without adding constraints returns the cached result in $O(1)$. Adding any constraint invalidates the cached result.

add_implication(a, f, b, g) also adds its contrapositive, as required by its equivalent 2-CNF clause.

Example

#include "graph/two_sat.hpp"

#include <iostream>

int main() {
    m1une::graph::TwoSat sat(3);

    sat.add_clause(0, true, 1, false); // x0 OR NOT x1
    sat.add_implication(1, true, 2, true);
    sat.set_value(0, true);

    if (!sat.satisfiable()) {
        std::cout << "impossible\n";
        return 0;
    }

    for (bool value : sat.answer()) {
        std::cout << value << "\n";
    }
}

Required by

Verified with

Code

#ifndef M1UNE_GRAPH_TWO_SAT_HPP
#define M1UNE_GRAPH_TWO_SAT_HPP 1

#include <cassert>
#include <cstddef>
#include <limits>
#include <utility>
#include <vector>

namespace m1une {
namespace graph {

// A 2-SAT solver using iterative strongly connected components.
struct TwoSat {
   private:
    struct Csr {
        std::vector<int> start;
        std::vector<int> to;
    };

    int _n;
    std::vector<std::pair<int, int>> _edges;
    bool _solved;
    bool _satisfiable;
    std::vector<bool> _answer;

    int node(int variable, bool value) const {
        assert(0 <= variable && variable < _n);
        return 2 * variable + int(value);
    }

    void add_edge(int from, int to) {
        _edges.emplace_back(from, to);
        _solved = false;
        _answer.clear();
    }

    Csr build_csr(bool reverse) const {
        int vertices = 2 * _n;
        Csr graph;
        graph.start.assign(vertices + 1, 0);
        graph.to.resize(_edges.size());

        for (auto [from, to] : _edges) {
            int source = reverse ? to : from;
            graph.start[source + 1]++;
        }
        for (int v = 0; v < vertices; v++) {
            graph.start[v + 1] += graph.start[v];
        }

        std::vector<int> cursor = graph.start;
        for (auto [from, to] : _edges) {
            int source = reverse ? to : from;
            int target = reverse ? from : to;
            graph.to[cursor[source]++] = target;
        }
        return graph;
    }

   public:
    TwoSat() : TwoSat(0) {}

    explicit TwoSat(int n)
        : _n(n), _solved(false), _satisfiable(false) {
        assert(0 <= n);
        assert(n <= std::numeric_limits<int>::max() / 2);
    }

    int size() const {
        return _n;
    }

    bool empty() const {
        return _n == 0;
    }

    // Reserves space for approximately `clause_count` two-literal clauses.
    void reserve(std::size_t clause_count) {
        assert(clause_count <= std::size_t(std::numeric_limits<int>::max()) / 2);
        _edges.reserve(2 * clause_count);
    }

    // Adds (variable i == f) OR (variable j == g).
    void add_clause(int i, bool f, int j, bool g) {
        int a = node(i, f);
        int b = node(j, g);
        add_edge(a ^ 1, b);
        add_edge(b ^ 1, a);
    }

    // Adds (variable i == f) => (variable j == g).
    void add_implication(int i, bool f, int j, bool g) {
        add_clause(i, !f, j, g);
    }

    // Forces variable i to equal value.
    void set_value(int i, bool value) {
        add_clause(i, value, i, value);
    }

    // Forces variables i and j to have equal values.
    void add_equal(int i, int j) {
        add_clause(i, false, j, true);
        add_clause(i, true, j, false);
    }

    // Forces variables i and j to have different values.
    void add_not_equal(int i, int j) {
        add_clause(i, true, j, true);
        add_clause(i, false, j, false);
    }

    bool satisfiable() {
        if (_solved) return _satisfiable;
        assert(_edges.size() <= std::size_t(std::numeric_limits<int>::max()));

        int vertices = 2 * _n;
        Csr graph = build_csr(false);
        Csr reverse_graph = build_csr(true);

        std::vector<char> seen(vertices, false);
        std::vector<int> order;
        order.reserve(vertices);
        std::vector<std::pair<int, int>> stack;
        stack.reserve(vertices);

        for (int start = 0; start < vertices; start++) {
            if (seen[start]) continue;
            seen[start] = true;
            stack.emplace_back(start, graph.start[start]);

            while (!stack.empty()) {
                int v = stack.back().first;
                int& edge = stack.back().second;
                if (edge == graph.start[v + 1]) {
                    order.push_back(v);
                    stack.pop_back();
                    continue;
                }

                int to = graph.to[edge++];
                if (!seen[to]) {
                    seen[to] = true;
                    stack.emplace_back(to, graph.start[to]);
                }
            }
        }

        std::vector<int> component(vertices, -1);
        std::vector<int> vertices_stack;
        vertices_stack.reserve(vertices);
        int component_count = 0;
        for (int index = vertices - 1; index >= 0; index--) {
            int start = order[index];
            if (component[start] != -1) continue;

            component[start] = component_count;
            vertices_stack.push_back(start);
            while (!vertices_stack.empty()) {
                int v = vertices_stack.back();
                vertices_stack.pop_back();
                for (int edge = reverse_graph.start[v];
                     edge < reverse_graph.start[v + 1];
                     edge++) {
                    int to = reverse_graph.to[edge];
                    if (component[to] == -1) {
                        component[to] = component_count;
                        vertices_stack.push_back(to);
                    }
                }
            }
            component_count++;
        }

        _answer.assign(_n, false);
        _satisfiable = true;
        for (int i = 0; i < _n; i++) {
            if (component[2 * i] == component[2 * i + 1]) {
                _satisfiable = false;
                _answer.clear();
                break;
            }
            _answer[i] = component[2 * i] < component[2 * i + 1];
        }
        _solved = true;
        return _satisfiable;
    }

    const std::vector<bool>& answer() const {
        assert(_solved && _satisfiable);
        return _answer;
    }

    bool value(int variable) const {
        assert(_solved && _satisfiable);
        assert(0 <= variable && variable < _n);
        return _answer[variable];
    }
};

}  // namespace graph
}  // namespace m1une

#endif  // M1UNE_GRAPH_TWO_SAT_HPP

#line 1 "graph/two_sat.hpp"



#include <cassert>
#include <cstddef>
#include <limits>
#include <utility>
#include <vector>

namespace m1une {
namespace graph {

// A 2-SAT solver using iterative strongly connected components.
struct TwoSat {
   private:
    struct Csr {
        std::vector<int> start;
        std::vector<int> to;
    };

    int _n;
    std::vector<std::pair<int, int>> _edges;
    bool _solved;
    bool _satisfiable;
    std::vector<bool> _answer;

    int node(int variable, bool value) const {
        assert(0 <= variable && variable < _n);
        return 2 * variable + int(value);
    }

    void add_edge(int from, int to) {
        _edges.emplace_back(from, to);
        _solved = false;
        _answer.clear();
    }

    Csr build_csr(bool reverse) const {
        int vertices = 2 * _n;
        Csr graph;
        graph.start.assign(vertices + 1, 0);
        graph.to.resize(_edges.size());

        for (auto [from, to] : _edges) {
            int source = reverse ? to : from;
            graph.start[source + 1]++;
        }
        for (int v = 0; v < vertices; v++) {
            graph.start[v + 1] += graph.start[v];
        }

        std::vector<int> cursor = graph.start;
        for (auto [from, to] : _edges) {
            int source = reverse ? to : from;
            int target = reverse ? from : to;
            graph.to[cursor[source]++] = target;
        }
        return graph;
    }

   public:
    TwoSat() : TwoSat(0) {}

    explicit TwoSat(int n)
        : _n(n), _solved(false), _satisfiable(false) {
        assert(0 <= n);
        assert(n <= std::numeric_limits<int>::max() / 2);
    }

    int size() const {
        return _n;
    }

    bool empty() const {
        return _n == 0;
    }

    // Reserves space for approximately `clause_count` two-literal clauses.
    void reserve(std::size_t clause_count) {
        assert(clause_count <= std::size_t(std::numeric_limits<int>::max()) / 2);
        _edges.reserve(2 * clause_count);
    }

    // Adds (variable i == f) OR (variable j == g).
    void add_clause(int i, bool f, int j, bool g) {
        int a = node(i, f);
        int b = node(j, g);
        add_edge(a ^ 1, b);
        add_edge(b ^ 1, a);
    }

    // Adds (variable i == f) => (variable j == g).
    void add_implication(int i, bool f, int j, bool g) {
        add_clause(i, !f, j, g);
    }

    // Forces variable i to equal value.
    void set_value(int i, bool value) {
        add_clause(i, value, i, value);
    }

    // Forces variables i and j to have equal values.
    void add_equal(int i, int j) {
        add_clause(i, false, j, true);
        add_clause(i, true, j, false);
    }

    // Forces variables i and j to have different values.
    void add_not_equal(int i, int j) {
        add_clause(i, true, j, true);
        add_clause(i, false, j, false);
    }

    bool satisfiable() {
        if (_solved) return _satisfiable;
        assert(_edges.size() <= std::size_t(std::numeric_limits<int>::max()));

        int vertices = 2 * _n;
        Csr graph = build_csr(false);
        Csr reverse_graph = build_csr(true);

        std::vector<char> seen(vertices, false);
        std::vector<int> order;
        order.reserve(vertices);
        std::vector<std::pair<int, int>> stack;
        stack.reserve(vertices);

        for (int start = 0; start < vertices; start++) {
            if (seen[start]) continue;
            seen[start] = true;
            stack.emplace_back(start, graph.start[start]);

            while (!stack.empty()) {
                int v = stack.back().first;
                int& edge = stack.back().second;
                if (edge == graph.start[v + 1]) {
                    order.push_back(v);
                    stack.pop_back();
                    continue;
                }

                int to = graph.to[edge++];
                if (!seen[to]) {
                    seen[to] = true;
                    stack.emplace_back(to, graph.start[to]);
                }
            }
        }

        std::vector<int> component(vertices, -1);
        std::vector<int> vertices_stack;
        vertices_stack.reserve(vertices);
        int component_count = 0;
        for (int index = vertices - 1; index >= 0; index--) {
            int start = order[index];
            if (component[start] != -1) continue;

            component[start] = component_count;
            vertices_stack.push_back(start);
            while (!vertices_stack.empty()) {
                int v = vertices_stack.back();
                vertices_stack.pop_back();
                for (int edge = reverse_graph.start[v];
                     edge < reverse_graph.start[v + 1];
                     edge++) {
                    int to = reverse_graph.to[edge];
                    if (component[to] == -1) {
                        component[to] = component_count;
                        vertices_stack.push_back(to);
                    }
                }
            }
            component_count++;
        }

        _answer.assign(_n, false);
        _satisfiable = true;
        for (int i = 0; i < _n; i++) {
            if (component[2 * i] == component[2 * i + 1]) {
                _satisfiable = false;
                _answer.clear();
                break;
            }
            _answer[i] = component[2 * i] < component[2 * i + 1];
        }
        _solved = true;
        return _satisfiable;
    }

    const std::vector<bool>& answer() const {
        assert(_solved && _satisfiable);
        return _answer;
    }

    bool value(int variable) const {
        assert(_solved && _satisfiable);
        assert(0 <= variable && variable < _n);
        return _answer[variable];
    }
};

}  // namespace graph
}  // namespace m1une

m1une's library

This documentation is automatically generated by online-judge-tools/verification-helper

Two-Satisfiability
(graph/two_sat.hpp)

Overview

Literal Convention

Construction

Methods

Example

Required by

Verified with

Code

Two-Satisfiability (graph/two_sat.hpp)

Overview

Literal Convention

Construction

Methods

Example

Required by

Verified with

Code

Two-Satisfiability
(graph/two_sat.hpp)