布尔可满足性的流水车间[多项式时间缩减]

Question

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

我已经对一个 N*N 数独、一个 N 皇后和一个 Class 调度问题进行了这样的简化，但是我对如何将流水车间转换为 SAT 有一些问题。

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

目标是：使用不同的布尔变量，找到每个变量的影响以使“句子”为真。（如果找到解决方案是可能的）。

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

Flow shop scheduling problems are a class of scheduling problems with a workshop or group shop in which the flow control shall enable an appropriate sequencing for each job and for processing on a set of machines or with other resources 1,2,...,m in compliance with given processing orders.

Especially the maintaining of a continuous flow of processing tasks is desired with a minimum of idle time and a minimum of waiting time.

Flow shop scheduling is a special case of job shop scheduling where there is strict order of all operations to be performed on all jobs.

Flow shop scheduling may apply as well to production facilities as to computing designs.

(http://en.wikipedia.org/wiki/Flow_shop_scheduling)

结果是一系列工作，这些工作将经过每个车间，图形结果将如下所示：

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

2 4
4 26 65 62 
63 83 57 9

这个文件意味着我有 2 个商店和 4 个作业，每个作业在每台机器上的所有持续时间。

目标：找到最小化 C_max 的序列，如果您愿意，最后一台机器上最后一个作业的结束日期。

我的 Flow-Shop 现在真的很简单，但我不知道如何将它们形式化以便创建一个 CNF 文件来执行我的 SAT 求解器。

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

这个问题的下一部分：

Answer 1

我正在使用 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);
            }
        }
    }
}

结果是：

Answer 2

我会这样处理：

对于在每台机器上的每个可能时间开始的每个资源使用情况，您都有一个布尔变量（当然，这要求时间是有限且离散的，所以我假设是整数）。

所以你得到像 s_1_2_3 这样的变量，这意味着资源一从第二个 3 开始在机器 2 上使用。

现在您可以根据这些变量制定各种条件。喜欢：

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

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

正如@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 ...

Answer 3

第一个read this page (Job Shop Scheduling)

问题是最短路径。为了合理地近似最优，忘记 SAT 表达式。尝试什么是显而易见的。如果您先运行 M1 上的最短作业，那么该作业已准备好使用 M2，而下一个最短作业正在使用 M1。
在这些问题中每个人都忽略的是 'phantom machines'消耗时间即等待状态。最大生产率相当于等待状态的最短时间。因此，每个工作都可以表示为一个二进制字符串，表示任务中的时间是生产性的还是非生产性的。每组长度为 n 的字符串都可以用 n-SAT 表达式表示。该表达式可以在多项式时间内简化为 k-SAT 表达式，其中 2 < k < n。
其余的是 'coding' 问题；就像如何 'code' 二进制字符串，以便解决 SAT 表达式产生你正在寻找的东西。

参见this (Three complete deterministic polynomial algorithms for 3SAT)解决SAT表达式。

布尔可满足性的流水车间[多项式时间缩减]

Flow Shop to Boolean satisfiability [Polynomial-time reduction]

algorithm

optimization

reduction

sat