sat: satget: don't duplicate binary clauses

This commit is contained in:
aiju 2018-03-22 13:35:52 +00:00
parent 8389465f94
commit 39dd26bf08

View file

@ -18,7 +18,7 @@ satget(SATSolve *s, int i, int *t, int n)
}
for(l = s->lit; l < s->lit + 2 * s->nvar; l++)
for(k = 0; k < l->nbimp; k++)
if(i-- == 0){
if(l - s->lit < l->bimp[k] && i-- == 0){
if(n > 0) t[0] = -signf(l - s->lit);
if(n > 1) t[1] = signf(l->bimp[k]);
return 2;