Skip to content

Commit

Permalink
merge binary optimization into regular optimization, and use variable…
Browse files Browse the repository at this point in the history 
… phases for guidance
  • Loading branch information
Simon Felix committed Sep 8, 2023
1 parent d3ef8ea commit 46ff583
Show file tree
Hide file tree
Showing 2 changed files with 57 additions and 189 deletions.
10 changes: 9 additions & 1 deletion SATInterface/Configuration.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -98,7 +98,7 @@ public class Configuration //<T> where T : struct, IBinaryInteger<T>
public int Verbosity = 2;

/// <summary>
/// Bundled SAT solver to use.
/// SAT solver to use.
///
/// Default: new SATInterface.Solver.CaDiCaL()
/// </summary>
Expand Down Expand Up @@ -186,5 +186,13 @@ internal void Validate()
/// Default: 4
/// </summary>
public int EnumerateLinExprComparisonsLimit = 4;

/// <summary>
/// Set the initial phase of all variables in the objective towards the
/// optimization direction.
///
/// Default: true
/// </summary>
public bool SetVariablePhaseFromObjective = true;
}
}
236 changes: 48 additions & 188 deletions SATInterface/Model.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -434,7 +434,7 @@ public void MultiSolve(Action _solutionCallback)
}
}

private void OptimizeBinary(LinExpr _obj, Action? _solutionCallback, bool _minimization)
private void Optimize(LinExpr _obj, Action? _solutionCallback, bool _minimization)
{
if (State == State.Unsatisfiable && !UnsatWithAssumptions)
return;
Expand Down Expand Up @@ -508,219 +508,72 @@ private void OptimizeBinary(LinExpr _obj, Action? _solutionCallback, bool _minim
break;
}

//start search
//guide search towards better solutions
if (Configuration.SetVariablePhaseFromObjective)
foreach (var t in _obj.Terms)
if (t.Var is BoolVar bv)
bv.SetPhase(t.Weight > 0 ? !_minimization : _minimization);

//if (Configuration.SetVariablePhaseFromObjective)
// foreach (var t in obj.Bits)
// if (t is BoolVar bv)
// bv.SetPhase(!_minimization);

var lb = obj.X;
var ub = T.Min(_obj.UB - objOffset, obj.UB);
var objGELB = T.Zero;
var assumptions = new List<int>();
while (lb != ub && !AbortOptimization)
{
//determine common leading bits of lb and ub
var assumptionBits = new List<int>();
var msb = checked((int)ub.GetBitLength() - 1);
var diffBit = -1;
for (var i = msb; ; i--)
{
Debug.Assert(i >= 0);

if ((ub >> i) != (lb >> i))
{
diffBit = i;

if (ReferenceEquals(obj.Bits[i], Model.True))
{
}
else if (ReferenceEquals(obj.Bits[i], Model.False))
{
assumptionBits.Add(1);
assumptionBits.Add(-1);
}
else if (obj.Bits[i] is BoolVar bv)
assumptionBits.Add(bv.Id);
else
throw new Exception();

break;
}
else if (obj.Bits[i] is BoolVar bv)
assumptionBits.Add((((ub >> i) & T.One) == T.One) ? bv.Id : -bv.Id);
}
Debug.Assert(diffBit != -1);

if (Configuration.Verbosity > 0)
{
if (_minimization)
Console.WriteLine($"Minimizing objective, range {-(ub + objOffset)} - {-(lb + objOffset)}, testing {-(((ub >> diffBit) << diffBit) + objOffset)}");
else
Console.WriteLine($"Maximizing objective, range {(lb + objOffset)} - {(ub + objOffset)}, testing {((ub >> diffBit) << diffBit) + objOffset}");
}

(var subState, var assignment) = State == State.Unsatisfiable ? (State, null) : InvokeSolver(timeout, assumptionBits.ToArray());
if (subState == State.Satisfiable)
{
Debug.Assert(assignment is not null);

State = State.Satisfiable;
for (var i = 0; i < assignment.Length; i++)
varsX[i] = assignment[i];

Debug.Assert(obj.X >= lb);
Debug.Assert(obj.X <= ub);
Debug.Assert(((obj.X >> diffBit) & T.One) == T.One);

//callback might add lazy constraints
var mClauses = ClauseCount;
_solutionCallback?.Invoke();

if (State == State.Satisfiable && ClauseCount == mClauses)
{
//no new lazy constraints
lb = obj.X;
bestAssignment = assignment;
}

if (AbortOptimization)
break;
}
else if (subState == State.Unsatisfiable)
{
ub = ((ub >> diffBit) << diffBit) - T.One;
}
else
{
Debug.Assert(subState == State.Undecided);
break;
}

Debug.Assert(lb <= ub);
}

//restore best known solution
State = State.Satisfiable;
UnsatWithAssumptions = false;
for (var i = 0; i < bestAssignment.Length; i++)
varsX[i] = bestAssignment[i];
}
finally
{
InOptimization = false;
}
}

