#include <cassert>
#include <cstdlib>
#include <fstream>
#include <iomanip>
#include <iostream>
#include <iterator>
#include <map>
#include <set>
#include <string>
#include <vector>

using namespace std;

typedef map<int,int> mii;
typedef set<int> si;
typedef vector<int> vi;
typedef vector<vi> vvi;

const int statistics   = 9; // level of statistic reports

const int tuplesize    = 4; // must be 3 or 4
const int permutations = tuplesize == 3 ? 6 : 24;
const int subsets      = 1 << permutations;

const int reduction_sequence_length = 18;
int reduction_sequence[reduction_sequence_length] = {
  0xfffffe, 0xfb0010, 0xd00010, 0xd40492, 0xa02000, 0x900000,
  0x808000, 0x860010, 0xc00800, 0xd40000, 0x840000, 0xc05000,
  0x800080, 0xe00001, 0xc00040, 0xa08200, 0xe38ab2, 0xfff0c3
};

const int reduction_pairs_length = 12;
int reduction_pairs[reduction_pairs_length][2] = {
  {0x810081, 0xff51c7}, {0xa80105, 0xc20043}, {0xe0084d, 0xf33ccf},
  {0xe30800, 0xebaa28}, {0xe80000, 0xeb0820}, {0xe80800, 0xeb0820},
  {0xeb0000, 0xeb0820}, {0xeb0800, 0xeb8a00}, {0xf00000, 0xf3cf00},
  {0xf30000, 0xf38e00}, {0xffff00, 0xffffc0}, {0xe3fb4d, 0xebfb6d}
};

const int remaining_classes_length = 9;
int remaining_classes[remaining_classes_length] = {
  0x000000, 0x800000, 0xd75aeb,
  0xe80000, 0xf00000, 0xfafdfe,
  0xfffddf, 0xfffffe, 0xffffff
};
string remaining_classes_name[remaining_classes_length] = {
  "nothing allowed", "topological sort", "reverse and cyclic symmetry",
  "not as last", "not as first", "cyclic symmetry",
  "reverse symmetry", "one not allowed", "everything allowed"
};

////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
// permutation algorithms
////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////

const int decode_permutation[24][4] = {
  {3,2,1,0},
  {3,2,0,1},
  {3,1,2,0},
  {3,1,0,2},
  {3,0,2,1},
  {3,0,1,2},
  {2,3,1,0},
  {2,3,0,1},
  {2,1,3,0},
  {2,1,0,3},
  {2,0,3,1},
  {2,0,1,3},
  {1,3,2,0},
  {1,3,0,2},
  {1,2,3,0},
  {1,2,0,3},
  {1,0,3,2},
  {1,0,2,3},
  {0,3,2,1},
  {0,3,1,2},
  {0,2,3,1},
  {0,2,1,3},
  {0,1,3,2},
  {0,1,2,3}
};

// find the number i such that decode_permutation[i] == p, i.e., the position in the lexicographic ordering
int encode_permutation(int *p) {
  for (int i=0 ; i<permutations ; i++) {
    for (int j=0 ; j<tuplesize ; j++)
      if (decode_permutation[i][j] != p[j])
        goto next;
    return i;
next:;
  }
  assert(0);
}

// Permutations are ordered reverse-lexicographically.
// A subset of permutations is represented by an integer of "permutations" bits.
// The highest of those bits represents the first permutation in lexicographical order, the lowest bit the last permutation.
// A permutation is included in the subset iff the corresponding bit is set to one.

const int method_open                 = 0;
const int method_symmetry_by_renaming = 1;
const int method_symmetry_by_reversal = 2;
const int method_topological_sorting  = 3;
const int method_npc                  = 4;
const int method_linear_time          = 5;
const int method_clause_conjunction   = 6;
const int method_max                  = 7;

typedef struct {
  int method;
  int symmetryclass;
  int classsize;
} solution;

solution problem[subsets];

void init() {
  for (int s=0 ; s<subsets ; s++) {
    problem[s].method        = method_open;
    problem[s].symmetryclass = s;
    problem[s].classsize     = 1;
  }
}

////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
// symmetry by renaming, i.e., permuting all constraints the same way (compensated by (reverse-)permuting the triples)
////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////

// find the code of the composition p1;p2 of two permutations given by their codes
int compose_permutation(int p1, int p2) {
  assert(0 <= p1 && p1 < permutations && 0 <= p2 && p2 < permutations);
  int perm[tuplesize];
  for (int i=0 ; i<tuplesize ; i++)
    perm[i] = decode_permutation[p2][decode_permutation[p1][i]];
  return encode_permutation(perm);
}

