#include <assert.h>
#include <algorithm>
#include <vector>
#include <string>
#include <iostream>
#include <set>

using namespace std;

class Placement;
class Rule;

// A Placement represents a "definite known" fact,
// such as "There is a '3' in the upper left cell
// of the grid."  The puzzle is solved when all
// Rules have exactly one Placement.
//
// When a Placement is Negated, it should remove
// its links to all rules.

class Placement {
 public:
  Placement() {
  }

  // set this placement to not be in the solution.
  // this should only be called at most once for any Placement.
  void Negate();

  bool isPossible() {
    return (rules.size() > 0);
  }

  int RuleCount() {
    return (rules.size());
  }

  void setName(string name) {
    name_ = name;
  }

  string toString() const {
    return name_;
  }

  void Remove(Rule* r) {
    rules.erase(r);
  }

  friend class Do;
 private:
  set<Rule*> rules;
  string name_;
};

enum RuleType {
  GENERIC = 0,
  CELL,
  ROW,
  COLUMN,
  SQUARE,
  kMaxRuleType
};

// A Rule represents a list of Placements such
// that exactly one of those Placements is true
// in a solution.  Examples of Rules in a sudoku puzzle are:
//   "There is a 5 in the second row."
//   "There is a unique value in the center cell of the grid."
//
// Sometimes a Rule becomes identical to another rule
// through elimination.  When that happens, we make one of
// the Rules a "Slave" to the other one.
// The "Master" has a list of all its Slaves.
// A Slave has to remove itself from all of its Placements
// as well.

class Rule {
 public:
  friend class Do;
  Rule() : slave_of_(NULL) {
  }
  bool solved() const {
    return (size() == 1);
  }
  int size() const {
    assert(placements.size() > 0);
    return placements.size();
  }

  void Negate(Placement* p) {
    assert(placements.find(p) != placements.end());
    placements.erase(p);
  }

  void setName(RuleType type, int index, int value) {
    type_ = type;
    index_ = index;
    value_ = value;
  }

  string toString() {
    string answer = "(";
    if (type_ == CELL) {
      answer += "There is something in ";
      answer += toRow(index_);
      answer += toCol(value_);
    } else if (type_ == ROW) {
      answer += "There is a ";
      answer += toVal(value_);
      answer += " in row ";
      answer += toRow(index_);
    } else if (type_ == COLUMN) {
      answer += "There is a ";
      answer += toVal(value_);
      answer += " in column ";
      answer += toCol(index_);
    } else if (type_ == SQUARE) {
      answer += "There is a ";
      answer += toVal(value_);
      answer += " in box ";
      answer += toVal(index_);
    } else {
      assert(false);
    }
    answer += ")";
    return answer;
  }

  bool CanEnslave(Rule* r) const;
  void Enslave(Rule* r);

  bool isSlave() const {
    return (slave_of_ != NULL);
  }

 private:
  set<Placement*> placements;

  // Used for English descriptions.
  RuleType type_;
  // For CELL type, these are row and column.
  int index_, value_;  

  char toRow(int row) {
    return (char)(row+(int)'A');
  }
  char toCol(int col) {
    return (char)(col+(int)'J');
  }
  char toVal(int val) {
    return (char)(val+(int)'1');
  }
  
  Rule* slave_of_;
  set<Rule*> slaves_;
};

// A Deduction is composed of two sets of Rules of equal
// size, call them the premises and the conclusions, and
// two sets of Placements, called the possibilities
// and the impossibilities.
//
// These conditions must be met:
//   All Placements in the premises are pairwise disjoint.
//   The possibilities and the impossibilities are pairwise
//    disjoint.
//   The union of all the Placements in the premises
//    is equal to the possibilities.
//   The union of all the Placements in the conclusions
//    is equal to the the union of the possibilities and
//    the impossibilities.
//
// We also create a set of Placements called the overloads.
//   The overloads is a subset of the possibilities.
//   Each overload must be in at least two conclusions.
//
// A (perhaps) more understandable way to state this in English is:
//   Suppose we have N Rules, and they are disjoint
//     (don't share any Placements).
//   Call them the premises.
//   Take all of their Placements, and call that the possibilities.
//   We know that exactly N of the possibilities are in the solution.
//   Now, Suppose we have another N Rules.
//   Call them the conclusions.
//   Take all of their Placements, and let's suppose that all
//      the possiblities are in there, calling the rest of the
//      Placements impossibilities.
//   Since we know N of the possibilities are in the solution, then
//      all the other ones (the impossibilities) can be labeled
//      impossible.
//
//  Also, none of the overloads can be true, or else there would
//  be more than N elements true in the conclusions.

