Skip to content

Commit

Permalink
PHF for LE constrs
Browse files Browse the repository at this point in the history
  • Loading branch information
Simon Felix committed Sep 24, 2023
1 parent 3b14b14 commit 13ccd11
Show file tree
Hide file tree
Showing 3 changed files with 159 additions and 51 deletions.
6 changes: 3 additions & 3 deletions SATInterface/Configuration.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -197,10 +197,10 @@ internal void Validate()

/// <summary>
/// The maximum number of variables for which linear constraints are encoded
/// using Totalizer or sequentially. Both grow quadratically.
/// using Totalizer.
///
/// Default: 16
/// Default: 32
/// </summary>
public int LinExprKOfLimit = 16;
public int LinExprKOfLimit = 32;
}
}
106 changes: 85 additions & 21 deletions SATInterface/LinExpr.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -328,6 +328,10 @@ private void ClearCached()

public static BoolExpr operator <=(LinExpr _a, T _b)
{
//TODO: Asín, R., Nieuwenhuis, R., Oliveras, A. and Rodríguez-Carbonell, E., 2011. Cardinality networks: a theoretical and empirical study. Constraints, 16, pp.195-221.

//TODO: https://ii.uni.wroc.pl/~karp/thesis.pdf, page 73pdf

if (_a.UB <= _b)
return Model.True;
if (_a.LB > _b)
Expand Down Expand Up @@ -418,16 +422,13 @@ private static BoolExpr UncachedLE(LinExpr _a, T _b)
minAbsWeight = absWeight;
if (absWeight > rhs)
{
//TODO: simplify
var vWithout = new LinExpr()
{
Model = _a.Model
};
foreach (var wi in _a.Weights)
if (wi.Value > T.Zero && wi.Value <= rhs)
vWithout.AddTerm(_a.Model.GetVariable(wi.Key), wi.Value);
else if (wi.Value < T.Zero && -wi.Value <= rhs)
vWithout.AddTerm(_a.Model.GetVariable(-wi.Key), -wi.Value);
if (T.Abs(wi.Value) <= rhs)
vWithout.AddTerm(_a.Model.GetVariable(wi.Value > T.Zero ? wi.Key : -wi.Key), T.Abs(wi.Value));

return _a.Model.And(_a.Weights
.Where(w => T.Abs(w.Value) > rhs)
Expand Down Expand Up @@ -499,10 +500,10 @@ private static BoolExpr UncachedLE(LinExpr _a, T _b)
if (ub <= T.CreateChecked(_a.Model.Configuration.LinExprKOfLimit))
return _a.Model.AtMostKOf(_a.Weights.SelectMany(w => Enumerable.Repeat(_a.Model.GetVariable(w.Value > T.Zero ? w.Key : -w.Key), int.CreateChecked(T.Abs(w.Value)))), int.CreateChecked(rhs), Model.KOfMethod.SortTotalizer);

if (rhs <= T.CreateChecked(_a.Model.Configuration.LinExprKOfLimit))
return _a.Model.AtMostKOf(_a.Weights.SelectMany(w => Enumerable.Repeat(_a.Model.GetVariable(w.Value > T.Zero ? w.Key : -w.Key), int.CreateChecked(T.Abs(w.Value)))), int.CreateChecked(rhs), Model.KOfMethod.Sequential);
//if (rhs <= T.CreateChecked(_a.Model.Configuration.LinExprKOfLimit))
// return _a.Model.AtMostKOf(_a.Weights.SelectMany(w => Enumerable.Repeat(_a.Model.GetVariable(w.Value > T.Zero ? w.Key : -w.Key), int.CreateChecked(T.Abs(w.Value)))), int.CreateChecked(rhs), Model.KOfMethod.Sequential);

if (false && maxVarCnt < 16 && (ub - (T.Abs(maxVar.Value) * (maxVarCnt + 1)) <= rhs))
if (maxVarCnt < 8)
{
var maxVars = new List<BoolExpr>(maxVarCnt);
var withoutMaxVars = new LinExpr();
Expand All @@ -521,10 +522,28 @@ private static BoolExpr UncachedLE(LinExpr _a, T _b)
}
else
{
//TODO: implement section 5 with r=2k and c=1 of Ben-Haim, Y., Ivrii, A., Margalit, O. and Matsliah, A., 2012, June. Perfect hashing and CNF encodings of cardinality constraints. In International Conference on Theory and Applications of Satisfiability Testing (pp. 397-409). Berlin, Heidelberg: Springer Berlin Heidelberg.
try
{
_a.Model.StartStatistics("LE Bit", _a.Weights.Count);

//Debug.WriteLine($"Binary");
return _a.ToUInt(_a.Model) <= rhs;
if (rhs * 2 <= _a.Model.Configuration.LinExprKOfLimit)
{
//Ben-Haim, Y., Ivrii, A., Margalit, O. and Matsliah, A., 2012, June. Perfect hashing and CNF encodings of cardinality constraints. In International Conference on Theory and Applications of Satisfiability Testing (pp. 397-409). Berlin, Heidelberg: Springer Berlin Heidelberg.
var varForY = Enumerable.Range(0, int.CreateChecked(rhs) * 2).Select(i => new List<BoolExpr>()).ToArray();
{
var i = 0;
foreach (var v in _a.Weights.SelectMany(w => Enumerable.Repeat(_a.Model.GetVariable(w.Value > T.Zero ? w.Key : -w.Key), int.CreateChecked(T.Abs(w.Value)))))
varForY[i++ % varForY.Length].Add(v);
}
return (_a.Model.AtMostKOf(varForY.Select(l => _a.Model.Or(l)), int.CreateChecked(rhs), Model.KOfMethod.SortTotalizer)) & (_a.ToUInt(_a.Model) <= rhs);
}
else
return _a.ToUInt(_a.Model) <= rhs;
}
finally
{
_a.Model.StopStatistics("LE Bit");
}
}
}

Expand Down Expand Up @@ -1143,16 +1162,13 @@ private static BoolExpr UncachedEq(LinExpr _a, T _b)
minAbsWeight = absWeight;
if (absWeight > rhs)
{
//TODO: simplify
var vWithout = new LinExpr()
{
Model = _a.Model
};
foreach (var wi in _a.Weights)
if (wi.Value > T.Zero && wi.Value <= rhs)
vWithout.AddTerm(_a.Model.GetVariable(wi.Key), wi.Value);
else if (wi.Value < T.Zero && -wi.Value <= rhs)
vWithout.AddTerm(_a.Model.GetVariable(-wi.Key), -wi.Value);
if (T.Abs(wi.Value) <= rhs)
vWithout.AddTerm(_a.Model.GetVariable(wi.Value > T.Zero ? wi.Key : -wi.Key), T.Abs(wi.Value));

return _a.Model.And(_a.Weights
.Where(w => T.Abs(w.Value) > rhs)
Expand Down Expand Up @@ -1221,10 +1237,10 @@ private static BoolExpr UncachedEq(LinExpr _a, T _b)
if (ub <= T.CreateChecked(_a.Model.Configuration.LinExprKOfLimit))
return _a.Model.ExactlyKOf(_a.Weights.SelectMany(w => Enumerable.Repeat(_a.Model.GetVariable(w.Value > T.Zero ? w.Key : -w.Key), int.CreateChecked(T.Abs(w.Value)))), int.CreateChecked(rhs), Model.KOfMethod.SortTotalizer);

if (rhs <= T.CreateChecked(_a.Model.Configuration.LinExprKOfLimit))
return _a.Model.ExactlyKOf(_a.Weights.SelectMany(w => Enumerable.Repeat(_a.Model.GetVariable(w.Value > T.Zero ? w.Key : -w.Key), int.CreateChecked(T.Abs(w.Value)))), int.CreateChecked(rhs), Model.KOfMethod.Sequential);
//if (rhs <= T.CreateChecked(_a.Model.Configuration.LinExprKOfLimit))
// return _a.Model.ExactlyKOf(_a.Weights.SelectMany(w => Enumerable.Repeat(_a.Model.GetVariable(w.Value > T.Zero ? w.Key : -w.Key), int.CreateChecked(T.Abs(w.Value)))), int.CreateChecked(rhs), Model.KOfMethod.Sequential);

if (maxVarCnt < 16)
if (maxVarCnt < 8)
{
var maxVars = new List<BoolExpr>(maxVarCnt);
var withoutMaxVars = new LinExpr();
Expand All @@ -1243,8 +1259,24 @@ private static BoolExpr UncachedEq(LinExpr _a, T _b)
}
else
{
//Debug.WriteLine($"Binary");
return _a.ToUInt(_a.Model) == rhs;
try
{
_a.Model.StartStatistics("Eq Bit", _a.Weights.Count);

var ands = new List<BoolExpr>
{
_a.ToUInt(_a.Model) == rhs
};

if (rhs > 3)
ands.Add(_a.EqualsMod(rhs, 3));

return _a.Model.And(ands);
}
finally
{
_a.Model.StopStatistics("Eq Bit");
}
}
}

Expand Down Expand Up @@ -1284,6 +1316,38 @@ public override string ToString()
return sb.ToString();
}

private BoolExpr EqualsMod(T _rhs, T _b)
{
Debug.Assert(Model is not null);

if (_rhs < T.Zero)
throw new ArgumentException(nameof(_rhs));
if (_b < T.One)
throw new ArgumentException(nameof(_b));

if (_b == T.One)
return Model.True;

var oldUnary = new BoolExpr[int.CreateChecked(_b)];
var newUnary = new BoolExpr[int.CreateChecked(_b)];
newUnary[0] = Model.True;
for (var i = 1; i < newUnary.Length; i++)
newUnary[i] = Model.False;

foreach (var e in Weights)
{
var rot = int.CreateChecked(T.Abs(e.Value) % _b);
if (rot == 0)
continue;

(oldUnary, newUnary) = (newUnary, oldUnary);
for (var i = 0; i < newUnary.Length; i++)
newUnary[i] = Model.ITE(Model.GetVariable(e.Value > T.Zero ? e.Key : -e.Key), oldUnary[(i + oldUnary.Length - rot) % oldUnary.Length], oldUnary[i]);
}

return newUnary[int.CreateChecked(_rhs % _b)];
}

public static BoolExpr operator !=(LinExpr _a, T _b) => !(_a == _b);
public static BoolExpr operator >(LinExpr _a, T _b) => -_a < -_b;
public static BoolExpr operator >=(LinExpr _a, T _b) => !(_a <= (_b - T.One));
Expand Down
98 changes: 71 additions & 27 deletions SATInterface/Model.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -256,8 +256,6 @@ internal VarId AllocateVar()
State = State.Undecided;

varsX.Add(false);
//if (ActiveStatKey is null && (VariableCount % 20000) == 0)
// Console.WriteLine(Environment.StackTrace);
return VariableCount;
}

Expand Down Expand Up @@ -794,6 +792,14 @@ public void Write(TextWriter _out)
/// <returns></returns>
public BoolExpr And(IEnumerable<BoolExpr> _elems) => AndExpr.Create(_elems.ToArray());

/// <summary>
/// Returns an expression equivalent to a conjunction of the supplied
/// expressions.
/// </summary>
/// <param name="_elems"></param>
/// <returns></returns>
public BoolExpr And(List<BoolExpr> _elems) => AndExpr.Create(CollectionsMarshal.AsSpan(_elems));

/// <summary>
/// Returns an expression equivalent to a conjunction of the supplied
/// expressions.
Expand All @@ -820,6 +826,15 @@ public void Write(TextWriter _out)
[Pure]
public BoolExpr Or(IEnumerable<BoolExpr> _elems) => OrExpr.Create(_elems.ToArray());

/// <summary>
/// Returns an expression equivalent to a disjunction of the supplied
/// expressions.
/// </summary>
/// <param name="_elems"></param>
/// <returns></returns>
[Pure]
public BoolExpr Or(List<BoolExpr> _elems) => OrExpr.Create(CollectionsMarshal.AsSpan(_elems));

/// <summary>
/// Returns an expression equivalent to a disjunction of the supplied
/// expressions.
Expand Down Expand Up @@ -874,6 +889,11 @@ public BoolExpr Xor(params BoolExpr[] _elems)
/// </summary>
public LinExpr Sum(IEnumerable<BoolExpr> _elems) => Sum(_elems.ToArray());

/// <summary>
/// Returns the sum of the supplied expressions.
/// </summary>
public LinExpr Sum(List<BoolExpr> _elems) => Sum(CollectionsMarshal.AsSpan(_elems));

/// <summary>
/// Returns the sum of the supplied expressions.
/// </summary>
Expand All @@ -890,6 +910,11 @@ public LinExpr Sum(IEnumerable<LinExpr> _elems)
/// </summary>
public UIntVar SumUInt(IEnumerable<BoolExpr> _elems) => SumUInt(_elems.ToArray());

/// <summary>
/// Returns the sum of the supplied expressions as UIntVar.
/// </summary>
public UIntVar SumUInt(List<BoolExpr> _elems) => SumUInt(CollectionsMarshal.AsSpan(_elems));

/// <summary>
/// Returns the sum of the supplied expressions as UIntVar.
/// </summary>
Expand Down Expand Up @@ -1097,9 +1122,9 @@ public int GetHashCode([DisallowNull] (LinExpr, T) _x)
}
}

