FindMUS/lib/HierMUSEnumer.cpp at develop · MiniZinc/FindMUS · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
#include <iostream>
#include <vector>

#include "HierMUSEnumer.h"
#include "Marco.h"
#include "ReMUS.h"

namespace HierMUS {
using std::vector;

HierMUSEnumer::HierMUSEnumer(SubProblem &prob, MUSEnumOptions &mo)
    : MusEnumerator(prob, mo), frontier_idx{0} {
  if (mo.map_enumeration_alg == ALG_REMUS) {
    if (mo.subproblem_structure != STR_FLAT ||
        mo.subproblem_binarize != BIN_NONE) {
      error("Warning: Hierarchical ReMUS has not been implemented. "
            "Results will be incorrect!");
    }
    inner_enum = new ReMUS(prob, mo, subsetMap);
  } else {
    inner_enum = new Marco(prob, mo, subsetMap);
  }

  inner_enum->setUnsatCallback([&](const Selection &s) {
    {
      std::stringstream ss;
      ss << "SubEnumerator adding set: " << s << " to candidates";
      log(ss.str());
    }

    if (frontier_idx != -1) {
      {
        std::stringstream ss;
        ss << "Unsetting: " << candidates[frontier_idx];
        log(ss.str());
      }
      candidates[frontier_idx].setMinimal(false);
    }
    unsatUnion = sel_union(unsatUnion, s);

    candidates.push_back(subsetMap->expand(s, s));
  });

  Statistics &stats = inner_enum->getStatistics();
  stats.restarts_enabled = mo.restarts_enabled;
  stats.treecounts = subProblem.getTree().getCounts();

  Selection root = subsetMap->getRootSelector();
  root.setMinimal(true);
  candidates.push_back(root);
  loadNextCandidate();
}
HierMUSEnumer::~HierMUSEnumer() { delete subsetMap; }

void HierMUSEnumer::setFrontier(const Selection &) {}

void HierMUSEnumer::loadNextCandidate() {
  Statistics &stats = inner_enum->getStatistics();
  if (stats.shouldRestart()) {
    log("Restarting in flat mode");
    candidates.clear();
    Selection leaves = subsetMap->getLeavesSelector();
    leaves.setMinimal(false);
    candidates.push_back(leaves);
    stats.restarts_enabled = false;
  }

  // Expand frontier
  if (frontier_idx != -1) {
    if (unsatUnion.empty()) {
      candidates[frontier_idx] =
          subsetMap->expand(candidates[frontier_idx], candidates[frontier_idx]);
    } else {
      candidates[frontier_idx] =
          subsetMap->expand(candidates[frontier_idx], unsatUnion);
      unsatUnion = {};
    }
  }

  Selection top = candidates.back();
  candidates.pop_back();
  if (!top.isLeaves()) {
    frontier_idx = static_cast<int>(candidates.size());
    candidates.push_back(top);
  } else {
    frontier_idx = -1;
  }
  inner_enum->setFrontier(top);
}

bool HierMUSEnumer::search() {
  current_mus = empty_selection;
  while (!mopts.timedOut()) {
    if (inner_enum->search()) {
      if (frontier_idx != -1) {
        {
          std::stringstream ss;
          ss << "Unsetting: " << candidates[frontier_idx];
          log(ss.str());
        }
        candidates[frontier_idx].setMinimal(false);
      }
      current_mus = inner_enum->getCurrentMUS();
      return true;
    }
    if (candidates.empty())
      return false;
    loadNextCandidate();
  }
  return false;
}

void HierMUSEnumer::printMUS(void) {
  if (mopts.timedOut()) {
    if (candidates.empty()) {
      log("Finished early. No remaining candidates.");
    } else if (mopts.print_leftover) {
      log("Finished early. Last (non-minimal) candidate:", 0);
      mopts.solution(subProblem.getSolStr(candidates.back()));
    } else {
      log("Finished early. Remaining candidate not printed (--no-leftover)", 0);
    }
    return;
  }
  if (!current_mus.empty()) {
    mopts.solution(subProblem.getSolStr(current_mus));
  }
}

Statistics &HierMUSEnumer::getStatistics(void) {
  return inner_enum->getStatistics();
}

} // namespace HierMUS