From 18eb009672398d6155ecc246a618a059b8d79005 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Wed, 12 Jul 2017 13:28:16 -0700
Subject: [PATCH] Don't generate redundant constraints

---
 src/Backend/satelemencoder.c | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Backend/satelemencoder.c b/src/Backend/satelemencoder.c
index facb374..38d5398 100644
--- a/src/Backend/satelemencoder.c
+++ b/src/Backend/satelemencoder.c
@@ -99,8 +99,8 @@ void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
 	allocElementConstraintVariables(encoding, encoding->encArraySize);
 	getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);	
 	for(uint i=0;i<encoding->numVars;i++) {
-		for(uint j=0;j<encoding->numVars;j++) {
-			addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf, encoding->variables[i], constraintNegate(encoding->variables[j])));
+		for(uint j=i+1;j<encoding->numVars;j++) {
+			addConstraintCNF(This->cnf, constraintNegate(constraintAND2(This->cnf, encoding->variables[i], encoding->variables[j])));
 		}
 	}
 	addConstraintCNF(This->cnf, constraintOR(This->cnf, encoding->numVars, encoding->variables));
-- 
2.34.1