Flow Shop to Boolean satisfiability [Polynomial-time reduction]

Question

I contact you in order to get an idea on "how to transform a flow shop scheduling problem" into a boolean satisfiability.

I already done such reduction for a N*N Sudoku, a N-queens and a Class scheduling problem, but I have some issue on how to transform the flow shop into SAT.

a SAT problem looks like this :

The goal is : with different boolean variables, to find an affectation of every variable in order to make the "sentence" true. (If finding a solution is possible).

I create my own solver with genetic algorithm able to find a solution and to prove when there is none. And now, I try it on different NP-problems, like 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)

and the result is a sequence of jobs who will go through every workshop and the graphical result will look like this :

So to represent flow-shop instances, in input I have files like this :

2 4
4 26 65 62 
63 83 57 9 

This file means that I have 2 shops and 4 jobs, with all the duration time of each jobs on each machines.

The goal : to find the sequence who minimize the C_max, the end-date of the last job on the last machine if you prefer.

My Flow-Shop are really simple for now, but I have no idea how to formalize them in order to create a CNF file to execute my SAT solver after.

If one of you has some idea : article ? beginning of an idea ?

Next part of this question : Flow/Job Shop to Boolean satisfiability [Polynomial-time reduction] part 2

Answer 1

First read this page (Job Shop Scheduling)

The problem is shortest path. For a reasonable approximation of optimal, forget SAT expressions. Try what is obvious. If you run the shortest job on M1 first then that job is ready to use M2 while the next shortest job is using M1.
What everyone ignores in these problems is that there are 'phantom machines' consuming time that are the wait states. Maximum productivity is the equivalent of minimum time in wait states. So every job can be represented as a binary string representing time in a task that is productive or non-productive. Every set of strings of length n can be represented by a n-SAT expression. That expression can be reduced to a k-SAT expression where 2 < k < n, in polynomial time.
The rest is a 'coding' problem; as in how to 'code' the binary strings so that solving the SAT expression produces what you are seeking.

See this (Three complete deterministic polynomial algorithms for 3SAT) to solve the SAT expression.

Answer 2

I'd approach it like this:

You have a boolean variable for each resource usage start at each possible time at each machine (of course that requires that the time is limited and discrete, so I'd assume integers).

So you get variables like s_1_2_3 with the meaning resource one gets used at machine 2 starting from second 3.

Now you can formulate you various conditions in terms of these variables. Like:

• each resource can be used only at one machine at a time
• each machine can process only one resource at a time
• machine steps have to happen in order (machine 1 needs to process resource x, before machine 2 can do it's job)

Warning: Even for small problems this will create a HUGE amount of boolean expressions.

As @gwilkins mentioned you need to transform the optimization problem into a boolean Problem. And I'd follow his approach: find a maximum time you are willing to accept and solve for that time limit (which actually limits the number of variables).

You can also start with something that should have a solution (like the time of all jobs added) and something that is a natural lower limit (the time needed for the longest job) and by splitting the interval find the optimal solution.

Once again: this will probably perform really awful, but it should provide the correct solution.

Example for a constraint formulated with this variables:

Machine 1 has to process resource x before Machine 2 can do its job (assuming the job has length 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

I'm using c#; I handle that result by these if statements:
( 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;

---

Code of my Console Application is :

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);
            }
        }
    }
}

And result is: