流车间到布尔可满足性[多项式-时间约简]

Question

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

我已经为N*N Sudoku，N皇后和类调度问题做了这样的缩减，但我有一些关于如何将flow shop转换为SAT的问题。

SAT问题如下：

​

​

目标是:用不同的布尔变量，找出每个变量的做作，使“句子”成为真。(如果找到解决方案是可能的)。

我用遗传算法创建了自己的求解器，能够找到一个解决方案，并在没有解的情况下证明。现在，我在不同的NP问题上尝试，比如Flow Shop。

Flow shop调度问题是车间或组车间的一类调度问题，其中流量控制应使每个作业和一组机器上的加工或其他资源( 1,2，.，m)能够按照给定的处理顺序进行适当排序。 特别是需要保持处理任务的连续流，并且需要最小的空闲时间和最小的等待时间。 Flow shop调度是作业车间调度的一种特例，对所有作业都有严格的执行顺序。 流水车间调度也可以适用于生产设施以及计算设计。 (排程)

结果是一系列的工作，他们将经历每一个车间，图形结果将如下所示：

​

​

因此，为了表示flow-shop实例，在输入中我有如下文件：

2 4
4 26 65 62 
63 83 57 9 

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

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

我的Flow-Shop目前确实很简单，但是我不知道如何将它们正式化，以便创建一个CNF文件来执行我的SAT求解程序。

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

这个问题的下一部分：流/作业车间到布尔可满足性[多项式-时间约简]第2部分

Answer 1

我会这样对待它：

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

因此，您可以得到像s_1_2_3这样的变量，从第二个3开始，在机器2上使用第一个资源。

现在，您可以用这些变量来表示各种条件。比如：

• 每个资源一次只能在一台机器上使用。
• 每台机器一次只能处理一个资源。
• 机器步骤必须按顺序执行(机器1需要处理资源x，机器2才能完成它的工作)

警告:即使是一些小问题，这也会造成大量的布尔表达式。

正如@gwilkins所提到的，您需要将优化问题转换为布尔问题。我会遵循他的方法:找出你愿意接受的最大时间，并解决这个时间限制(这实际上限制了变量的数量)。

您还可以从应该有一个解决方案(比如添加所有作业的时间)和一个自然下限(最长作业所需的时间)开始，并通过分割间隔来找到最优解。

再一次:这可能会执行非常糟糕，但它应该提供正确的解决方案。

用此变量表示的约束示例：

机器1必须先处理资源x，才能完成机器2的工作(假设作业长度为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 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);
            }
        }
    }
}

其结果是：

​

Answer 3

第一阅读此页面(作业车间计划)

问题是最短路径。对于最优的合理近似，忘记SAT表达式。试试那些显而易见的。如果您首先在M1上运行最短的作业，那么该作业就可以使用M2，而下一个最短的作业是使用M1。

在这些问题中，每个人都忽略的是，存在“幻影机器”的时间消耗，即等待状态。最大生产率相当于等待状态下的最小时间。因此，每个作业都可以表示为二进制字符串，表示任务中的时间，这是生产性的或非生产性的。每组长度为n的字符串都可以用n表达式表示.该表达式可以简化为k-SAT表达式，其中2

剩下的是一个“编码”问题；比如如何对二进制字符串进行“编码”，以便解决SAT表达式产生您正在寻找的内容。

请参阅这是(3 3SAT的三种完全确定性多项式算法)以解决SAT表达式。