class Deduction {
 public:
  set<Rule*> premises;
  set<Rule*> conclusions;
  set<Placement*> possibilities;
  set<Placement*> impossibilities;
  set<Placement*> overloads;
  int size() {
    return premises.size();
  }
  string toString();
  void Implement() {
    for (set<Placement*>::iterator it = impossibilities.begin();
         it != impossibilities.end(); ++it) {
      if ((*it)->isPossible())
        (*it)->Negate();
    }
    for (set<Placement*>::iterator it = overloads.begin();
         it != overloads.end(); ++it) {
      if ((*it)->isPossible())
        (*it)->Negate();
    }
  }
};

// Given a set and a count, runs through all
// the subsets of that set of size count.

template <class T> class Odometer {
 public:
  Odometer(const set<T*>& fodder, const int count)
      : fodder_(fodder), 
        odometer_(count),
        finished_(false),
        count_(count) {
    if (fodder_.size() < count) {
      finished_ = true;
      return;
    }
    odometer_[0] = fodder_.begin();
    for (int i = 1; i < count_; ++i) {
      odometer_[i] = odometer_[i-1];
      ++(odometer_[i]);
    }
  };
  bool finished() const {
    return finished_;
  }
  set<T*> currentValue() {
    set<T*> answer;
    for (int i = 0; i < count_; ++i) {
      answer.insert(*(odometer_[i]));
    }
    assert(answer.size() == count_);
    return answer;
  }
  void operator++ () {
    for (int i = count_-1; i >= 0; --i) {
      ++(odometer_[i]);
      if (odometer_[i] != fodder_.end()) {
        for (int j = i+1; j < count_; ++j) {
          odometer_[j] = odometer_[j-1];
          ++(odometer_[j]);
          if (odometer_[j] == fodder_.end()) {
            finished_ = true;
            return;
          }
        }
      }
    }
    if (odometer_[0] == fodder_.end()) {
      finished_ = true;
    }
  } 
 private:
  const set<T*> fodder_;
  vector<typename set<T*>::const_iterator> odometer_;
  bool finished_;
  const int count_;
};

// Actions that act on rules and placements.
class Do {
 public:
  // Associate a placement with a rule.
  static void Associate(Placement* p, Rule* r) {
    p->rules.insert(r);
    r->placements.insert(p);
  } 
  static string toString(set<Rule*>& rs) {
    string answer = "{";
    bool first = true;
    for (set<Rule*>::iterator it=rs.begin();
         it != rs.end(); ++it) {
      if (first)
        first = false;
      else
        answer += " and ";
      answer += (*it)->toString();
    }
    answer += "}";
    return answer;
  }
  static string toString(set<Placement*>& ps) {
    string answer = "{";
    bool first = true;
    for (set<Placement*>::iterator it=ps.begin();
         it != ps.end(); ++it) {
      if (first)
        first = false;
      else
        answer += " or ";
      answer += (*it)->toString();
    }
    answer += "}";
    return answer;
  }

  static bool CheckIdentical(const set<Placement*>& s1,
                             const set<Placement*>& s2) {
    if (SetDifference(s1, s2).size() > 0) return false;
    if (SetDifference(s2, s1).size() > 0) return false;
    return true;
  }

  static set<Placement*> Union(const Rule& r1, const Rule& r2) {
    set<Placement*> answer = r1.placements;
    for (set<Placement*>::iterator it = r2.placements.begin();
         it != r2.placements.end(); ++it) {
      answer.insert(*it);
    }
    return answer;
  }

  static set<Placement*> Intersection(const Rule& r1, const Rule& r2) {
    set<Placement*> answer;
    for (set<Placement*>::iterator it = r2.placements.begin();
         it != r2.placements.end(); ++it) {
      if (r1.placements.find(*it) != r1.placements.end())
        answer.insert(*it);
    }
    return answer;
  }

  static set<Placement*> Union(const Rule& r1, set<Placement*> r2) {
cout << "bah\n";
    set<Placement*> answer = r1.placements;
    for (set<Placement*>::iterator it = r2.begin();
         it != r2.end(); ++it) {
      answer.insert(*it);
    }
    return answer;
  }

  static set<Placement*> Union(set<Rule*> rs) {
    Rule* temp = *(rs.begin());
    assert(rs.size() != 0);
    if (rs.size() == 1) {
      return temp->placements;
    }
    rs.erase(temp);
    assert(0 != rs.size());
    return Union(*temp, Union(rs));
  }

  static bool IsSubset(const set<Placement*>& sub,
                       const set<Placement*>& super) {
    for (set<Placement*>::iterator it = sub.begin();
         it != sub.end(); ++it) {
      if (super.find(*it) == super.end())
        return false;
    }
    return true;
  }

