#include <omp.h>
#include <atomic>
#include <iostream>
#include <map>
#include <set>
#include <boost/rational.hpp>
#include <string>
#include <variant>
#include <optional>
#include <vector>

////////////////////////////////////////////////////////////////////////////////
// 周期列
////////////////////////////////////////////////////////////////////////////////
// 周期列の型 PinwheelInstance。周期は必ず昇順に並べるものとする。
class PinwheelInstance {
public:
  std::vector<unsigned int> periods;
  std::string to_string () const {
    std::string r{};
    for (size_t i = 0; i < periods.size(); ++i) r += (i == 0 ? "(" : " ") + std::to_string(periods[i]) + (i == periods.size() - 1 ? ")" : "");
    return r;
  };
  auto operator <=>(const PinwheelInstance&) const = default;
};

// density(c): 周期列 c の密度（周期の逆数の和）。
using rational = boost::rational<long long>; // 不等号の正確な判定のため有理数で計算するが、本プログラムで用いる周期列は各要素が下述の max_period 以下であり、それらの最小公倍数は数億程度なので、分母・分子は long long で十分
rational density (const PinwheelInstance& c) { 
  rational sum = 0;
  for (const auto& a : c.periods) sum += rational(1, a);
  return sum; 
}

////////////////////////////////////////////////////////////////////////////////
// 日割
////////////////////////////////////////////////////////////////////////////////
// 有限の日割（或いは、それを繰り返す無限の日割）の型 Schedule。周期（仕事番号ではなく）の列。
class Schedule {
public:
  std::vector<unsigned int> periods;
  template<typename Iter>
  Schedule(Iter first, Iter last) : periods(first, last) {}
  Schedule() = default;
  std::string to_string() const {
    std::string r{};
    for (size_t j = 0; j < periods.size(); ++j) r += (j == 0 ? "[" : " ") + std::to_string(periods[j]) + (j == periods.size() - 1 ? "]" : "");
    return r;
  }
};

////////////////////////////////////////////////////////////////////////////////
// 周期列 c が詰込割当可能か否かを、状態グラフが閉路をもつか調べることで判定
////////////////////////////////////////////////////////////////////////////////

// 状態の型 State
// 「周期 c_j の仕事を c_j - r_j 日前にした（j = 0, ..., k）」という状態（緊急度ベクトル）を列 {{r_1, c_1}, {r_2, c_2}, ..., {r_k, c_k}} で表す。
// 但し (r_j, c_j) が辞書順で昇順になるように並べるものとする。
class State {
public:
  std::vector<std::pair<unsigned int, unsigned int>> q;
  explicit State(size_t reserve_size = 0) {
    q.reserve(reserve_size); // 容量 reserve_size を確保して状態を作る
  }
  auto operator <=>(const State&) const = default;
}; 

// w = next_State(v, j0): 状態 v であった日に第 j0 番目（v において）の仕事を行うと（行える入力であることは保証されている）、次の日は状態 w になる。
std::optional<State> next_state (const State& v, size_t j0) {
  State w(v.q.size()); // v と同じ容量を確保して状態 w を作る
  // 以下では v.q の各成分を、適切に書き換えながら w.q に書き写してゆく。
  // j = 0, 1, ..., v.q.size() について順に見てゆく。j = j0 の場合以外は単に対 v.q[j] の左成分を 1 減らして w.q の末尾に書き加える。j = j0 の場合は直ちには書き加えないが、shifting を真にする。shifting が真であるときには、もし次に書き込もうとする対よりも j0 に由来する対 (v.q[j0].second - 1, v.q[j0].second) が辞書順で早ければ、この対を書き加えておく。但し辞書順でといっても、(v.q[j0].second - 1, v.q[j0].second) は左成分が v.q[j0].second - 1 である対のうち最小なので、左成分だけを見ればよい。
  bool shifting = false; // 現在の j の値が j0 以上 j1 以下のとき true（j1 は v.q の第 j0 成分の、w.q における行先）
  for (size_t j = 0; j < v.q.size(); j++) { // j は v 中の着目する成分の番地であり、この繰返しの開始時点で w.q の要素数は j - (shifting ? 1 : 0)
    if (j == j0) shifting = true;
    else {
      if ((not shifting) and v.q[j].first <= j) return std::nullopt;
      w.q.push_back({v.q[j].first - 1, v.q[j].second});
    }
    if (shifting and (j + 1 == v.q.size() or v.q[j + 1].first >= v.q[j0].second)) { // v.q[j + 1].first が（無いか）v.q[j0].second 以上、すなわち現在の j が j1 である
      w.q.push_back({v.q[j0].second - 1, v.q[j0].second});
      shifting = false;
    }
  }
  return w;
}

