From 46ff5834a9b24eaa991e75b4da0bd579846046b0 Mon Sep 17 00:00:00 2001 From: Simon Felix Date: Fri, 8 Sep 2023 21:09:58 +0200 Subject: [PATCH] merge binary optimization into regular optimization, and use variable phases for guidance --- SATInterface/Configuration.cs | 10 +- SATInterface/Model.cs | 236 +++++++--------------------------- 2 files changed, 57 insertions(+), 189 deletions(-) diff --git a/SATInterface/Configuration.cs b/SATInterface/Configuration.cs index 31db9d4..0b20021 100644 --- a/SATInterface/Configuration.cs +++ b/SATInterface/Configuration.cs @@ -98,7 +98,7 @@ public class Configuration // where T : struct, IBinaryInteger public int Verbosity = 2; /// - /// Bundled SAT solver to use. + /// SAT solver to use. /// /// Default: new SATInterface.Solver.CaDiCaL() /// @@ -186,5 +186,13 @@ internal void Validate() /// Default: 4 /// public int EnumerateLinExprComparisonsLimit = 4; + + /// + /// Set the initial phase of all variables in the objective towards the + /// optimization direction. + /// + /// Default: true + /// + public bool SetVariablePhaseFromObjective = true; } } diff --git a/SATInterface/Model.cs b/SATInterface/Model.cs index a00cea4..506349c 100644 --- a/SATInterface/Model.cs +++ b/SATInterface/Model.cs @@ -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; @@ -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(); while (lb != ub && !AbortOptimization) { //determine common leading bits of lb and ub - var assumptionBits = new List(); - 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(); - 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; @@ -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; } @@ -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 { @@ -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; } } @@ -1067,7 +925,7 @@ UIntVar SumThree(BoolExpr _a, BoolExpr _b, BoolExpr _c) if (arr is not null) ArrayPool.Shared.Return(arr); - return res + trueCount; + return res + AddUIntConst(trueCount); } private readonly Dictionary<(BoolExpr, BoolExpr), UIntVar> UIntSumTwoCache = new(); @@ -1325,6 +1183,7 @@ public BoolExpr AtMostOneOf(ReadOnlySpan _expr, AtMostOneOfMethod? _me return !SortTotalizer(expr)[1]; else return AtMostOneOfPairwiseTree(expr); + //return AtMostOneOfCommander(expr); case AtMostOneOfMethod.SortTotalizer: return !SortTotalizer(expr)[1]; case AtMostOneOfMethod.SortPairwise: @@ -1455,6 +1314,7 @@ public BoolExpr ExactlyOneOf(ReadOnlySpan _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: