From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Sat, 4 Aug 2018 21:59:45 +0000 (-0700)
Subject: Adding the symmetry breaking constraint to the original encoding
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=94f8fac018d5abd8afcb9590e6ac3d19587ed47a;p=Benchmarks_CSolver.git

Adding the symmetry breaking constraint to the original encoding
---

diff --git a/nqueens/nqueens.cc b/nqueens/nqueens.cc
index 24f45233..e4eb1ab3 100644
--- 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++){