class SetBoolExprComparer : IEqualityComparer<BoolExpr[]>
class IntArrayComparer : IEqualityComparer<int[]>
{
public bool Equals(BoolExpr[]? _x, BoolExpr[]? _y)
public bool Equals(int[]? _x, int[]? _y)
{
if (_x is null && _y is null)
return true;
Expand All @@ -1108,25 +1133,14 @@ public bool Equals(BoolExpr[]? _x, BoolExpr[]? _y)
if (_y is null)
return false;

if (_x.Length != _y.Length)
return false;

foreach (var x in _x)
if (!_y.Contains(x))
return false;

return true;
return MemoryExtensions.SequenceEqual(_x.AsSpan(), _y.AsSpan());
}

public int GetHashCode([DisallowNull] BoolExpr[] _x)
public int GetHashCode([DisallowNull] int[] _x)
{
var hash = 0;
foreach (var x in _x)
hash ^= x.GetHashCode();

var hc = new HashCode();
hc.Add(_x.Length);
hc.Add(hash);
foreach(var x in _x)
hc.Add(x);
return hc.ToHashCode();
}
}
Expand All @@ -1138,7 +1152,7 @@ public int GetHashCode([DisallowNull] BoolExpr[] _x)
private readonly Dictionary<T, UIntVar> UIntConstCache = new();
internal readonly Dictionary<(LinExpr, T), BoolExpr> LinExprEqCache = new(new IgnoreLinExprOffsetTupleComparer());
internal readonly Dictionary<(LinExpr, T), BoolExpr> LinExprLECache = new(new IgnoreLinExprOffsetTupleComparer());
private readonly Dictionary<BoolExpr[], BoolExpr[]> SortCache = new(new SetBoolExprComparer());
private readonly Dictionary<int[], BoolExpr[]> SortCache = new(new IntArrayComparer());