  static set<Placement*> SetDifference(const set<Placement*>& big,
                                       const set<Placement*>& small) {
    set<Placement*> answer;
    for (set<Placement*>::iterator it = big.begin();
         it != big.end(); ++it) {
      if (small.find(*it) == small.end()) {
        answer.insert(*it);
      }
    }
    return answer;
  }

  // returns true if p appears in at least two elements of rs.
  static bool Twice(Placement* p, const set<Rule*>& rs) {
    if (rs.size() < 2) return false;
    int count = 0;
    for (set<Rule*>::iterator it = rs.begin();
         it != rs.end(); ++it) {
      set<Placement*>& ps = (*it)->placements;
      if (ps.find(p) != ps.end()) {
        count++;
        if (count >= 2) return true;
      }
    }
    return false;
  }

  static bool Disjoint(const Rule& r1, const Rule& r2) {
    return (Intersection(r1, r2).size() == 0);
  }

  static bool PairwiseDisjoint(set<Rule*> rs) {
    Rule* temp = *(rs.begin());
    rs.erase(temp);
    for (set<Rule*>::iterator it = rs.begin();
         it != rs.end(); ++it) {
      if (!Disjoint(*temp, **it)) return false;
    }
    return true;
  }

  static set<Rule*> AllRules(const set<Placement*>& ps) {
    set<Rule*> answer;
    for (set<Placement*>::iterator it = ps.begin();
         it != ps.end(); ++it) {
      Placement* p = *it;
      for (set<Rule*>::iterator it2 = p->rules.begin();
           it2 != p->rules.end(); ++it2) {
        answer.insert(*it2);
      }
    }
    return answer;
  }

  // Given a possible set of premises, come up with all the
  // Deductions and add them to the "answer" set.  The
  // callee is responsible for deleting the Deductions.
  static void MakeDeductions(const set<Rule*>& prems, set<Deduction*>* answer) {
    int count = prems.size();
    if (count == 0) return;
    if (!PairwiseDisjoint(prems)) return;
    set<Placement*> possibilities = Union(prems);

    // Now we need to find a list of conclusions that span
    // the Placements we have.
    set<Rule*> candidates = AllRules(possibilities);

    for (Odometer<Rule> odom(candidates, count); !(odom.finished()); ++odom) {
      Deduction* d = new Deduction();
      d->premises = prems;
      d->conclusions = odom.currentValue();
      d->possibilities = possibilities;
      set<Placement*> span = Union(d->conclusions);
      if (IsSubset(possibilities, span)) {
        // yay!  This is a possible deduction.
        for (set<Placement*>::iterator it = span.begin();
             it != span.end(); ++it) {
          if (Twice(*it, d->conclusions)) {
            d->overloads.insert(*it);
            if (possibilities.find(*it) != possibilities.end()) {
              d->possibilities.erase(*it);
            }
          } else if (possibilities.find(*it) == possibilities.end()) {
            d->impossibilities.insert(*it);
          }
        }
      }
      // the Deduction is only useful if there are actually
      // are impossiblities or overloads.
      if (d->overloads.size() + d->impossibilities.size() > 0) {
        answer->insert(d);
      } else {
        delete d;
      }
    }
  }
};

void Placement::Negate() {
  assert(rules.size() > 0);
  for (set<Rule*>::iterator it = rules.begin();
       it != rules.end(); ++it) {
    (*it)->Negate(this);
  }
  rules.clear();
}

bool Rule::CanEnslave(Rule* r) const {
  if (slave_of_ != NULL) return false;
  if (!Do::CheckIdentical(placements,r->placements)) return false;
  return true;
}

void Rule::Enslave(Rule* r) {
  assert(slave_of_ == NULL);
  assert(Do::CheckIdentical(placements,r->placements));
  // first, take all of r's copies.
  for (set<Rule*>::iterator it = r->slaves_.begin();
       it != r->slaves_.end(); ++it) {
    slaves_.insert(*it);
    (*it)->slave_of_ = this;
  }
  // next, enslave r.
  slaves_.insert(r);
  r->slave_of_ = this;
  for (set<Placement*>::iterator it = r->placements.begin();
       it != r->placements.end(); ++it) {
    (*it)->Remove(r);
  }
}

