example_bdd_constraint_var18.cpp

example_bdd_constraint_var18.cpp

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

using namespace std;

int main() {
    Cudd mgr;

    // 桁数19 (= 変数の個数) x0, x1, ..., x18
    const int N = 19;
    vector<BDD> X(N);
    for (int i = 0; i < N; i++)
        X[i] = mgr.bddVar();

    // Coefficients
    vector<int> C = {300, 300, 285, 285, 265, 265, 230, 230,
                     190, 200, 400, 200, 400, 200, 400, 200,
                     400, 200, 200};
    const int Capacity = 2700;

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

    // dot dump
    const vector<ADD> vec = {f.Add()};
    auto fp = fopen("F.dot", "w");
    const char* iname[19] = {"x0", "x1", "x2", "x3", "x4",
                             "x5", "x6", "x7", "x8", "x9",
                             "x10", "x11", "x12", "x13", "x14",
                             "x15", "x16", "x17", "x18"};
    const char* oname[1] = {"F"};
    mgr.DumpDot(vec, iname, oname, fp);
    return 0;
}