example_bdd_constraint.cpp

example_bdd_constraint.cpp

#include <iostream>
#include <random>
#include <vector>
#include "cuddObj.hh"

using namespace std;

int main() {
    Cudd mgr;

    // 桁数4 (= 変数の個数) x0, x1, x2, x3
    const int N = 4;
    vector<BDD> X(N);
    for (int i = 0; i < N; i++)
    X[i] = mgr.bddVar(); // 変数Xiの作成

    // 2x0 + 3x1 + 5x2 + 5x3 ≥ 7
    vector<int> values = {0, 0, 0, 1,
                          0, 1, 1, 1,
                          0, 1, 1, 1,
                          0, 1, 1, 1};

    BDD f = mgr.bddZero();
    for (int i = 0; i < (1 << N); i++) {
        // cout << i << " " << values[i] << endl;
        if (values[i] == 1) {
            BDD termi = mgr.bddOne();
            cout << i << " " << values[i] << ":";
            for (int k = 0; k < N; k++) {
                if (i & (1 << (N - k - 1)))
                    cout << k << "(" << (1 << k) << ") ";
                termi &= (i & (1 << (N - k - 1))) ? X[k] : !X[k];
            }
            cout << endl;
            f |= termi;
        }
    }

    // dot dump
    const vector<ADD> vec = {f.Add()};
    auto fp = fopen("F.dot", "w");
    const char* iname[4] = {"2 x0", "3 x1", "5 x2", "5 x3"};
    const char* oname[1] = {"F"};
    mgr.DumpDot(vec, iname, oname, fp);
    return 0;
}