00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019 #include <cstdio>
00020 #include <map>
00021
00022 #include "base/commandlineflags.h"
00023 #include "base/commandlineflags.h"
00024 #include "base/integral_types.h"
00025 #include "base/logging.h"
00026 #include "base/scoped_ptr.h"
00027 #include "base/stringprintf.h"
00028 #include "base/map-util.h"
00029 #include "constraint_solver/constraint_solveri.h"
00030
00031 DEFINE_bool(print, false, "If true, print one of the solution.");
00032 DEFINE_bool(print_all, false, "If true, print all the solutions.");
00033 DEFINE_int32(nb_loops, 1,
00034 "Number of solving loops to perform, for performance timing.");
00035 DEFINE_int32(size, 0,
00036 "Size of the problem. If equal to 0, will test several increasing sizes.");
00037 DEFINE_bool(use_symmetry, false, "Use Symmetry Breaking methods");
00038 DECLARE_bool(cp_no_solve);
00039
00040 static const int kNumSolutions[] = {
00041 1, 0, 0, 2, 10, 4, 40, 92, 352, 724,
00042 2680, 14200, 73712, 365596, 2279184
00043 };
00044 static const int kKnownSolutions = 15;
00045
00046 static const int kNumUniqueSolutions[] = {
00047 1, 0, 0, 1, 2, 1, 6, 12, 46, 92, 341, 1787, 9233, 45752,
00048 285053, 1846955, 11977939, 83263591, 621012754
00049 };
00050 static const int kKnownUniqueSolutions = 19;
00051
00052 namespace operations_research {
00053
00054 class NQueenSymmetry : public SymmetryBreaker {
00055 public:
00056 NQueenSymmetry(Solver* const s, const std::vector<IntVar*>& vars)
00057 : solver_(s), vars_(vars), size_(vars.size()) {
00058 for (int i = 0; i < size_; ++i) {
00059 indices_[vars[i]] = i;
00060 }
00061 }
00062 virtual ~NQueenSymmetry() {}
00063
00064 protected:
00065 int Index(IntVar* const var) const {
00066 return FindWithDefault(indices_, var, -1);
00067 }
00068 IntVar* Var(int index) const {
00069 DCHECK_GE(index, 0);
00070 DCHECK_LT(index, size_);
00071 return vars_[index];
00072 }
00073 int size() const { return size_; }
00074 int symmetric(int index) const { return size_ - 1 - index; }
00075 Solver* const solver() const { return solver_; }
00076
00077 private:
00078 Solver* const solver_;
00079 const std::vector<IntVar*> vars_;
00080 std::map<IntVar*, int> indices_;
00081 const int size_;
00082 };
00083
00084
00085 class SX : public NQueenSymmetry {
00086 public:
00087 SX(Solver* const s, const std::vector<IntVar*>& vars) : NQueenSymmetry(s, vars) {}
00088 virtual ~SX() {}
00089
00090 virtual void VisitSetVariableValue(IntVar* const var, int64 value) {
00091 const int index = Index(var);
00092 IntVar* const other_var = Var(symmetric(index));
00093 AddIntegerVariableEqualValueClause(other_var, value);
00094 }
00095 };
00096
00097
00098 class SY : public NQueenSymmetry {
00099 public:
00100 SY(Solver* const s, const std::vector<IntVar*>& vars) : NQueenSymmetry(s, vars) {}
00101 virtual ~SY() {}
00102
00103 virtual void VisitSetVariableValue(IntVar* const var, int64 value) {
00104 AddIntegerVariableEqualValueClause(var, symmetric(value));
00105 }
00106 };
00107
00108
00109 class SD1 : public NQueenSymmetry {
00110 public:
00111 SD1(Solver* const s, const std::vector<IntVar*>& vars) : NQueenSymmetry(s, vars) {}
00112 virtual ~SD1() {}
00113
00114 virtual void VisitSetVariableValue(IntVar* const var, int64 value) {
00115 const int index = Index(var);
00116 IntVar* const other_var = Var(value);
00117 AddIntegerVariableEqualValueClause(other_var, index);
00118 }
00119 };
00120
00121
00122 class SD2 : public NQueenSymmetry {
00123 public:
00124 SD2(Solver* const s, const std::vector<IntVar*>& vars) : NQueenSymmetry(s, vars) {}
00125 virtual ~SD2() {}
00126
00127 virtual void VisitSetVariableValue(IntVar* const var, int64 value) {
00128 const int index = Index(var);
00129 IntVar* const other_var = Var(symmetric(value));
00130 AddIntegerVariableEqualValueClause(other_var, symmetric(index));
00131 }
00132 };
00133
00134
00135 class R90 : public NQueenSymmetry {
00136 public:
00137 R90(Solver* const s, const std::vector<IntVar*>& vars) : NQueenSymmetry(s, vars) {}
00138 virtual ~R90() {}
00139
00140 virtual void VisitSetVariableValue(IntVar* const var, int64 value) {
00141 const int index = Index(var);
00142 IntVar* const other_var = Var(value);
00143 AddIntegerVariableEqualValueClause(other_var, symmetric(index));
00144 }
00145 };
00146
00147
00148 class R180 : public NQueenSymmetry {
00149 public:
00150 R180(Solver* const s, const std::vector<IntVar*>& vars)
00151 : NQueenSymmetry(s, vars) {}
00152 virtual ~R180() {}
00153
00154 virtual void VisitSetVariableValue(IntVar* const var, int64 value) {
00155 const int index = Index(var);
00156 IntVar* const other_var = Var(symmetric(index));
00157 AddIntegerVariableEqualValueClause(other_var, symmetric(value));
00158 }
00159 };
00160
00161
00162 class R270 : public NQueenSymmetry {
00163 public:
00164 R270(Solver* const s, const std::vector<IntVar*>& vars)
00165 : NQueenSymmetry(s, vars) {}
00166 virtual ~R270() {}
00167
00168 virtual void VisitSetVariableValue(IntVar* const var, int64 value) {
00169 const int index = Index(var);
00170 IntVar* const other_var = Var(symmetric(value));
00171 AddIntegerVariableEqualValueClause(other_var, index);
00172 }
00173 };
00174
00175 void CheckNumberOfSolutions(int size, int num_solutions) {
00176 if (FLAGS_use_symmetry) {
00177 if (size - 1 < kKnownUniqueSolutions) {
00178 CHECK_EQ(num_solutions, kNumUniqueSolutions[size - 1]);
00179 } else if (!FLAGS_cp_no_solve) {
00180 CHECK_GT(num_solutions, 0);
00181 }
00182 } else {
00183 if (size - 1 < kKnownSolutions) {
00184 CHECK_EQ(num_solutions, kNumSolutions[size - 1]);
00185 } else if (!FLAGS_cp_no_solve) {
00186 CHECK_GT(num_solutions, 0);
00187 }
00188 }
00189 }
00190
00191 void NQueens(int size) {
00192 CHECK_GE(size, 1);
00193 Solver s("nqueens");
00194
00195
00196 std::vector<IntVar*> queens;
00197 for (int i = 0; i < size; ++i) {
00198 queens.push_back(s.MakeIntVar(0, size - 1, StringPrintf("queen%04d", i)));
00199 }
00200 s.AddConstraint(s.MakeAllDifferent(queens));
00201
00202 std::vector<IntVar*> vars(size);
00203 for (int i = 0; i < size; ++i) {
00204 vars[i] = s.MakeSum(queens[i], i)->Var();
00205 }
00206 s.AddConstraint(s.MakeAllDifferent(vars));
00207 for (int i = 0; i < size; ++i) {
00208 vars[i] = s.MakeSum(queens[i], -i)->Var();
00209 }
00210 s.AddConstraint(s.MakeAllDifferent(vars));
00211
00212 SolutionCollector* const solution_counter = s.MakeAllSolutionCollector(NULL);
00213 SolutionCollector* const collector = s.MakeFirstSolutionCollector();
00214 collector->Add(queens);
00215 std::vector<SearchMonitor*> monitors;
00216 monitors.push_back(solution_counter);
00217 monitors.push_back(collector);
00218 DecisionBuilder* const db = s.MakePhase(queens,
00219 Solver::CHOOSE_FIRST_UNBOUND,
00220 Solver::ASSIGN_MIN_VALUE);
00221 if (FLAGS_use_symmetry) {
00222 std::vector<SymmetryBreaker*> breakers;
00223 NQueenSymmetry* const sx = s.RevAlloc(new SX(&s, queens));
00224 breakers.push_back(sx);
00225 NQueenSymmetry* const sy = s.RevAlloc(new SY(&s, queens));
00226 breakers.push_back(sy);
00227 NQueenSymmetry* const sd1 = s.RevAlloc(new SD1(&s, queens));
00228 breakers.push_back(sd1);
00229 NQueenSymmetry* const sd2 = s.RevAlloc(new SD2(&s, queens));
00230 breakers.push_back(sd2);
00231 NQueenSymmetry* const r90 = s.RevAlloc(new R90(&s, queens));
00232 breakers.push_back(r90);
00233 NQueenSymmetry* const r180 = s.RevAlloc(new R180(&s, queens));
00234 breakers.push_back(r180);
00235 NQueenSymmetry* const r270 = s.RevAlloc(new R270(&s, queens));
00236 breakers.push_back(r270);
00237 SearchMonitor* const symmetry_manager = s.MakeSymmetryManager(breakers);
00238 monitors.push_back(symmetry_manager);
00239 }
00240
00241 for (int loop = 0; loop < FLAGS_nb_loops; ++loop) {
00242 s.Solve(db, monitors);
00243 CheckNumberOfSolutions(size, solution_counter->solution_count());
00244 }
00245
00246 const int num_solutions = solution_counter->solution_count();
00247 if (num_solutions > 0 && size < kKnownSolutions) {
00248 int print_max = FLAGS_print_all ? num_solutions : FLAGS_print ? 1 : 0;
00249 for (int n = 0; n < print_max; ++n) {
00250 printf("--- solution #%d\n", n);
00251 for (int i = 0; i < size; ++i) {
00252 const int pos = static_cast<int>(collector->Value(n, queens[i]));
00253 for (int k = 0; k < pos; ++k) printf(" . ");
00254 printf("%2d ", i);
00255 for (int k = pos + 1; k < size; ++k) printf(" . ");
00256 printf("\n");
00257 }
00258 }
00259 }
00260 printf("========= number of solutions:%d\n", num_solutions);
00261 printf(" number of failures: %lld\n", s.failures());
00262 }
00263 }
00264
00265 int main(int argc, char **argv) {
00266 google::ParseCommandLineFlags(&argc, &argv, true);
00267 if (FLAGS_size != 0) {
00268 operations_research::NQueens(FLAGS_size);
00269 } else {
00270 for (int n = 1; n < 12; ++n) {
00271 operations_research::NQueens(n);
00272 }
00273 }
00274 return 0;
00275 }