// apply permutation p to all permutations in the subset s simultaneously
int permute_by(int s, int p) {
  int result = 0;
  for (int j=0 ; j<permutations ; j++)
    if (s & (1 << j))
      result |= 1 << compose_permutation(j, p);
  return result;
}

// apply all permutations to a subset s
si all_permutations_of(int s) {
  si result;
  for (int i=0 ; i<permutations ; i++)
    result.insert(permute_by(s, i));
  return result;
}

// find the symmetry classes by renaming
void symmetry_by_renaming() {
  if (statistics >= 1) {
    cout << "Now removing those problems solvable using symmetry by renaming." << endl;
  }
  // By using the reverse order, the single remaining open problem in each class is the lexicographically smallest.
  int left = subsets, nextstat = subsets/1000000*1000000;
  for (int s=subsets-1 ; s>=0 ; s--) {
    if (statistics >= 9) {
      if (left < nextstat) {
        cout << nextstat << " more problems to consider..." << endl;
        nextstat -= 1000000;
      }
    }
    if (problem[s].method == method_open) {
      si perms = all_permutations_of(s);
      assert(perms.find(s) != perms.end());
      for (si::iterator it = perms.begin() ; it != perms.end() ; ++it)
        // Problem s remains open, all others are solved.
        if (*it != s) {
          problem[*it].method        = method_symmetry_by_renaming;
          problem[*it].symmetryclass = s;
          ++problem[s].classsize;
        }
      left -= problem[s].classsize;
    }
  }
}

////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
// reduction from 3-tuples to 4-tuples and between
////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////

bool is_subsequence_of(const vi xs, const vi ys) {
  vi::const_iterator xt = xs.begin();
  vi::const_iterator yt = ys.begin();
  while (xt != xs.end() && yt != ys.end()) {
    if (*xt == *yt)
      ++xt;
    ++yt;
  }
  return xt == xs.end();
}

const int max_elements = 7+1;
const int max_perms    = 7*6*5*4*3*2*1;
const int max_combs    = 7*6*5*4;

vvi all_perms[max_elements];
vvi all_combs[max_elements][max_elements];

void precalc_all_perms() {
  for (int ne=0 ; ne<max_elements ; ne++) {
    all_perms[ne].clear();
    // generate all permutations of ne elements
    vi perm(ne);
    for (int i=0 ; i<ne ; i++)
      perm[i] = i;
    do all_perms[ne].push_back(perm); while (next_permutation(perm.begin(), perm.end()));
    reverse(all_perms[ne].begin(), all_perms[ne].end());
  }
}

void precalc_all_combs() {
  for (int choose=3 ; choose<=4 ; choose++) {
    vi comb(choose);
    for (int outof=choose ; outof<max_elements ; outof++) {
      all_combs[choose][outof].clear();
      // generate all combinations of type2 elements from ne elements, with significant order
      for (comb[0]=0 ; comb[0]<outof ; comb[0]++)
        for (comb[1]=0 ; comb[1]<outof ; comb[1]++)
          if (comb[0] != comb[1])
            for (comb[2]=0 ; comb[2]<outof ; comb[2]++)
              if (comb[0] != comb[2] && comb[1] != comb[2])
                if (choose == 3)
                  all_combs[choose][outof].push_back(comb);
                else
                  for (comb[3]=0 ; comb[3]<outof ; comb[3]++)
                    if (comb[0] != comb[3] && comb[1] != comb[3] && comb[2] != comb[3])
                      all_combs[choose][outof].push_back(comb);
    }
  }
}

void precalc() {
  precalc_all_perms();
  precalc_all_combs();
}

int extend_perms[max_elements][max_perms];
bool extend_combs[max_elements][max_combs][max_perms];

void precalc_extend_perms(int type1, int p1, int ne) {
  for (int i2=0 ; i2<all_perms[ne].size() ; i2++) {
    extend_perms[ne][i2] = 0;
    for (int i1=0 ; i1<all_perms[type1].size() ; i1++)
      if ((p1 & (1<<i1)) != 0 && is_subsequence_of(all_perms[type1][i1], all_perms[ne][i2]))
        extend_perms[ne][i2] |= 1<<i1;
  }
}

