Mister雑記

競プロやります。

AOJ 1620 「論理式圧縮機」

onlinejudge.u-aizu.ac.jp

問題

以下の文法からなる論理式が与えられる。

<E> ::= 0 | 1 | a | b | c | d | -<E> | (<E>*<E>) | (<E>^<E>)

ここで-*^はそれぞれnot、and、xorに当たる。

与えられた式と同値な論理式で、最短のものの長さを求めよ。

制約

  • 論理式の長さは 16以下

考察

与えられた論理式を同値なものに圧縮する、みたいなことを考えるとどツボにハマる。

そもそも論理式が同値というのは「a~dにどんな真理値を割り振っても、全体の真理値が合致する」ということである。 よって全ての割り振りに対して全体の真理値を求め、それをintにすることでその論理式を表現することができる(これを真理値表と呼ぶことにする)。 この真理値表は 2^4通りの全ての割り振りに対して構文解析を行うことで求められる。

後はこの真理値表に対応する論理式の、長さの最小値が分かればいい。 これは長さが短い方から、「その長さの論理式で表現できる真理値表」を求めていけばいい。これは

  • 長さを1増やしてnotをつける
  • 長さを3増やしてandかxorをつける

という遷移によって埋めることができる。

疑問なのは計算量だが、なんと長さ16の論理式で表せる真理値表の数は 3,000を超えない。これはxorとandは高々3個しか入らないことが大きな要因となっている。

実装例

構文解析とDPで実装はそこそこ重いが、やるしかない。

なお以下のコードでは、実装しやすいように文法を以下のように変換している。

expr ::= term | -expr | (bin)
bin  ::= expr*expr | expr^expr
term ::= 0 | 1 | a | b | c | d

onlinejudge.u-aizu.ac.jp

constexpr int mask = (1 << 16) - 1;
constexpr int INF = 1 << 30;

/* ----- 真理値表埋め ----- */
vector<vector<int>> T(17);
// T[l] = 長さlの論理式で表せる真理値表の集合(lは最小)

vector<int> U(1 << 16, INF);
// T[t] = 真理値表tを表す最短の論理式の長さ

void init() {
    // 長さ1は0, 1, a, b, c, dのみ
    T[1] = {0b0000000000000000,
            0b1111111111111111,
            0b1010101010101010,
            0b1100110011001100,
            0b1111000011110000,
            0b1111111100000000};
    for (auto t : T[1]) U[t] = 1;

    for (int k = 2; k <= 16; ++k) {
        for (auto t : T[k - 1]) {
            int v = mask ^ t;  // notを合成
            if (U[v] == INF) {
                U[v] = k;
                T[k].push_back(v);
            }
        }

        for (int i = 1; i <= k - 3 - i; ++i) {
            // 長さの和がk-3になる組を全て試す
            for (auto t1 : T[i]) {
                for (auto t2 : T[k - 3 - i]) {
                    int v = t1 & t2;  // andを合成
                    if (U[v] == INF) {
                        U[v] = k;
                        T[k].push_back(v);
                    }

                    v = t1 ^ t2;  // xorを合成
                    if (U[v] == INF) {
                        U[v] = k;
                        T[k].push_back(v);
                    }
                }
            }
        }
    }
}

/* ----- 構文解析 ----- */
string S;
int pat;  // a, b, c, dの割り振り

bool expr(int&);

// expr^expr, expr*expr
bool bin(int& i) {
    bool ret = expr(i);
    if (S[i] == '*') {
        ++i;
        ret = expr(i) && ret;
    } else if (S[i] == '^') {
        ++i;
        ret = expr(i) != ret;
    }
    return ret;
}

// 0, 1, a, b, c, d
bool term(int& i) {
    bool ret;
    if ('0' <= S[i] && S[i] <= '1') {
        ret = S[i] - '0';
    } else if ('a' <= S[i] && S[i] <= 'd') {
        ret = (pat >> (S[i] - 'a')) & 1;
    }
    ++i;
    return ret;
}

// term, -expr, (bin)
bool expr(int& i) {
    bool ret;
    if (S[i] == '(') {
        ++i;
        ret = bin(i);
        ++i;
    } else if (S[i] == '-') {
        ++i;
        ret = !expr(i);
    } else {
        ret = term(i);
    }
    return ret;
}

/* ----- main ----- */
bool solve() {
    cin >> S;

    // 真理値表を計算
    int i, tab = 0;
    for (pat = 0; pat < (1 << 4); ++pat) {
        i = 0;
        tab += expr(i) << pat;
    }

    // 前計算で得たテーブルを参照
    cout << U[tab] << endl;
    return true;
}

構文解析にて1つ大きな注意点がある。 bin内のret = expr(i) && ret;だが、これは順番を逆にすると短絡評価によってexpr(i)が評価されないことがある。 一番確実なのは変数に格納することである。

反省

  • シンプルに実装が重くてしんどい。
  • 真理値表の数があれだけ少ないのは非自明だった。