流水车间调度问题到布尔可满足性问题的多项式时间归约

Question

我联系你是为了了解如何将“流水车间调度问题”转化为布尔可满足性问题。

我已经对N * N数独、N皇后和班级排课问题进行了这样的简化，但我在如何将流水车间转化为SAT方面遇到了一些问题。

一个SAT问题看起来像这样：

目标是：通过不同的布尔变量，找到每个变量的赋值以使“语句”为真（如果有解的话）。

我创建了自己的遗传算法求解器，能够找到解决方案并证明无解时。现在，我将它尝试用于不同的NP问题，例如Flow Shop。

流水车间调度问题是一类调度问题，具有车间或群组车间，在其中流量控制应使每个作业的适当排序，并在1、2、…、m台机器或其他资源上进行处理，以符合给定的处理顺序。

特别需要维护连续的处理任务流，并在最少的空闲时间和等待时间下完成。

流水车间调度是作业车间调度的特例，其中所有作业的所有操作都有严格的顺序。

流水车间调度可以适用于生产设施和计算设计。

结果是一系列经过每个车间的工作，图形结果如下所示:

所以为了表示流水车间实例，我有这样的输入文件：

2 4
4 26 65 62 
63 83 57 9 

这个文件表示我有2家商店和4个工作，每个工作在各自的机器上的持续时间都记录在内。

目标：找到最小化C_max的序列，即最后一个工作在最后一台机器上的结束日期。

我的Flow-Shop现在非常简单，但我不知道如何规范化它们，以便创建CNF文件并在之后执行我的SAT求解器。

如果你们中的任何人有想法：文章？开始的想法？

这个问题的下一部分： Flow/Job Shop to Boolean satisfiability [Polynomial-time reduction] part 2

- Valentin Montmirail

---

c 和这个问题有什么关系呢？ - Pham Trung

如果您想用SAT的术语来表达您的问题，那么我认为您首先需要将其从优化问题转换为决策问题。具体而言，不要问：“什么是最佳解决方案？”而是问：“是否有一个在N时间内结束的解决方案？”这样，您可以验证所提出的解决方案是否满足流水车间约束，并轻松检查它是否在N时间内完成。我假设您在尝试用SAT的术语来表达优化条件时遇到了困难。这正确吗？ - gwilkins

我不确定我完全理解了，但最终，你对这个过程的控制是生成机器的排列，然后在给定的排列上尽可能快地处理下一个任务，或者我误解了这个问题？（与SAT约简无关，只是理解问题本身） - amit

请原谅，但至少为了开始我的理解，我添加了一个Code，用于获取您拥有的结果。在处理开始时间的最简条件下 ;)。 - shA.t

我提了一个新问题（有更多的细节，因为我在实现我认为的解决方案时出现了问题...: http://stackoverflow.com/questions/29651856/flow-job-shop-to-boolean-satisfiability-polynomial-time-reduction-part-2） - Valentin Montmirail

Answer 1

我会这样处理：

对于每个可能的时间和机器，您都有一个布尔变量来表示每个资源使用的开始时间（当然需要时间是有限且离散的，所以我假设是整数）。

因此，您可以得到像 s_1_2_3 这样的变量，它的意思是资源 1 从第 2 台机器的第 3 秒开始使用。

现在，您可以根据这些变量来表述各种条件。例如：

• 每个资源一次只能在一台机器上使用
• 每台机器一次只能处理一个资源
• 必须按顺序进行机器步骤（机器 1 需要处理资源 x，然后机器 2 才能完成其工作）

警告：即使是小问题，这也会产生大量的布尔表达式。

如 @gwilkins 所提到的，您需要将优化问题转换为布尔问题。我会遵循他的方法：找到您愿意接受的最长时间，并解决该时间限制（这实际上限制了变量的数量）。

您还可以从某些应该有解决方案的内容开始（例如所有工作的时间之和），并从自然下限（最长工作所需的时间）开始，通过分割区间找到最佳解决方案。