vvi precalc_apply_perms(int type2, int p2, int ne, const vi comb) {
  vvi result;
  for (int i2=0 ; i2<all_perms[type2].size() ; i2++)
    if ((p2 & (1<<i2)) != 0) {
      vi permuted_comb(type2);
      for (int i=0 ; i<type2 ; i++)
        permuted_comb[i] = comb[all_perms[type2][i2][i]];
      result.push_back(permuted_comb);
    }
  return result;
}

void precalc_extend_combs(int type2, int p2, int ne) {
  for (int i1=0 ; i1<all_combs[type2][ne].size() ; i1++) {
    vvi combs = precalc_apply_perms(type2, p2, ne, all_combs[type2][ne][i1]);
    for (int i2=0 ; i2<all_perms[ne].size() ; i2++) {
      extend_combs[ne][i1][i2] = false;
      for (int i=0 ; i<combs.size() ; i++)
        if (is_subsequence_of(combs[i], all_perms[ne][i2])) {
          extend_combs[ne][i1][i2] = true;
          break;
        }
    }
  }
}

int init_timeout, timeout;
vi used;

int bt_p1, bt_ne, bt_combs, bt_maxcombs;

bool is_reducible_bt(const vi perms) {
  if (--timeout <= 0)
    return false;
  int ored = 0;
  bool zero = true;
  for (int i=0 ; i<perms.size() ; i++) {
    ored |= extend_perms[bt_ne][perms[i]];
    zero &= (extend_perms[bt_ne][perms[i]] != 0);
  }
  if (ored != bt_p1)
    return false;
  if (zero)
    return true;
  if (bt_combs == bt_maxcombs)
    return false;
  vi cut_perms;
  for (int i=0 ; i<perms.size() ; i++)
    if (extend_combs[bt_ne][bt_combs][perms[i]])
      cut_perms.push_back(perms[i]);
  used.push_back(bt_combs);
  ++bt_combs;
  if (cut_perms.size() < perms.size() && is_reducible_bt(cut_perms))
    return true;
  used.pop_back();
  if (is_reducible_bt(perms))
    return true;
  --bt_combs;
  return false;
}

bool is_reducible(int type1, int p1, int type2, int p2, int ne) {
  timeout=init_timeout;
  precalc_extend_perms(type1, p1, ne);
  precalc_extend_combs(type2, p2, ne);
  vi init_perms(all_perms[ne].size());
  for (int i=0 ; i<all_perms[ne].size() ; i++)
    init_perms[i] = i;
  used.clear();
  bt_p1 = p1;
  bt_ne = ne;
  bt_combs = 0;
  bt_maxcombs = all_combs[type2][ne].size();
  if (is_reducible_bt(init_perms)) {
    cerr << "0x"
         << hex << setw(6) << setfill('0') << p1
         << dec << setw(0) << setfill(' ') << "<=0x"
         << hex << setw(6) << setfill('0') << p2
         << dec << setw(0) << setfill(' ') << " ";
    int bits[32];
    for (int i=0 ; i<32 ; i++)
      bits[i] = 0;
    for (int i=0 ; i<used.size() ; i++) {
      // copy(all_combs[type2][ne][used[i]].begin(), all_combs[type2][ne][used[i]].end(), ostream_iterator<int>(cerr, ""));
      // cerr << " ";
      int bit = bt_maxcombs-1 - used[i];
      bits[bit/4] |= 1 << (bit%4);
    }
    for (int i=29 ; i>=0 ; i--)
      cerr << hex << bits[i] << dec;
    cerr << endl;
    return true;
  }
  return false;
}

////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
// mutually reducible problems
////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////

typedef struct {
  int p;
  int rank;
  int size;
} disjoint_sets;

disjoint_sets problem_set[subsets];
int problem_set_p[subsets];

void make_disjoint_sets() {
  for (int s=0 ; s<subsets ; s++) {
    problem_set[s].p    = s;
    problem_set[s].rank = 0;
    problem_set[s].size = 1;
  }
}

int find_set(int x) {
  if (x != problem_set[x].p)
    problem_set[x].p = find_set(problem_set[x].p);
  return problem_set[x].p;
}

void link_sets(int x, int y) {
  if (problem_set[x].rank > problem_set[y].rank) {
    problem_set[y].p     = x;
    problem_set[x].size += problem_set[y].size;
  } else {
    problem_set[x].p     = y;
    problem_set[y].size += problem_set[x].size;
    if (problem_set[x].rank == problem_set[y].rank)
      ++problem_set[y].rank;
  }
}

void union_sets(int x, int y) {
  link_sets(find_set(x), find_set(y));
}

