From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Thu, 26 Jul 2018 19:49:05 +0000 (-0700)
Subject: Bug fix for onehot encoding
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=b4325ff489cde93c72be32c7159398cd85761ad2;p=Benchmarks_CSolver.git

Bug fix for onehot encoding
---

diff --git a/nqueens/nqueens.cc b/nqueens/nqueens.cc
index 657f005e..18d7c6a6 100644
--- a/nqueens/nqueens.cc
+++ b/nqueens/nqueens.cc
@@ -312,6 +312,12 @@ void atmostOneConstraint(CSolver *solver, vector<BooleanEdge> &constraints){
 	}
 }
 
+void mustHaveValueConstraint(CSolver* solver, vector<Element*> &elems){
+	for(int i=0; i<elems.size(); i++){
+		solver->mustHaveValue(elems[i]);
+	}
+}
+
 void differentInEachRow(CSolver* solver, int N, vector<Element*> &elems){
 	Predicate *eq = solver->createPredicateOperator(SATC_EQUALS);
 	for(int i=0; i<N-1; i++){
@@ -388,7 +394,7 @@ void csolverNQueens(int N){
 	for(int i=0; i<N; i++){
 		elems.push_back(solver->getElementVar(domainSet));
 	}
-	
+	mustHaveValueConstraint(solver, elems);
 	differentInEachRow(solver, N, elems);
 	diagonallyDifferentConstraintBothDir(solver, N, elems);
 //	solver->printConstraints();