再次强调：这可能会表现得非常糟糕，但它应该提供正确的解决方案。

以下是使用这些变量表述约束条件的示例：

机器 1 必须在机器 2 开始工作之前处理资源 x（假设作业长度为 1）：

(S_x_1_1 and ! S_x_2_1) 
or (S_x_1_2 and ! S_x_2_1 and ! S_x_2_2) 
or (S_x_1_3 and ! S_x_2_1 and ! S_x_2_2 and ! S_x_2_3)
or ...

- Jens Schauder

---

确实，你的布尔变量看起来可以工作，但我不确定你如何使用这些变量编写约束条件？:/ 你能给我一个小例子吗？:/ - Valentin Montmirail

例如，如果要表达一个资源一次只能在一台机器上使用，可以说我将有N个约束（其中N是机器的数量），可以这样说：“对于每个l:AND ( ¬S_i_j_k OR ¬S_i_l_k )”。就像这样，如果S_i_j_k为真，则S_i_l_k应该为假。这样正确吗？ :) - Valentin Montmirail

我认为我可以将此视为解决方案，这确实是将Flow Shop转换为SAT的一种方式。不幸的是，它是伪多项式时间，而不仅仅是多项式时间...但至少它会给出一个解决方案。 - Valentin Montmirail

对于其他的限制条件，都没问题，但我有一个问题：如何使用这样的变量来编写“机器步骤必须按顺序进行（机器1需要处理资源x，然后机器2才能开始工作）”这个约束条件？:/ - Valentin Montmirail

我想提一个新问题（更详细，因为我在解决方案的实现中遇到了问题...：http://stackoverflow.com/questions/29651856/flow-job-shop-to-boolean-satisfiability-polynomial-time-reduction-part-2） - Valentin Montmirail

Answer 2

我使用的是C#语言；我通过以下这些if语句处理结果：
（EndTime = StartTime + Duration）

// This is for handling start of M1J4 that starts after end of M2J2
// Bt I think this is out of 'Flow Shop Working'
if (i > 1)
    if (M[m].jobs[i].StartTime < M[m + 1].jobs[i - 2].EndTime)
        M[m].jobs[i].StartTime = M[m + 1].jobs[i - 2].EndTime;

if (i > 0)
    if (M[m].jobs[i].StartTime < M[m + 1].jobs[i - 1].StartTime)
        M[m].jobs[i].StartTime = M[m + 1].jobs[i - 1].StartTime;
if (M[m + 1].jobs[i].StartTime < M[m].jobs[i].EndTime)
    M[m + 1].jobs[i].StartTime = M[m].jobs[i].EndTime;

---

我的控制台应用程序代码是：

class job
{
    public int Id { get; set; }
    public int Duration { get; set; }
    public int StartTime { get; set; }
    public int EndTime { get { return this.StartTime + this.Duration; } } 

    public job(int _Id) { this.Id = _Id; }

    public override string ToString()
    {
        if (this.Duration == 1)
            return "|";
        string result = "[";
        for (int i = 0; i < this.Duration - 2; i++)
            result += "#";
        return result + "]";
    } 
}

class machine
{
    public int Id { get; set; }
    public List<job> jobs = new List<job>();
    public int C_Max { get { return this.jobs[jobs.Count - 1].EndTime; } }

    public machine(int _Id) { this.Id = _Id; }

    public job AddJob(int _Duration)
    {
        int newId = 1;
        if (newId < jobs.Count + 1)
            newId = jobs.Count + 1;
        jobs.Add(new job(newId));
        jobs[newId - 1].Duration = _Duration;
        if (newId == 1)
            jobs[newId - 1].StartTime = 0;
        else
            jobs[newId - 1].StartTime = jobs[newId - 2].EndTime;
        return jobs[newId - 1];
    }