// find_cycle_sub(v, dead, visited, done): 
// 実行開始時における約束として、dead に属するどの状態からも閉路に到達不能であり、visited は初期状態から v への経路（但し初期状態から i 番目の状態を i へ写す写像として表す）、path はそれに対応する仕事列である。
// v から閉路に到達可能であるとき、その閉路を返す。さもなくば、v から到達可能な状態をすべて dead に加えた上で、真を返す。但し計算中に done が真になったことに気づくと中断して偽を返す。
std::variant<Schedule, bool> find_cycle_sub (const State& v, std::set<State>& dead, std::map<State, size_t>& visited, Schedule& path, std::atomic<bool>& done) {
  if (visited.contains(v)) return Schedule(path.periods.begin() + visited[v], path.periods.end()); // path のうち第 visited[v] 位置以降を出力
  visited[v] = path.periods.size();
  for (size_t j = 0; j < v.q.size(); ++j) { // すべての行先を試す
    auto ww = next_state(v, j);
    if (not ww) continue;
    State w = ww.value();
    if (dead.contains(w)) continue;
    if (done) return false;
    path.periods.push_back(v.q[j].second);
    std::variant<Schedule, bool> r = find_cycle_sub(w, dead, visited, path, done);
    path.periods.pop_back();
    if (std::holds_alternative<Schedule>(r) or not std::get<bool>(r)) return r; // w から到達可能な閉路が見つかった場合はその閉路を（v から到達可能な閉路として）返すし、計算中断ならば中断と返す
  }
  dead.insert(v);
  visited.erase(v);
  return true;
}
// find_cycle(c, done): 状態グラフ上の閉路検出の方法により、周期列 c の割当可能性を判定する。割当可能なら日割の一つを返し、不能なら真を返す。計算中に done が真になると中断して偽を返す。
std::variant<Schedule, bool> find_cycle (const PinwheelInstance& c, std::atomic<bool>& done) {
  std::set<State> dead{};
  std::map<State, size_t> visited{};
  State initial_state(c.periods.size());
  for (const auto& a : c.periods) initial_state.q.push_back({a - 1, a});
  Schedule path{};
  return find_cycle_sub(initial_state, dead, visited, path, done);
}

////////////////////////////////////////////////////////////////////////////////
// 割当可能性を高速に確かめる
////////////////////////////////////////////////////////////////////////////////
// 周期列 c の割当可能性が、より短い周期列 fold(c) の割当可能性を示すことで確かめられる場合がある。これを利用して高速に c の割当可能性を確かめる。

// fold(c): 長さ 2 以上の周期列 c の最後の二つの周期を一つに纏めて得られる周期列。fold(c) が割当可能ならば c も割当可能である。
PinwheelInstance fold (const PinwheelInstance& c) {
  PinwheelInstance d = c;
  unsigned int new_period = d.periods[d.periods.size() - 2] / 2;
  d.periods.pop_back();
  d.periods[d.periods.size() - 1] = new_period;
  sort(d.periods.begin(), d.periods.end());
  return d;
}

// all_folds(c): 周期列 c の割当可能性を調べるために調べるべき周期列集合。c が割当可能であるには、all_folds(c) の周期列のうち一つ以上が割当可能であることが必要十分。ここでは c, fold(c), fold(fold(c)), ... のうち密度 1 以下のもの全体としている。
std::vector<PinwheelInstance> all_folds (const PinwheelInstance& c) {
  if (density(c) > 1) return {};
  if (c.periods.size() <= 1) return {c};
  std::vector<PinwheelInstance> r = all_folds(fold(c));
  r.push_back(c);
  return r;
}