/// <summary>
/// Returns the count of the supplied expressions.
Expand Down Expand Up @@ -1335,6 +1349,14 @@ public enum KOfMethod
[Pure]
public BoolExpr AtMostOneOf(IEnumerable<BoolExpr> _expr, AtMostOneOfMethod? _method = null) => AtMostOneOf(_expr.ToArray(), _method);

/// <summary>
/// Expression is True iff at most one of the supplied expressions is True.
///
/// Consider using LinExpr-based constraints instead.
/// </summary>
[Pure]
public BoolExpr AtMostOneOf(List<BoolExpr> _expr, AtMostOneOfMethod? _method = null) => AtMostOneOf(CollectionsMarshal.AsSpan(_expr), _method);

/// <summary>
/// Expression is True iff at most one of the supplied expressions is True.
///
Expand Down Expand Up @@ -1472,6 +1494,14 @@ private BoolExpr AtMostOneOfCommander(ReadOnlySpan<BoolExpr> _expr)
[Pure]
public BoolExpr ExactlyOneOf(IEnumerable<BoolExpr> _expr, ExactlyOneOfMethod? _method = null) => ExactlyOneOf(_expr.ToArray().AsSpan(), _method);

/// <summary>
/// Expression is True iff exactly one of the supplied expressions is True.
///
/// Consider using LinExpr-based constraints instead.
/// </summary>
[Pure]
public BoolExpr ExactlyOneOf(List<BoolExpr> _expr, ExactlyOneOfMethod? _method = null) => ExactlyOneOf(CollectionsMarshal.AsSpan(_expr), _method);