    public void LagJobs(job fromJob, int lagDuration)
    {
        for (int i = fromJob.Id; i <= jobs.Count; i++)
            jobs[i].StartTime += lagDuration;
    }

    public void AddJobs(int[] _Durations)
    {
        for (int i = 0; i < _Durations.Length; i++)
            this.AddJob(_Durations[i]);
    }

    public override string ToString()
    {
        return this.ToString(false);
    }

    public string ToString(bool withMax)
    {
        string result = string.Empty;
        for (int i = 0; i < jobs.Count; i++)
        {
            while (jobs[i].StartTime > result.Length)
                result += " ";
            result += jobs[i].ToString();
        }
        result = this.Id.ToString() + ". " + result;
        if (withMax) 
            result += " : " + this.C_Max;
        return result;
    }
}

class Program
{
    static void Main(string[] args)
    {
        int machinesCount = 4;
        List<machine> machines = new List<machine>();
        for (int i = 0; i < machinesCount; i++)
        {
            machines.Add(new machine(i + 1));
        }
        machines[0].AddJobs(new int[] { 5, 5, 3, 6, 3 });
        machines[1].AddJobs(new int[] { 4, 4, 2, 4, 4 });
        machines[2].AddJobs(new int[] { 4, 4, 3, 4, 1 });
        machines[3].AddJobs(new int[] { 3, 6, 3, 2, 6 });
        handelMachines(machines);
        for (int i = 0; i < machinesCount; i++)
            Console.WriteLine(machines[i].ToString(true));
        Console.ReadKey();
    }

    static void handelMachines(List<machine> M)
    {
        if (M.Count == 2)
        {
            for (int i = 0; i < M[0].jobs.Count; i++)
            {
                if (i > 1)
                    if (M[0].jobs[i].StartTime < M[1].jobs[i - 2].EndTime)
                        M[0].jobs[i].StartTime = M[1].jobs[i - 2].EndTime;
                if (i > 0)
                    if (M[0].jobs[i].StartTime < M[1].jobs[i - 1].StartTime)
                        M[0].jobs[i].StartTime = M[1].jobs[i - 1].StartTime;
                if (M[1].jobs[i].StartTime < M[0].jobs[i].EndTime)
                    M[1].jobs[i].StartTime = M[0].jobs[i].EndTime;
            }
        }
        else
        {
            for (int i = 0; i < M.Count - 1; i++)
            {
                List<machine> N = new List<machine>();
                N.Add(M[i]);
                N.Add(M[i + 1]);
                handelMachines(N);
            }
        }
    }
}

结果如下：

- shA.t

---

这确实是解决Flow Shop问题的方法，但我的问题不在于此，而更多地在于我需要将其转化为SAT问题，解决SAT问题，然后像您一样显示甘特图解决方案 :) - Valentin Montmirail

我有一个新的问题（更多细节，因为我在解决方案的实现中遇到了问题...：http://stackoverflow.com/questions/29651856/flow-job-shop-to-boolean-satisfiability-polynomial-time-reduction-part-2） - Valentin Montmirail

Answer 3

首先阅读此页面（Job Shop Scheduling）

问题是最短路径。为了合理地逼近最优解，忘记SAT表达式。试试显而易见的方法。如果你先在M1上运行最短的作业，那么当下一个最短的作业正在使用M1时，该作业已经准备好使用M2。
在这些问题中，每个人都忽略了消耗时间的“幻影机器”，即等待状态。最大生产力相当于最小的等待时间。因此，每个作业都可以表示为二进制字符串，表示在生产性或非生产性任务中的时间。每组长度为n的字符串可以用n-SAT表达式表示。该表达式可以在多项式时间内简化为k-SAT表达式，其中2 < k < n。
其余部分是一个“编码”问题；就像如何“编码”二进制字符串一样，以便解决SAT表达式产生您所寻求的结果。

请参见此处（三种完整的确定性多项式算法用于3SAT）以解决SAT表达式。

- george