// check_one(c, known_schedules): 写像 known_schedules に書かれているのは、既知の周期列と正しい日割の組であるとする。このとき、周期列 c は割当可能か調べ、真偽を返す。これを all_folds(c) の各周期列の割当可能性を並列に調べることで行う。まず known_schedules から直ちに判るか調べる。判らなければ、並列に find_cycle で調べる。割当可能なら、割当できた周期列とその日割とを表示し、known_schedules に記入する。割当不能なら UNSCHEDULABLE と表示する。
bool check_one (const PinwheelInstance& c, std::map<PinwheelInstance, Schedule>& known_schedules) {
  std::vector<PinwheelInstance> cs = all_folds(c);
  for (const auto& d : cs) if (known_schedules.contains(d)) return true;
  std::atomic<bool> done{false}; // 共有変数
#pragma omp parallel num_threads(cs.size()) // cs の各要素を並列に調べる。或るスレッドが解を見つけて共有変数 done を真にすると、他のスレッドは中断して終了する。
  {
    PinwheelInstance d = cs[omp_get_thread_num()]; // 第 omp_get_thread_num() スレッド（cs[omp_get_thread_num()] を調べる）
    std::variant<Schedule, bool> s = find_cycle(d, done);
#pragma omp critical
    {
      if (std::holds_alternative<Schedule>(s) and not done) {
	known_schedules[d] = std::get<Schedule>(s); 
	done = true; 
      } 
    }
  }
  if (not done) std::cout << "UNSCHEDULABLE: " << c.to_string() << std::endl;
  return done;
}

////////////////////////////////////////////////////////////////////////////////
// main: 補題の検証
////////////////////////////////////////////////////////////////////////////////
// 補題の主張は、以下の定数を使って「max_period 以下の自然数からなる任意の PinwheelInstance c は、もし modified_density(c) ＜ bound_on_modified_density ならば詰込割当可能」。以下ではこの補題を確かめる。
const unsigned int half_theta = 11;
const unsigned int max_period = 2 * half_theta - 1;
const rational bound_on_modified_density = rational(29, 33);
rational modified_density (const PinwheelInstance& c) { // 周期列 c の half_theta 以上の各周期に 1 を加えたものの密度。
  rational sum = 0;
  for (const auto& a : c.periods) sum += rational(1, a + (a >= half_theta ? 1 : 0));
  return sum; 
}

// critical(c): 周期列 c は空でなく modified_density(c) ＜ bound_on_modified_density を満すとする。このとき、この条件を満す周期列すべての割当可能性を確かめるという文脈において周期列 c は本質的であるか判定する。但し c が本質的でないとは、周期列 d が存在してやはり modified_density(d) ＜ bound_on_modified_density を満し、d から c が明らかに単調性で得られることをいう。
bool critical (const PinwheelInstance& c) {
  if (c.periods.empty()) return false;
  PinwheelInstance d = c;
  d.periods[d.periods.size() - 1]--;
  if (modified_density(d) < bound_on_modified_density) return false;
  return true;
}

// check_all(c, known_schedules): 写像 known_schedules に書かれているのは、既知の周期列と正しい日割の組であるとする。このとき、周期列 c の末尾に max_period 以下の周期を一つ以上付け加えてできる周期列 d であって modified_density(d) ＜ bound_on_modified_density なるものすべてについて、詰込割当可能性を確かめ、その根拠となる周期列と日割の組を known_schedules に記入する。もし割当不能なら UNSCHEDULABLE と表示する。
void check_all (const PinwheelInstance& c, std::map<PinwheelInstance, Schedule>& known_schedules) {
  if (critical(c)) check_one(c, known_schedules);
  for (unsigned int e = c.periods.empty() ? 1 : c.periods[c.periods.size() - 1]; e <= max_period; ++e) {
    PinwheelInstance d = c;
    d.periods.push_back(e);
    if (modified_density(d) < bound_on_modified_density) check_all(d, known_schedules);
  }
}

// main(): これを実行して UNSCHEDULABLE が表示されないことを以て、補題が確かめられる。根拠となる周期列と日割の組を表示する。
int main (void) {
  std::map<PinwheelInstance, Schedule> known_schedules{};
  check_all({{}}, known_schedules); 
  for (const auto& [c, s] : known_schedules) std::cout << c.to_string() << ": " << s.to_string() << std::endl;
  return 0;
}