private void Optimize(LinExpr _obj, Action? _solutionCallback, bool _minimization)
{
if (Configuration.OptimizationFocus == OptimizationFocus.Binary)
{
OptimizeBinary(_obj, _solutionCallback, _minimization);
return;
}

if (State == State.Unsatisfiable && !UnsatWithAssumptions)
return;
var diffBit = checked((int)ub.GetBitLength() - 1);
for (; (ub >> diffBit) == (lb >> diffBit); diffBit--) ;
Debug.Assert(diffBit >= -1);

var timeout = long.MaxValue;
if (Configuration.TimeLimit != TimeSpan.Zero)
timeout = Environment.TickCount64 + (long)Configuration.TimeLimit.TotalMilliseconds;

try
{
InOptimization = true;
AbortOptimization = false;

if (Configuration.Verbosity > 0)
{
if (_minimization)
Console.WriteLine($"Minimizing objective, range {-_obj.UB} - {-_obj.LB}");
else
Console.WriteLine($"Maximizing objective, range {_obj.LB} - {_obj.UB}");
}

bool[]? bestAssignment;
for (; ; )
{
(State, bestAssignment) = InvokeSolver(timeout, null);
if (State != State.Satisfiable)
{
UnsatWithAssumptions = false;
return;
}

Debug.Assert(bestAssignment is not null);

//found initial, potentially feasible solution
for (var i = 0; i < bestAssignment.Length; i++)
varsX[i] = bestAssignment[i];

State = State.Satisfiable;
var mClauses = ClauseCount;

//callback might add lazy constraints or abort
_solutionCallback?.Invoke();

if (State == State.Unsatisfiable)
{
UnsatWithAssumptions = false;
return;
}

if (AbortOptimization)
{
if (State == State.Satisfiable && ClauseCount != mClauses)
{
State = State.Undecided;
UnsatWithAssumptions = false;
}
return;
}

//if it didn't, we have a feasible solution
if (mClauses == ClauseCount)
break;
}

//start search
var lb = _obj.X;
var ub = _obj.UB;
var objGELB = _obj.LB;
var assumptionGE = new List<int>();
while (lb != ub && !AbortOptimization)
{
var cur = Configuration.OptimizationFocus switch
{
OptimizationFocus.Bisection => (lb + T.One + ub) >> 1,
OptimizationFocus.Incumbent => lb + T.One,
OptimizationFocus.Bound => ub,
OptimizationFocus.Binary => (ub >> diffBit) << diffBit,
_ => throw new NotImplementedException()
};

if (Configuration.Verbosity > 0)
//is the current round only a repetition with additional lazy constraints,
//and we already added the GE constraint?
if (assumptions.Count == 0 || objGELB != cur)
{
if (_minimization)
Console.WriteLine($"Minimizing objective, range {-ub} - {-lb}, testing {-cur}");
objGELB = cur;
var ge = (obj >= cur).Flatten();
if (ge is BoolVar v)
{
Debug.Assert(!ReferenceEquals(v, Model.True) && !ReferenceEquals(v, Model.False));
assumptions.Add(v.Id);
}
else
Console.WriteLine($"Maximizing objective, range {lb} - {ub}, testing {cur}");
throw new Exception();
}

//perhaps we already added this GE constraint, and the current
//round is only a repetition with additional lazy constraints?
if (assumptionGE.Count == 0 || objGELB != cur)
if (Configuration.Verbosity > 0)
{
objGELB = cur;
var ge = (_obj >= cur).Flatten();
if (ge is BoolVar v)
assumptionGE.Add(v.Id);
if (_minimization)
Console.WriteLine($"Minimizing objective, range {-(ub + objOffset)} - {-(lb + objOffset)}, testing {-(cur + objOffset)}");
else
throw new Exception();
Console.WriteLine($"Maximizing objective, range {(lb + objOffset)} - {(ub + objOffset)}, testing {(cur + objOffset)}");
}

(var subState, var assignment) = State == State.Unsatisfiable ? (State, null) : InvokeSolver(timeout, assumptionGE.ToArray());
(var subState, var assignment) = State == State.Unsatisfiable ? (State, null) : InvokeSolver(timeout, assumptions.ToArray());

if (subState == State.Satisfiable)
{
Debug.Assert(assignment is not null);

State = State.Satisfiable;
for (var i = 0; i < assignment.Length; i++)
varsX[i] = assignment[i];

Debug.Assert(_obj.X >= cur);
Debug.Assert(obj.X >= lb);
Debug.Assert(obj.X <= ub);
Debug.Assert(obj.X >= cur);

//callback might add lazy constraints
var mClauses = ClauseCount;
Expand All @@ -729,7 +582,7 @@ private void Optimize(LinExpr _obj, Action? _solutionCallback, bool _minimizatio
if (State == State.Satisfiable && ClauseCount == mClauses)
{
//no new lazy constraints
lb = _obj.X;
lb = obj.X;
bestAssignment = assignment;
}

Expand All @@ -739,7 +592,7 @@ private void Optimize(LinExpr _obj, Action? _solutionCallback, bool _minimizatio
else if (subState == State.Unsatisfiable)
{
ub = cur - T.One;
assumptionGE.Clear();
assumptions.Clear();
}
else
{
Expand All @@ -758,6 +611,11 @@ private void Optimize(LinExpr _obj, Action? _solutionCallback, bool _minimizatio
}
finally
{
if (Configuration.SetVariablePhaseFromObjective)
foreach (var t in _obj.Terms)
if (t.Var is BoolVar bv)
bv.SetPhase(null);

InOptimization = false;
}
}
Expand Down Expand Up @@ -1067,7 +925,7 @@ UIntVar SumThree(BoolExpr _a, BoolExpr _b, BoolExpr _c)
if (arr is not null)
ArrayPool<BoolExpr>.Shared.Return(arr);

return res + trueCount;
return res + AddUIntConst(trueCount);
}

private readonly Dictionary<(BoolExpr, BoolExpr), UIntVar> UIntSumTwoCache = new();
Expand Down Expand Up @@ -1325,6 +1183,7 @@ public BoolExpr AtMostOneOf(ReadOnlySpan<BoolExpr> _expr, AtMostOneOfMethod? _me
return !SortTotalizer(expr)[1];
else
return AtMostOneOfPairwiseTree(expr);
//return AtMostOneOfCommander(expr);
case AtMostOneOfMethod.SortTotalizer:
return !SortTotalizer(expr)[1];
case AtMostOneOfMethod.SortPairwise:
Expand Down Expand Up @@ -1455,6 +1314,7 @@ public BoolExpr ExactlyOneOf(ReadOnlySpan<BoolExpr> _expr, ExactlyOneOfMethod? _
return ExactlyKOf(expr.ToArray(), 1, ExactlyKOfMethod.SortTotalizer);
else
return ExactlyOneOfPairwiseTree(expr);
//return ExactlyOneOfCommander(expr);
case ExactlyOneOfMethod.SortTotalizer:
return ExactlyKOf(expr.ToArray(), 1, ExactlyKOfMethod.SortTotalizer);
case ExactlyOneOfMethod.SortPairwise:
Expand Down

0 comments on commit 46ff583

Please sign in to comment.