<p>First <a href="https://en.wikipedia.org/wiki/Job_shop_scheduling" rel="nofollow noreferrer">read this page (Job Shop Scheduling)</a></p>

<p>The problem is <strong>shortest path</strong>. 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.<br>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 &lt; k &lt; n, in polynomial time.<br>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.</p>

<p>See <a href="https://arxiv.org/abs/cs/0205064" rel="nofollow noreferrer">this (Three complete deterministic polynomial algorithms for 3SAT)</a> to solve the SAT expression.</p>
Flow Shop to Boolean satisfiability [Polynomial-time reduction]
<p>I contact you in order to get an idea on &quot;how to transform a flow shop scheduling problem&quot; into a boolean satisfiability.</p>
<p>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.</p>
<p>a SAT problem looks like this :</p>
<p><img src="https://i.stack.imgur.com/SzHSS.png" alt="Illustration of a SAT problem" /></p>
<p>The goal is : with different boolean variables, to find an affectation of every variable in order to make the &quot;sentence&quot; true. (If finding a solution is possible).</p>
<p>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.</p>
<blockquote>
<p>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.</p>
<p>Especially the maintaining of a continuous flow of processing tasks is desired with a minimum of idle time and a minimum of waiting time.</p>
<p>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.</p>
<p>Flow shop scheduling may apply as well to production facilities as to computing designs.</p>
<p>(<a href="http://en.wikipedia.org/wiki/Flow_shop_scheduling" rel="nofollow noreferrer">http://en.wikipedia.org/wiki/Flow_shop_scheduling</a>)</p>
</blockquote>
<p>and the result is a sequence of jobs who will go through every  workshop and the graphical result will look like this :</p>
<p><img src="https://i.stack.imgur.com/lQs2v.gif" alt="Graphical result of a Flow Shop" /></p>
<p>So to represent flow-shop instances, in input I have files like this :</p>
<pre><code>2 4
4 26 65 62 
63 83 57 9 
</code></pre>
<p>This file means that I have 2 shops and 4 jobs, with all the duration time of each jobs on each machines.</p>
<p>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.</p>
<p>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.</p>
<p>If one of you has some idea : article ? beginning of an idea ?</p>
<p>Next part of this question : <a href="https://stackoverflow.com/questions/29651856/flow-job-shop-to-boolean-satisfiability-polynomial-time-reduction-part-2">Flow/Job Shop to Boolean satisfiability [Polynomial-time reduction] part 2</a></p>