From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Sun, 5 Aug 2018 01:57:46 +0000 (-0700)
Subject: bug fix for odd-size tables
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=865d4ae30f50525a2ebd793267f130cfc81a4571;p=Benchmarks_CSolver.git

bug fix for odd-size tables
---

diff --git a/nqueens/nqueens.cc b/nqueens/nqueens.cc
index bed871ab..616600eb 100644
--- a/nqueens/nqueens.cc
+++ b/nqueens/nqueens.cc
@@ -211,7 +211,8 @@ void originalNqueensEncoding(int N){
 	}
 
 	//Symmetry breaking constraint
-	for (int i=0; i<N/2; i++){
+	int mid = 1+ ((N-1)/2);
+	for (int i=0; i<mid; i++){
 		vars.push_back(VarName[0][i]);
 	}
 	Or(vars, cnf);
@@ -442,20 +443,14 @@ void diagonallyDifferentConstraintBothDir(CSolver *solver, int N, vector<Element
 } 
 
 void symmetryBreakingConstraint(CSolver *solver, int N, vector<Element*>& elems){
-	Predicate *eq = solver->createPredicateOperator(SATC_EQUALS);
-	vector<BooleanEdge> constr;
-	for(int i=0; i<N/2; i++){
-		Element *e1x = elems[0];
-		Element *e2x = solver->getElementConst(2, (uint64_t)i);
-		Element *inputs2 [] = {e1x, e2x};
-		BooleanEdge equals = solver->applyPredicate(eq, inputs2, 2);
-		constr.push_back( equals);
-	}
-	solver->addConstraint(solver->applyLogicalOperation(SATC_OR, &constr[0], constr.size()) );
-	
 	Predicate *lt = solver->createPredicateOperator(SATC_LT);
+	int mid = N/2 + N%2;
 	Element *e1x = elems[0];
-	Element *e2x = elems[N-1];
+	Element *e2x = solver->getElementConst(2, mid);
+	Element *inputs [] = {e1x, e2x};
+	solver->addConstraint(solver->applyPredicate(lt, inputs, 2));
+	
+	e2x = elems[N-1];
 	Element *inputs2 [] = {e1x, e2x};
 	BooleanEdge equals = solver->applyPredicate(lt, inputs2, 2);
 	solver->addConstraint(equals);