Skip to content

Commit

Permalink
simplify Commander encoding
Browse files Browse the repository at this point in the history
Simon Felix committed Feb 26, 2024
1 parent f1acd67 commit 6b95f66
Showing 1 changed file with 4 additions and 5 deletions.
9 changes: 4 additions & 5 deletions SATInterface/Model.cs
Original file line number Diff line number Diff line change
@@ -1636,7 +1636,8 @@ public BoolExpr ExactlyOneOf(ReadOnlySpan<BoolExpr> _expr, ExactlyOneOfMethod? _
return uc[0] & !uc[1];
}
else
return ExactlyOneOfPairwiseTree(expr);
//return ExactlyOneOfPairwiseTree(expr);
return ExactlyOneOfCommander(expr);
case ExactlyOneOfMethod.SortTotalizer:
return ExactlyKOf(expr.ToArray(), 1, KOfMethod.SortTotalizer);
case ExactlyOneOfMethod.SortPairwise:
@@ -2010,15 +2011,13 @@ private BoolExpr ExactlyOneOfCommander(ReadOnlySpan<BoolExpr> _expr)
commanders[i] = groups[i].Single();
else
{
commanders[i] = AddVar();

//1
for (var j = 0; j < groups[i].Length; j++)
for (var k = j + 1; k < groups[i].Length; k++)
valid.Add(OrExpr.Create(!groups[i][j], !groups[i][k]).Flatten());

AddConstr((!commanders[i]) | OrExpr.Create(groups[i])); //2
AddConstr(commanders[i] | (!OrExpr.Create(groups[i]))); //3
//2 3
commanders[i] = OrExpr.Create(groups[i]).Flatten();
}

valid.Add(ExactlyOneOfCommander(commanders).Flatten());

0 comments on commit 6b95f66

Please sign in to comment.