Adding the symmetry breaking constraint to the original encoding

diff --git a/nqueens/nqueens.cc b/nqueens/nqueens.cc
index 24f452333efdaa9db4b877aa86bbad37924bb0a6..e4eb1ab3c1c07cb406ae3c0b0477e967cd933603 100644 (file)
--- a/nqueens/nqueens.cc
+++ b/nqueens/nqueens.cc
@@ -30,6 +30,29 @@ void EqualOneToCNF(vector<int> literals, vector< vector<int> > & cnf){
        }
 }
 
+void verticalSymmetryBreaking(vector<int> col1, vector<int> colN, vector<vector<int> > &cnf){
+       vector<int> dnf;
+       for(int i=0; i<col1.size(); i++){
+               dnf.push_back(-col1[i]);
+               for(int j=i+1; j<colN.size(); j++){
+                       dnf.push_back(colN[j]);
+               }
+               cnf.push_back(dnf);
+               dnf.clear();
+       }
+               
+
+}
+
+void Or( vector<int> literals, vector<vector<int> > & cnf){
+       int N= literals.size();
+       vector<int> dnf;
+       for( int i=0; i<N; i++){
+               dnf.push_back(literals[i]);
+       }
+       cnf.push_back(dnf);
+}
+
 void LessEqualOneToCNF(vector<int> literals, vector< vector<int> > & cnf){
        int N = literals.size();
        vector<int> dnf; 
@@ -186,7 +209,19 @@ void originalNqueensEncoding(int N){
                LessEqualOneToCNF(vars, cnf);
                vars.clear();
        }
-       
+
+       //Symmetry breaking constraint
+       for (int i=0; i<N/2; i++){
+               vars.push_back(VarName[0][i]);
+       }
+       Or(vars, cnf);
+       vector<int> lastCol;
+       for(int i=0; i<N; i++){
+               lastCol.push_back(VarName[N-1][i]);
+       }
+       verticalSymmetryBreaking(vars, lastCol, cnf);
+       vars.clear();
+       //That's it ... Let's solve the problem ...
        IncrementalSolver *solver =allocIncrementalSolver();
        
        for (int i=0; i<cnf.size(); i++){