SAT解决人员、技能、景点和日程安排方面的日程安排问题

Question

虽然我对开发并不陌生，但我对SAT求解非常陌生。我有一个解决模式问题的旧代码库(不使用SAT(，我正在尝试使用谷歌OR工具以及"员工调度"one_answers"车间问题"的组合。基本问题：每位员工都有自己的日程安排。每天都有X个必须有人值守的附件要允许员工被分配到某个景点，他/她必须接受适当的培训。现在我有了前两个的代码(使用C#(，但我正在努力思考如何将最后一位添加到pussle中。这是我目前的代码：

现在我需要用另一个维度来扩展它吗？比如：

private CpModel AddExactlyOnePersonToOnePosAndOneTimeslot(int[] personel, int[] timeslots, int[] positions, Dictionary<(int, int), bool> skills, CpModel model, Dictionary<(int, int, int), BoolVar> personelTimePos)
{
List<ILiteral> literals = new List<ILiteral>();
// Add exaktly one employee on each timeslotposition
// Each position is assigned to exactly one personel in the time period.
foreach (var n in personel)
{
foreach (var d in timeslots)
{
foreach (var s in positions)
{
literals.Add(personelTimePos[(n, d, s)]);
}
model.AddExactlyOne(literals);
literals.Clear();
}
}
// One person works at most on one postion during any given timeslot
foreach (var s in positions)
{
foreach (var d in timeslots)
{
foreach (var n in personel)
{
literals.Add(personelTimePos[(n, d, s)]);
}
model.AddAtMostOne(literals);
literals.Clear();
}
}
return model;
}

现在我需要用另一个维度来扩展它吗？比如：

foreach (var s in positions)
{
foreach (var d in timeslots)
{
foreach (var n in personel)
{
foreach(var pp in personSkill)
{

}
}
}
} 

或者我应该使用一个新的变量，比如：

foreach (var s in positions)
{
foreach (var d in timeslots)
{
foreach (var n in personel)
{
var b = model.NewIntVar(0, 1, $"HasSkill_n{n}d{d}s{s}");
}
}
}

正如我所说，我是SAT解决方案的新手，但我觉得这必须是可以实现的。我只是不知道怎么做，我不想拥有它；为我解决"；我正努力在实践中学习。

提前谢谢当做Claes

******下方的完整代码

using Google.OrTools.Sat;

namespace Scheduler1
{
public class SmallTest3
{
public class SolutionPrinter : CpSolverSolutionCallback
{
public SolutionPrinter(int[] allPersonel, int[] allTimeSlots, int[] allPos,
Dictionary<(int, int, int), BoolVar> allPersonelTimePos, int limit)
{
solutionCount_ = 0;
personel = allPersonel;
positions = allPos;
timeslots = allTimeSlots;
personelTimePos = allPersonelTimePos;
solutionLimit_ = limit;
}
public override void OnSolutionCallback()
{
Console.WriteLine($"Solution #{solutionCount_}:");
foreach (var pers in personel)
foreach (var time in timeslots)
foreach (var pos in positions)
{
if (Value(personelTimePos[(pers, time, pos)]) != 0)
Console.WriteLine($"Success personel: {pers}, Time {time}, Pos{pos} filling the position");
}
solutionCount_++;
if (solutionCount_ >= solutionLimit_)
{
Console.WriteLine($"Stop search after {solutionLimit_} solutions");
StopSearch();
}
}
public int SolutionCount()
{
return solutionCount_;
}
private int solutionCount_;

int[] personel;
int[] positions;
int[] timeslots;
Dictionary<(int, int, int), BoolVar> personelTimePos;
private int solutionLimit_;
}
private int[] getPersonel(int noPersonel)
{
int personelId = 1000;
var p = Enumerable.Range(0, noPersonel).ToArray();
for (int i = 0; i < p.Length; i++)
{
p[i] = personelId + i;
}
return p;
}
private int[] getPos(int noPos)
{
var p = Enumerable.Range(0, noPos).ToArray();
for (int i = 0; i < p.Length; i++)
{
p[i] = i;
}
return p;
}
private int[] getTimeSlots(int noTimeSlots)
{
var t = Enumerable.Range(0, noTimeSlots).ToArray();
for (int i = 0; i < t.Length; i++)
{
t[i] = i;
}
return t;
}
private Dictionary<(int, int), bool> getSkillForPos(int[] personel, int[] position)
{
Dictionary<(int, int), bool> skill = new Dictionary<(int, int), bool>();
var pi = 0;
var posi = 0;
foreach (var p in personel)
{
foreach (var pos in position)
{
skill.Add((p, pos), false);
posi++;
}
pi++;
}
return skill;
}
public void run()
{
const int personelCnt = 1;
const int positionsCnt = 1;
const int timeslotsCnt = 1;
int[] personel = getPersonel(personelCnt);
int[] positions = getPos(positionsCnt);
int[] timeslots = getTimeSlots(timeslotsCnt);
Dictionary<(int, int), bool> skills = getSkillForPos(personel, positions);
CpModel model = new CpModel();
model.Model.Variables.Capacity = personelCnt * positionsCnt * timeslotsCnt;
var personelTimePos = populateSchedule(personel, timeslots, positions, skills, model);
model = AddExactlyOnePersonToOnePosAndOneTimeslot(personel, timeslots, positions, skills, model, personelTimePos);
CpSolver solver = new CpSolver();
solver.StringParameters += "linearization_level:0 " + "enumerate_all_solutions:true ";
const int solutionLimit = 5;
SolutionPrinter cb = new SolutionPrinter(personel, timeslots, positions, personelTimePos, solutionLimit);
CpSolverStatus status = solver.Solve(model, cb);
Console.WriteLine($"Solve status: {status}");
Console.WriteLine("Statistics");
Console.WriteLine($"  conflicts: {solver.NumConflicts()}");
Console.WriteLine($"  branches : {solver.NumBranches()}");
Console.WriteLine($"  wall time: {solver.WallTime()}s");

}
private Dictionary<(int, int, int), BoolVar> populateSchedule(int[] personel, int[] timeslots, int[] positions, Dictionary<(int, int), bool> skills, CpModel model)
{ // här skapar vi hela arrayen som ska täcka in alla möjliga kombinationer
//Person    tid     pos
//Janson    12:00   XOP
//Janson    12:15   XOP
//Janson    12:00   FF
//Svenson   12:00   XOP
//
//
Dictionary<(int, int, int), BoolVar> personelTimePos = new Dictionary<(int, int, int), BoolVar>(personel.Count() * positions.Count() * timeslots.Count());
foreach (var n in personel)
foreach (var d in timeslots)
foreach (var s in positions)
{
personelTimePos.Add((n, d, s), model.NewBoolVar($"TimeSlotPositionPersonel_n{n}d{d}s{s}"));

}
return personelTimePos;
}
private CpModel AddExactlyOnePersonToOnePosAndOneTimeslot(int[] personel, int[] timeslots, int[] positions, Dictionary<(int, int), bool> skills, CpModel model, Dictionary<(int, int, int), BoolVar> personelTimePos)
{
List<ILiteral> literals = new List<ILiteral>();
// Add exaktly one employee on each timeslotposition
// Each position is assigned to exactly one personel in the time period.
foreach (var n in personel)
{
foreach (var d in timeslots)
{
foreach (var s in positions)
{
literals.Add(personelTimePos[(n, d, s)]);
}
model.AddExactlyOne(literals);
literals.Clear();
}
}
// One person works at most on one postion during any given timeslot
foreach (var s in positions)
{
foreach (var d in timeslots)
{
foreach (var n in personel)
{
literals.Add(personelTimePos[(n, d, s)]);
}
model.AddAtMostOne(literals);
literals.Clear();
}
}


return model;
}
}
}

Answer 1

您看过复杂的轮班调度示例吗？

它就在这里。它是对位于此处的python中的原始示例的改编。

所有编程语言中的CP-SAT简介都可以在这里找到。