void init_disjoint_sets() {
  for (int s=0 ; s<subsets ; s++)
    if (problem[s].method == method_symmetry_by_renaming)
      union_sets(s, problem[s].symmetryclass);
}

void flatten_sets() {
  for (int s=0 ; s<subsets ; s++)
    problem_set[s].rank = s == find_set(s) ? 1 : 0;
}

void prepare_before_write() {
  flatten_sets();
  for (int s=0 ; s<subsets ; s++)
    problem_set_p[s] = problem_set[s].p;
}

void prepare_after_read() {
  for (int s=0 ; s<subsets ; s++)
    problem_set[s].p = problem_set_p[s];
  for (int s=0 ; s<subsets ; s++)
    problem_set[s].size = 0;
  for (int s=0 ; s<subsets ; s++)
    problem_set[find_set(s)].size++;
  flatten_sets();
}

int global_cnt;

void reduce_from(int ne, int from) {
  assert(find_set(from) == find_set(0xfffffe));
  if (statistics >= 1) {
    cout << "Now removing those problems reducible from " << hex << from << dec << "." << endl;
  }
  int sets = global_cnt;
  int setsleft = sets;
  int left = subsets, nextstat = subsets/1000000*1000000;
  for (int s=subsets-1 ; s>=0 ; s--) {
    if (s == find_set(s)) {
      if (s != find_set(from) && is_reducible(4, from, 4, s, ne)) {
        union_sets(from, s);
        --sets;
      }
      --setsleft;
    }
    --left;
    if (statistics >= 9) {
      if (left < nextstat) {
        cout << nextstat << " problems to consider, " << setsleft << " sets to consider, " << sets << " sets remaining" << endl;
        nextstat -= 1000000;
      }
    }
  }
}

void reduce_pair(int ne, int x1, int x2) {
  if (statistics >= 1) {
    cout << "Now interreducing " << hex << x1 << dec << " and " << hex << x2 << dec << "." << endl;
  }
  if (find_set(x1) == find_set(x2))
    cout << "They are already in the same set." << endl;
  if (is_reducible(4, x1, 4, x2, ne) && is_reducible(4, x2, 4, x1, ne))
    union_sets(x1, x2);
}

void global_statistics() {
  mii sizes;
  for (int i=0 ; i<subsets ; i++)
    if (problem_set[i].p == i)
      ++sizes[problem_set[i].size];
  int cnt = 0;
  for (mii::iterator it = sizes.begin() ; it != sizes.end() ; ++it) {
    cout << it->first << ":" << it->second << " ";
    cnt += it->second;
  }
  cout << "...total=" << cnt << endl;
  global_cnt = cnt;
  system("/bin/date");
}

int count_bits(int x) {
  int cnt = 0;
  for ( ; x ; x >>= 1)
    if (x & 1)
      ++cnt;
  return cnt;
}

vi get_classes() {
  vi classes;
  mii best, cnt;
  for (int i=0 ; i<subsets ; i++)
    if (i == find_set(i)) {
      classes.push_back(i);
      best[i] = i;
      cnt[i] = 0;
    }
  for (int i=0 ; i<subsets ; i++) {
    ++cnt[find_set(i)];
    if (count_bits(i) <= count_bits(best[find_set(i)]))
      best[find_set(i)] = i;
  }
  cout << "classes:" << endl;
  for (mii::iterator it = best.begin() ; it != best.end() ; ++it)
    cout << "0x"
         << hex << setw(6) << setfill('0') << it->first
         << dec << setw(0) << setfill(' ')
         << ":size=" << cnt[it->first]
         << ":member=0x"
         << hex << setw(6) << setfill('0') << it->second
         << dec << setw(0) << setfill(' ')
         << ",bits=" << count_bits(it->second)
         << endl;
  return classes;
}

// reduce from every class to every other class and back
void reduce_open(int ne, vi &classes) {
  if (statistics >= 1) {
    cout << "Now merging those problems reducible to each other." << endl;
  }
  int sets = global_cnt;
  for (vi::iterator it = classes.begin() ; it != classes.end() ; ++it) {
    if (statistics >= 9) {
      global_statistics();
      cout << "Working on " << hex << *it << dec << "; remaining classes: " << sets << endl;
    }
    for (vi::iterator jt = it+1 ; jt != classes.end() ; ++jt)
      if (find_set(*it) != find_set(*jt)) {
        bool b1 = is_reducible(4, *it, 4, *jt, ne);
        bool b2 = is_reducible(4, *jt, 4, *it, ne);
        if (b1 && b2) {
          --sets;
          union_sets(*it, *jt);
        }
      }
  }
}

