port csharp sat examples

This commit is contained in:
Laurent Perron
2022-01-10 21:24:54 +01:00
parent 4d1eee929b
commit 2aba48589e
6 changed files with 62 additions and 73 deletions

View File

@@ -59,7 +59,7 @@ public class BalanceGroupSat
var model = new CpModel();
var itemInGroup = new IntVar[numberItems, numberGroups];
var itemInGroup = new BoolVar[numberItems, numberGroups];
foreach (var item in allItems)
{
foreach (var @group in allGroups)
@@ -97,7 +97,7 @@ public class BalanceGroupSat
}
// colorInGroup variables.
var colorInGroup = new IntVar[numberColors, numberGroups];
var colorInGroup = new BoolVar[numberColors, numberGroups];
foreach (var @group in allGroups)
{
foreach (var color in allColors)
@@ -156,11 +156,11 @@ public class BalanceGroupSat
private int[] _colors;
private int[] _allGroups;
private int[] _allItems;
private IntVar[,] _itemInGroup;
private BoolVar[,] _itemInGroup;
private int _solutionCount;
public SolutionPrinter(int[] values, int[] colors, int[] allGroups, int[] allItems, IntVar[,] itemInGroup)
public SolutionPrinter(int[] values, int[] colors, int[] allGroups, int[] allItems, BoolVar[,] itemInGroup)
{
this._values = values;
this._colors = colors;

View File

@@ -48,7 +48,7 @@ public class GateSchedulingSat
List<IntervalVar> intervals = new List<IntervalVar>();
List<IntervalVar> intervals0 = new List<IntervalVar>();
List<IntervalVar> intervals1 = new List<IntervalVar>();
List<IntVar> performed = new List<IntVar>();
List<BoolVar> performed = new List<BoolVar>();
List<IntVar> starts = new List<IntVar>();
List<IntVar> ends = new List<IntVar>();
List<int> demands = new List<int>();
@@ -65,7 +65,7 @@ public class GateSchedulingSat
ends.Add(end);
demands.Add(jobs[i, 1]);
IntVar performed_on_m0 = model.NewBoolVar(String.Format("perform_{0}_on_m0", i));
BoolVar performed_on_m0 = model.NewBoolVar(String.Format("perform_{0}_on_m0", i));
performed.Add(performed_on_m0);
// Create an optional copy of interval to be executed on machine 0.

View File

@@ -18,7 +18,7 @@ using Google.OrTools.Sat;
public class NurseSolutionObserver : CpSolverSolutionCallback
{
public NurseSolutionObserver(IntVar[,,] shifts, int num_nurses, int num_days, int num_shifts, HashSet<int> to_print,
public NurseSolutionObserver(BoolVar[,,] shifts, int num_nurses, int num_days, int num_shifts, HashSet<int> to_print,
int last_solution_explored)
{
shifts_ = shifts;
@@ -90,7 +90,7 @@ public class NursesSat
// Creates shift variables.
// shift[n, d, s]: nurse "n" works shift "s" on day "d".
IntVar[,,] shift = new IntVar[num_nurses, num_days, num_shifts];
BoolVar[,,] shift = new BoolVar[num_nurses, num_days, num_shifts];
foreach (int n in all_nurses)
{
foreach (int d in all_days)

View File

@@ -102,7 +102,7 @@ public class ShiftSchedulingSat
var model = new CpModel();
IntVar[,,] work = new IntVar[numEmployees, numShifts, numDays];
BoolVar[,,] work = new BoolVar[numEmployees, numShifts, numDays];
foreach (int e in Range(numEmployees))
{
@@ -116,17 +116,14 @@ public class ShiftSchedulingSat
}
// Linear terms of the objective in a minimization context.
var objIntVars = new List<IntVar>();
var objIntCoeffs = new List<int>();
var objBoolVars = new List<IntVar>();
var objBoolCoeffs = new List<int>();
LinearExprBuilder obj = LinearExpr.NewBuilder();
// Exactly one shift per day.
foreach (int e in Range(numEmployees))
{
foreach (int d in Range(numDays))
{
var temp = new IntVar[numShifts];
var temp = new BoolVar[numShifts];
foreach (int s in Range(numShifts))
{
temp[s] = work[e, s, d];
@@ -145,8 +142,7 @@ public class ShiftSchedulingSat
// Employee requests
foreach (var (e, s, d, w) in requests)
{
objBoolVars.Add(work[e, s, d]);
objBoolCoeffs.Add(w);
obj.AddTerm(work[e, s, d], w);
}
// Shift constraints
@@ -154,7 +150,7 @@ public class ShiftSchedulingSat
{
foreach (int e in Range(numEmployees))
{
var works = new IntVar[numDays];
var works = new BoolVar[numDays];
foreach (int d in Range(numDays))
{
works[d] = work[e, constraint.Shift, d];
@@ -165,8 +161,7 @@ public class ShiftSchedulingSat
constraint.HardMax, constraint.MaxPenalty,
$"shift_constraint(employee {e}, shift {constraint.Shift}");
objBoolVars.AddRange(variables);
objBoolCoeffs.AddRange(coeffs);
obj.AddWeightedSum(variables, coeffs);
}
}
@@ -177,7 +172,7 @@ public class ShiftSchedulingSat
{
foreach (int w in Range(numWeeks))
{
var works = new IntVar[7];
var works = new BoolVar[7];
foreach (int d in Range(7))
{
@@ -189,8 +184,7 @@ public class ShiftSchedulingSat
constraint.HardMax, constraint.MaxPenalty,
$"weekly_sum_constraint(employee {e}, shift {constraint.Shift}, week {w}");
objBoolVars.AddRange(variables);
objBoolCoeffs.AddRange(coeffs);
obj.AddWeightedSum(variables, coeffs);
}
}
}
@@ -214,8 +208,7 @@ public class ShiftSchedulingSat
var transVar = model.NewBoolVar($"transition (employee {e}, day={d}");
transition.Add(transVar);
model.AddBoolOr(transition);
objBoolVars.Add(transVar);
objBoolCoeffs.Add(penalizedTransition.Penalty);
obj.AddTerm(transVar, penalizedTransition.Penalty);
}
}
}
@@ -228,7 +221,7 @@ public class ShiftSchedulingSat
{
foreach (int d in Range(7))
{
var works = new IntVar[numEmployees];
var works = new BoolVar[numEmployees];
foreach (int e in Range(numEmployees))
{
works[e] = work[e, s, w * 7 + d];
@@ -245,18 +238,14 @@ public class ShiftSchedulingSat
var name = $"excess_demand(shift={s}, week={w}, day={d}";
var excess = model.NewIntVar(0, numEmployees - minDemand, name);
model.Add(excess == worked - minDemand);
objIntVars.Add(excess);
objIntCoeffs.Add(overPenalty);
obj.AddTerm(excess, overPenalty);
}
}
}
}
// Objective
var objBoolSum = LinearExpr.WeightedSum(objBoolVars, objBoolCoeffs);
var objIntSum = LinearExpr.WeightedSum(objIntVars, objIntCoeffs);
model.Minimize(objBoolSum + objIntSum);
model.Minimize(obj);
// Solve model
var solver = new CpSolver();
@@ -296,30 +285,30 @@ public class ShiftSchedulingSat
Console.WriteLine();
Console.WriteLine("Penalties:");
foreach (var (i, var) in objBoolVars.Select((x, i) => (i, x)))
{
if (solver.BooleanValue(var))
{
var penalty = objBoolCoeffs[i];
if (penalty > 0)
{
Console.WriteLine($" {var.Name()} violated, penalty={penalty}");
}
else
{
Console.WriteLine($" {var.Name()} fulfilled, gain={-penalty}");
}
}
}
// foreach (var (i, var) in objBoolVars.Select((x, i) => (i, x)))
// {
// if (solver.BooleanValue(var))
// {
// var penalty = objBoolCoeffs[i];
// if (penalty > 0)
// {
// Console.WriteLine($" {var.Name()} violated, penalty={penalty}");
// }
// else
// {
// Console.WriteLine($" {var.Name()} fulfilled, gain={-penalty}");
// }
// }
// }
foreach (var (i, var) in objIntVars.Select((x, i) => (i, x)))
{
if (solver.Value(var) > 0)
{
Console.WriteLine(
$" {var.Name()} violated by {solver.Value(var)}, linear penalty={objIntCoeffs[i]}");
}
}
// foreach (var (i, var) in objIntVars.Select((x, i) => (i, x)))
// {
// if (solver.Value(var) > 0)
// {
// Console.WriteLine(
// $" {var.Name()} violated by {solver.Value(var)}, linear penalty={objIntCoeffs[i]}");
// }
// }
Console.WriteLine();
Console.WriteLine("Statistics");
@@ -342,7 +331,7 @@ public class ShiftSchedulingSat
/// <returns>An array of variables which conjunction will be false if the
/// sub-list is assigned to True, and correctly bounded by variables assigned
/// to False, or by the start or end of works.</returns>
static ILiteral[] NegatedBoundedSpan(IntVar[] works, int start, int length)
static ILiteral[] NegatedBoundedSpan(BoolVar[] works, int start, int length)
{
var sequence = new List<ILiteral>();
@@ -380,11 +369,11 @@ public class ShiftSchedulingSat
/// base name for penalty literals.</param> <returns>A tuple (costLiterals,
/// costCoefficients) containing the different penalties created by the
/// sequence constraint.</returns>
static (IntVar[] costLiterals, int[] costCoefficients)
AddSoftSequenceConstraint(CpModel model, IntVar[] works, int hardMin, int softMin, int minCost, int softMax,
static (IEnumerable<BoolVar> costLiterals, IEnumerable<int> costCoefficients)
AddSoftSequenceConstraint(CpModel model, BoolVar[] works, int hardMin, int softMin, int minCost, int softMax,
int hardMax, int maxCost, string prefix)
{
var costLiterals = new List<IntVar>();
var costLiterals = new List<BoolVar>();
var costCoefficients = new List<int>();
// Forbid sequences that are too short.
@@ -449,7 +438,7 @@ public class ShiftSchedulingSat
model.AddBoolOr(temp);
}
return (costLiterals.ToArray(), costCoefficients.ToArray());
return (costLiterals, costCoefficients);
}
/// <summary>
@@ -473,8 +462,8 @@ public class ShiftSchedulingSat
/// base name for penalty literals.</param> <returns>A tuple (costVariables,
/// costCoefficients) containing the different penalties created by the
/// sequence constraint.</returns>
static (IntVar[] costVariables, int[] costCoefficients)
AddSoftSumConstraint(CpModel model, IntVar[] works, int hardMin, int softMin, int minCost, int softMax,
static (IEnumerable<IntVar> costVariables, IEnumerable<int> costCoefficients)
AddSoftSumConstraint(CpModel model, BoolVar[] works, int hardMin, int softMin, int minCost, int softMax,
int hardMax, int maxCost, string prefix)
{
var costVariables = new List<IntVar>();
@@ -508,7 +497,7 @@ public class ShiftSchedulingSat
costCoefficients.Add(maxCost);
}
return (costVariables.ToArray(), costCoefficients.ToArray());
return (costVariables, costCoefficients);
}
/// <summary>

View File

@@ -21,10 +21,10 @@ class SpeakerScheduling
{
struct Entry
{
public IntVar var;
public BoolVar var;
public int start;
public Entry(IntVar v, int s)
public Entry(BoolVar v, int s)
{
var = v;
start = s;
@@ -93,15 +93,15 @@ class SpeakerScheduling
entries[speaker] = new List<Entry>();
}
List<IntVar>[] contributions_per_slot = new List<IntVar>[last_slot + 1];
List<BoolVar>[] contributions_per_slot = new List<BoolVar>[last_slot + 1];
for (int slot = 1; slot <= last_slot; ++slot)
{
contributions_per_slot[slot] = new List<IntVar>();
contributions_per_slot[slot] = new List<BoolVar>();
}
for (int speaker = 0; speaker < number_of_speakers; ++speaker)
{
List<IntVar> all_vars = new List<IntVar>();
List<BoolVar> all_vars = new List<BoolVar>();
int duration = durations[speaker];
// Let's filter the possible starts.
int availability = speaker_availability[speaker].Length;
@@ -125,7 +125,7 @@ class SpeakerScheduling
}
if (ok)
{
IntVar var = model.NewBoolVar("speaker " + (speaker + 1) + " starts at " + slot);
BoolVar var = model.NewBoolVar("speaker " + (speaker + 1) + " starts at " + slot);
entries[speaker].Add(new Entry(var, slot));
all_vars.Add(var);
for (int offset = 0; offset < duration; ++offset)
@@ -134,12 +134,12 @@ class SpeakerScheduling
}
}
}
model.Add(LinearExpr.Sum(all_vars) == 1);
model.AddExactlyOne(all_vars);
}
// Force the schedule to be consistent.
for (int slot = first_slot; slot <= last_slot; ++slot)
{
model.Add(LinearExpr.Sum(contributions_per_slot[slot]) <= 1);
model.AddAtMostOne(contributions_per_slot[slot]);
}
// Creates last_slot.

View File

@@ -156,13 +156,13 @@ class TaskSchedulingSat
CpModel model = new CpModel();
IntervalVar[] tasks = new IntervalVar[taskCount];
IntVar[] taskChoosed = new IntVar[taskCount];
BoolVar[] taskChoosed = new BoolVar[taskCount];
IntVar[] allEnds = new IntVar[GetEndTaskCount()];
int endJobCounter = 0;
foreach (Job j in myJobList)
{
IntVar[] tmp = new IntVar[j.AlternativeTasks.Count];
BoolVar[] tmp = new BoolVar[j.AlternativeTasks.Count];
int i = 0;
foreach (Task t in j.AlternativeTasks)
{
@@ -178,7 +178,7 @@ class TaskSchedulingSat
tasksToEquipment[t.Equipment] = new List<IntervalVar>();
tasksToEquipment[t.Equipment].Add(tasks[ti]);
}
model.Add(LinearExpr.Sum(tmp) == 1);
model.AddExactlyOne(tmp);
}
foreach (KeyValuePair<long, List<IntervalVar>> pair in tasksToEquipment)