Symmetry breaking constraint for CSolver encoding

diff --git a/nqueens/nqueens.cc b/nqueens/nqueens.cc
index e4eb1ab3c1c07cb406ae3c0b0477e967cd933603..bed871abdc5966baf3fed47bc9f4a8744cb0c492 100644 (file)
--- 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();