From: bdemsky <bdemsky@uci.edu>
Date: Wed, 12 Jul 2017 20:28:16 +0000 (-0700)
Subject: Don't generate redundant constraints
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=18eb009672398d6155ecc246a618a059b8d79005;p=satune.git

Don't generate redundant constraints
---

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));