/// <summary>
/// Expression is True iff exactly one of the supplied expressions is True.
///
Expand Down Expand Up @@ -1952,12 +1982,17 @@ public BoolExpr[] SortPairwise(ReadOnlySpan<BoolExpr> _elems)
case 2:
return new BoolExpr[] { OrExpr.Create(_elems).Flatten(), AndExpr.Create(_elems).Flatten() };
default:
//adapted from https://en.wikipedia.org/wiki/Pairwise_sorting_network
var cacheKey = _elems.ToArray();
var R = new BoolExpr[_elems.Length];
var cacheKey = new int[_elems.Length];
for (var i = 0; i < _elems.Length; i++)
{
R[i] = _elems[i].Flatten();
cacheKey[i] = ((BoolVar)R[i]).Id;
}
Array.Sort(cacheKey);
if (SortCache.TryGetValue(cacheKey, out var res))
return res;

var R = _elems.ToArray();
void CompSwap(int _i, int _j)
{
var a = R[_i];
Expand All @@ -1967,6 +2002,7 @@ void CompSwap(int _i, int _j)
R[_j] = AndExpr.Create(a, b).Flatten();
}

//adapted from https://en.wikipedia.org/wiki/Pairwise_sorting_network
var a = 1;
for (; a < _elems.Length; a *= 2)
{
Expand Down Expand Up @@ -2026,18 +2062,26 @@ public BoolExpr[] SortTotalizer(ReadOnlySpan<BoolExpr> _elems)
case 2:
return new BoolExpr[] { OrExpr.Create(_elems).Flatten(), AndExpr.Create(_elems).Flatten() };
default:
var cacheKey = _elems.ToArray();
var elems = _elems.ToArray();
var cacheKey = new int[_elems.Length];
for (var i = 0; i < _elems.Length; i++)
{
elems[i] = _elems[i].Flatten();
cacheKey[i] = ((BoolVar)elems[i]).Id;
}
Array.Sort(cacheKey);
if (SortCache.TryGetValue(cacheKey, out var res))
return res;

var R = new BoolExpr[_elems.Length + 2];

var R = new BoolExpr[elems.Length + 2];
R[0] = True;
for (var i = 1; i < R.Length - 1; i++)
R[i] = AddVar();
R[^1] = False;

var A = new BoolExpr[] { True }.Concat(SortTotalizer(_elems[..(_elems.Length / 2)])).Append(False).ToArray();
var B = new BoolExpr[] { True }.Concat(SortTotalizer(_elems[(_elems.Length / 2)..])).Append(False).ToArray();
var A = new BoolExpr[] { True }.Concat(SortTotalizer(elems[..(elems.Length / 2)])).Append(False).ToArray();
var B = new BoolExpr[] { True }.Concat(SortTotalizer(elems[(elems.Length / 2)..])).Append(False).ToArray();
for (var a = 0; a < A.Length - 1; a++)
for (var b = 0; b < B.Length - 1; b++)
{
Expand Down

0 comments on commit 13ccd11

Please sign in to comment.