Horn-SAT
(sat/hornsat.hpp)

• View this file on GitHub
• Last update: 2024-01-08 13:32:33+09:00
• Include: #include "sat/hornsat.hpp"

Description

Horn-SAT は，節内の肯定リテラル数が高々1つであるような乗法標準形の論理式に対する充足可能性問題 (SAT) である．

$(a_1 \land a_2 \land \dots \land a_n \rightarrow b)$ や $(a_1 \land a_2 \land \dots \land a_n \rightarrow \lnot b)$ といった論理式は，高々1つの肯定リテラルからなる節 (Horn 節) に変換できる．

この問題は unit-propagation によって解ける．肯定リテラルのみからなる節がない場合はすべてのリテラルを false にし，そのような節があればそのリテラルの値を true に確定し残りのリテラルについて同じ問題を解けば良い．

Operations

• vector<bool> horn_sat(int n_literals, vector<pair<int, vector<int>>> clauses)
  • $n_{literals}$ リテラルを含む Horn 節のリストが与えられたとき，すべての節を充足するリテラルの真偽値の組み合わせを一つ返す．節は {p, {n}} の形で与え，$(p \lor \lnot n_1 \lor \dots \lor \lnot n_k)$ を追加する．肯定リテラルがない場合は pos = -1 とする．問題が充足可能でない場合，空リストを返す．
  • 時間計算量: $O(n_{literals})$

Reference

• Horn-satisfiability - Wikipedia
• Horn SATのメモ - むげんのぶろぐ
• verify: https://codeforces.com/gym/103202/submission/153602970

Code

#pragma once
#include <stack>
#include <utility>
#include <vector>

std::vector<bool> horn_sat(
    int n_literals,
    const std::vector<std::pair<int, std::vector<int>>>& clauses) {
    const int n_clauses = clauses.size();
    std::vector<bool> val(n_literals, false);
    std::vector<std::vector<int>> neg(n_clauses), idx(n_literals);
    std::vector<int> pos(n_clauses), n_neg(n_clauses);

    int k = 0;
    for (auto& [p, n] : clauses) {
        pos[k] = p;
        neg[k] = n;
        n_neg[k] = n.size();
        for (int i : n) idx[i].push_back(k);
        ++k;
    }

    // if there is a clause with no negative literals and a positive literal,
    // make it positive and remove it from other clauses.
    // if there is no such clause, make all remaining literals negative.
    std::stack<int> st;
    for (int i = 0; i < n_clauses; ++i) {
        if (n_neg[i] == 0 && pos[i] != -1) {
            st.push(i);
        }
    }
    while (!st.empty()) {
        int i = st.top();
        st.pop();
        if (val[pos[i]]) continue;
        val[pos[i]] = true;
        for (int j : idx[pos[i]]) {
            --n_neg[j];
            if (n_neg[j] == 0 && pos[j] != -1) {
                st.push(j);
            }
        }
    }
    // check
    for (int i = 0; i < n_clauses; ++i) {
        bool v = false;
        if (pos[i] != -1) v |= val[pos[i]];
        for (int j : neg[i]) v |= !val[j];
        if (!v) {
            // not satisfiable
            return {};
        }
    }
    return val;
}

#line 2 "sat/hornsat.hpp"
#include <stack>
#include <utility>
#include <vector>

std::vector<bool> horn_sat(
    int n_literals,
    const std::vector<std::pair<int, std::vector<int>>>& clauses) {
    const int n_clauses = clauses.size();
    std::vector<bool> val(n_literals, false);
    std::vector<std::vector<int>> neg(n_clauses), idx(n_literals);
    std::vector<int> pos(n_clauses), n_neg(n_clauses);

    int k = 0;
    for (auto& [p, n] : clauses) {
        pos[k] = p;
        neg[k] = n;
        n_neg[k] = n.size();
        for (int i : n) idx[i].push_back(k);
        ++k;
    }

    // if there is a clause with no negative literals and a positive literal,
    // make it positive and remove it from other clauses.
    // if there is no such clause, make all remaining literals negative.
    std::stack<int> st;
    for (int i = 0; i < n_clauses; ++i) {
        if (n_neg[i] == 0 && pos[i] != -1) {
            st.push(i);
        }
    }
    while (!st.empty()) {
        int i = st.top();
        st.pop();
        if (val[pos[i]]) continue;
        val[pos[i]] = true;
        for (int j : idx[pos[i]]) {
            --n_neg[j];
            if (n_neg[j] == 0 && pos[j] != -1) {
                st.push(j);
            }
        }
    }
    // check
    for (int i = 0; i < n_clauses; ++i) {
        bool v = false;
        if (pos[i] != -1) v |= val[pos[i]];
        for (int j : neg[i]) v |= !val[j];
        if (!v) {
            // not satisfiable
            return {};
        }
    }
    return val;
}

Back to top page