From af98520a7d233668a0a91a6bb53b2abd01dd5d56 Mon Sep 17 00:00:00 2001
From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Sat, 4 Aug 2018 16:23:44 -0700
Subject: [PATCH] Symmetry breaking constraint for CSolver encoding

---
 nqueens/nqueens.cc | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/nqueens/nqueens.cc b/nqueens/nqueens.cc
index e4eb1ab3..bed871ab 100644
--- a/nqueens/nqueens.cc
+++ b/nqueens/nqueens.cc
@@ -441,6 +441,26 @@ void diagonallyDifferentConstraintBothDir(CSolver *solver, int N, vector<Element
 	diagonallyDifferentConstraint(solver, N, elems);
 } 
 
+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);
+	Element *e1x = elems[0];
+	Element *e2x = elems[N-1];
+	Element *inputs2 [] = {e1x, e2x};
+	BooleanEdge equals = solver->applyPredicate(lt, inputs2, 2);
+	solver->addConstraint(equals);
+
+}
 
 void csolverNQueens(int N, bool serialize=false){
 	if(N <=1){
@@ -460,6 +480,7 @@ void csolverNQueens(int N, bool serialize=false){
 	mustHaveValueConstraint(solver, elems);
 	generateRowConstraints(solver, N, elems);
 	diagonallyDifferentConstraintBothDir(solver, N, elems);
+	symmetryBreakingConstraint(solver, N, elems);
 //	solver->printConstraints();
 	if(serialize){
 		solver->serialize();
-- 
2.34.1