string Deduction::toString() {
  assert(size() != 0);
  string answer = "Since ";
  answer += Do::toString(premises);
  answer += " we know\n    ";
  char s[10];
  sprintf(s, "%d", size());
  answer += s;
  answer += " of ";
  answer += Do::toString(possibilities);
  answer += " are true.\n  But those are a subset of\n    ";
  answer += Do::toString(conclusions);
  answer += ".\n  Therefore, we know that none of\n    ";
  answer += Do::toString(impossibilities);
  answer += "\n  are true.";
  if (overloads.size() > 0) {
    answer += " Also, none of ";
    answer += Do::toString(overloads);
    answer += "\n  are true because of overloading.";
  }
  return answer;
}

// A classic sudoku puzzle.
// It has:
//   9x9x9 = 729 Placements
//     (each of 9 numbers can be placed in each of 81 cells)
//   9x9 = 81 Cell Rules
//     (each of the 81 cells has one of 9 Placements)
//   9x9 = 81 Row Rules
//     (each of 9 rows has 9 RowRules)
//   9x9 = 81 Column Rules
//     (each of 9 columns has 9 ColumnRules)
//   9x9 = 81 Square Rules
//     (each of 9 square regions has 9 SquareRules)
//   (324 Rules total)
  
class ClassicSudokuPuzzle {
 public:
  ClassicSudokuPuzzle() {
    for (int row=0; row<9; row++) {
      for (int col=0; col<9; col++) {
        getRulePointer(CELL, row, col)->setName(CELL, row, col);
        getRulePointer(ROW, row, col)->setName(ROW, row, col);
        getRulePointer(COLUMN, row, col)->setName(COLUMN, row, col);
        getRulePointer(SQUARE, row, col)->setName(SQUARE, row, col);
        for (int val=0; val<9; val++) {
          Placement* p_ptr = getPlacementPointer(row, col, val);
          p_ptr->setName(makeName(row, col, val));
          Do::Associate(p_ptr, getRulePointer(CELL, row, col));
          Do::Associate(p_ptr, getRulePointer(ROW, row, val));
          Do::Associate(p_ptr, getRulePointer(COLUMN, col, val));
          int square = (row/3) * 3 + (col/3);
          Do::Associate(p_ptr, getRulePointer(SQUARE, square, val));
        }
      }
    }
    for (int i=0; i<324; ++i) {
      assert(rules_[i].size() == 9);
    }
    for (int i=0; i<729; ++i) {
      assert(placements_[i].RuleCount() == 4);
    }
  }
  Placement* getPlacementPointer(int row, int col, int val) {
    return(placements_ + (row*81) + (col*9) + val);
  }
  string makeName(int row, int col, int val) {
    string s = "";
    s += (char)(val+(int)('1'));
    s += (char)(row+(int)('A'));
    s += (char)(col+(int)('J'));
    return s;
  }
  Rule* getRulePointer(RuleType type, int index, int val) {
    if (type == CELL)
      // for cells, index == row and val == column
      return((Rule*)(rules_ + 0 + (index*9) + val));
    if (type == ROW)
      return((Rule*)(rules_ + 81 + (index*9) + val));
    if (type == COLUMN)
      return((Rule*)(rules_ + 2*81 + (index*9) + val));
    if (type == SQUARE)
      return((Rule*)(rules_ + 3*81 + (index*9) + val));
  }
  void Force(int row, int col, int val) {
    for (int i=0; i<9; ++i) {
      if (i == val) continue;
      getPlacementPointer(row,col,i)->Negate();
    }
  }
  void RowForce(int row, int c0, int c1, int c2,
                         int c3, int c4, int c5,
                         int c6, int c7, int c8) {
    if (c0 >=0 && c0 <=8) Force(row, 0, c0);
    if (c1 >=0 && c1 <=8) Force(row, 1, c1);
    if (c2 >=0 && c2 <=8) Force(row, 2, c2);
    if (c3 >=0 && c3 <=8) Force(row, 3, c3);
    if (c4 >=0 && c4 <=8) Force(row, 4, c4);
    if (c5 >=0 && c5 <=8) Force(row, 5, c5);
    if (c6 >=0 && c6 <=8) Force(row, 6, c6);
    if (c7 >=0 && c7 <=8) Force(row, 7, c7);
    if (c8 >=0 && c8 <=8) Force(row, 8, c8);
  }
  void Print() {
    cout << "      J       K       L       M       N       O       P       Q       R\n";
    for (int row=0;row<9*3;row++) {
      if (row % 3 == 0) {
        cout << "  +-------+-------+-------+-------+-------+-------+-------+-------+-------+\n  ";
      } else if (row % 3 == 1) {
        cout << (char)(row/3 + (int)'A') << " ";
      } else {
        cout << "  ";
      }
      for (int col=0;col<9*3;col++) {
        if (col % 3 == 0) {
          cout << "| ";
        }
        int cellrow = (row/3);
        int cellcol = (col/3);
        int value = (row%3) * 3 + (col%3);
        if (getPlacementPointer(cellrow, cellcol, value)->isPossible()) {
          cout << (value+1);
        } else {
          cout << " ";
        }
        cout << " ";
      }
      cout << "|\n";
    }
    cout << "  +-------+-------+-------+-------+-------+-------+-------+-------+-------+\n";
    cout << "\n";
  }
  set<Deduction*> GetSingleDeductions(bool show) {
    set<Deduction*> ds;
    for (int i=0; i<324; ++i) {
      if (rules_[i].isSlave()) continue;
      set<Rule*> foo;
      foo.insert(rules_ + i);
      Do::MakeDeductions(foo, &ds);
    }
    if (show) {
      cout << ds.size() << " Deductions found:\n";
      int index = 1;
      for (set<Deduction*>::iterator it = ds.begin();
           it != ds.end(); ++it) {
        cout << index << ". " << (*it)->toString() << "\n";
        index++;
      }
    }
    return ds;
  }
  set<Deduction*> GetDoubleDeductions(bool show) {
    set<Deduction*> ds;
    for (int i=0; i<324; ++i) for (int j=i+1; j<324; ++j) {
      if (rules_[i].isSlave()) continue;
      if (rules_[j].isSlave()) continue;
      set<Rule*> foo;
      foo.insert(rules_ + i);
      foo.insert(rules_ + j);
      Do::MakeDeductions(foo, &ds);
    }
    if (show) {
      cout << ds.size() << " Deductions found:\n";
      int index = 1;
      for (set<Deduction*>::iterator it = ds.begin();
           it != ds.end(); ++it) {
        cout << index << ". " << (*it)->toString() << "\n";
        index++;
      }
    }
    return ds;
  }
  void CleanUp(set<Deduction*> s) {
    for (set<Deduction*>::iterator it = s.begin();
         it != s.end(); ++it) {
      delete(*it);
    }
  }
  void Slavery(bool show) {
    // Finds rules that can enslave each other, and does so.
    if (show) {
      cout << "...Looking for slaves...\n";
    }
    for (int i=0; i<324; i++) for (int j=i+1; j<324; j++) {
      if (rules_[i].isSlave()) continue;
      if (rules_[j].isSlave()) continue;
      if (rules_[i].CanEnslave(rules_ + j)) {
        rules_[i].Enslave(rules_ + j);
        if (show) {
          cout << rules_[i].toString() << " will enslave "
               << rules_[j].toString() << "\n";
        }
      }
    }
    if (show) {
      cout << "...stopped looking for slaves...\n";
    }
  }
  void SolveUpToOneDeep(bool show) {
    set<Deduction*> ds = GetSingleDeductions(show);
    while (ds.size() > 0) {
      if (show) {
        cout << "Choosing the first deduction to implement...\n";
      }
      (*ds.begin())->Implement();
      Print();
      CleanUp(ds);
      ds.clear();
      Slavery(show);
      ds = GetSingleDeductions(show);
    }
    if (show) {
      cout << "No more single-deep deductions can be made.\n";
    }
  }
  void SolveUpToOneDeepInParallel(bool show) {
    set<Deduction*> ds = GetSingleDeductions(show);
    while (ds.size() > 0) {
      if (show) {
        cout << "Implementing ALL deductions...\n";
      }
      for (set<Deduction*>::iterator it = ds.begin();
           it != ds.end(); ++it) {
        (*it)->Implement();
      }
      Print();
      CleanUp(ds);
      ds.clear();
      Slavery(show);
      Print();
      ds = GetSingleDeductions(show);
    }
    if (show) {
      cout << "No more single-deep deductions can be made.\n";
    }
  }
 private:
  Placement placements_[729];
  Rule rules_[324];
};

int main() {
  ClassicSudokuPuzzle c;
  int x = -1;
  c.RowForce(0,8,4,x,2,3,7,6,x,x);
  c.RowForce(1,x,x,x,x,x,8,4,2,3);
  c.RowForce(2,3,2,0,x,6,4,x,x,x);
  c.RowForce(3,4,0,2,x,5,x,x,6,x);
  c.RowForce(4,6,3,x,7,2,0,x,5,4);
  c.RowForce(5,x,5,x,x,4,6,0,x,2);
  c.RowForce(6,x,x,x,x,7,2,5,x,x);
  c.RowForce(7,2,7,x,6,x,x,x,x,x);
  c.RowForce(8,x,x,3,4,x,x,2,7,6);

  c.Print();
//  c.SolveUpToOneDeepInParallel(true);
  c.SolveUpToOneDeep(true);
}