////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
// main
////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////

string read_from_file = "";
string read_sets_from_file = "";
string write_sets_to_file = "";

void args(int argc, char **argv) {
  for (int i=0 ; i<argc ; i++) {
    string s(argv[i]);
    if (s.substr(0, 5) == "read:")
      read_from_file = s.substr(5);
    if (s.substr(0, 9) == "readsets:")
      read_sets_from_file = s.substr(9);
    if (s.substr(0, 10) == "writesets:")
      write_sets_to_file = s.substr(10);
  }
}

void do_read() {
  if (read_from_file != "") {
    cout << "Reading data from " << read_from_file << " ..." << endl;
    ifstream in(read_from_file.c_str());
    in.read((char*)problem,sizeof(problem));
    in.close();
  }
  if (read_sets_from_file != "") {
    cout << "Reading sets from " << read_sets_from_file << " ..." << endl;
    ifstream in(read_sets_from_file.c_str());
    in.read((char*)problem_set_p,sizeof(problem_set_p));
    in.close();
    prepare_after_read();
  }
}

void do_write() {
  if (write_sets_to_file != "") {
    prepare_before_write();
    cout << "Writing sets to " << write_sets_to_file << " ..." << endl;
    ofstream out(write_sets_to_file.c_str());
    out.write((char*)problem_set_p,sizeof(problem_set_p));
    out.close();
  }
}

void graph() {
  mii cnt;
  for (int i=0 ; i<subsets ; i++)
    ++cnt[find_set(i)];
  // reducibility matrix
  init_timeout=10000;
  int m[remaining_classes_length][remaining_classes_length];
  for (int i=0 ; i<remaining_classes_length ; i++)
    for (int j=0 ; j<remaining_classes_length ; j++)
      m[i][j] = is_reducible(4, remaining_classes[i], 4, remaining_classes[j], 5) ? 1 : 0;
  // transitive hull
  for (int k=0 ; k<remaining_classes_length ; k++)
    for (int i=0 ; i<remaining_classes_length ; i++)
      for (int j=0 ; j<remaining_classes_length ; j++)
        if (m[i][k] && m[k][j])
          m[i][j] = 1;
  // mark transitive edges
  for (int i=0 ; i<remaining_classes_length ; i++)
    for (int j=0 ; j<remaining_classes_length ; j++)
      for (int k=0 ; k<remaining_classes_length ; k++)
        if (i!=k && j!=k && m[i][k] && m[k][j])
          m[i][j] = 2;
  // output graph in dot-format
  cout << "digraph G {" << hex << endl;
  cout << "  node [shape=box];" << endl;
  cout << "  // nodes" << endl;
  for (int i=0 ; i<remaining_classes_length ; i++) {
    cout << "  node" << remaining_classes[i] << " [label=\""
         << " " << remaining_classes_name[i] << "\\l"
         << " instance=0x" << remaining_classes[i] << "\\l"
         << " representative=0x" << find_set(remaining_classes[i]) << "\\l"
         << " size=" << dec << cnt[find_set(remaining_classes[i])] << hex << "\\l"
         << "\"];" << endl;
  }
  cout << "  // edges" << endl;
  for (int i=0 ; i<remaining_classes_length ; i++)
    for (int j=0 ; j<remaining_classes_length ; j++)
      if (i!=j && m[i][j] == 1)
        cout << "  node" << remaining_classes[i] << " -> node" << remaining_classes[j] << ";" << endl;
  cout << "}" << dec << endl;
}

int main(int argc, char **argv) {
  args(argc, argv);
  init();
  precalc();

  make_disjoint_sets();
  do_read();
  global_statistics();

  if (read_sets_from_file == "") {
    if (read_from_file == "") {
      symmetry_by_renaming();
    }
    init_disjoint_sets();
    global_statistics();
    do_write();

    init_timeout=200000;
    for (int i=0 ; i<reduction_sequence_length ; i++) {
      reduce_from(5, reduction_sequence[i]);
      global_statistics();
      if (i<4) do_write();
    }

    cerr << endl;
    init_timeout=10000;
    reduce_open(5, get_classes());
    global_statistics();
    get_classes();

    cerr << endl;
    init_timeout=5000000;
    for (int i=0 ; i<reduction_pairs_length ; i++) {
      reduce_pair(5, reduction_pairs[i][0], reduction_pairs[i][1]);
    }
    global_statistics();
    get_classes();
    do_write();

    cerr << endl;
    graph();
  }

  return 0;
}