Don't generate redundant constraints

diff --git a/src/Backend/satelemencoder.c b/src/Backend/satelemencoder.c
index facb374f189c7100fe82bbfdc8ba904f52e98b91..38d539873d957cd7d223b3a4575c354f2165577a 100644 (file)
--- 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));