Flow / Job Shop for logical feasibility [Part 2]

Question

here is the continuity of my first question ( Flow Shop to Boolean feasibility [Polynomial time reduction] ).

Because something is wrong, and I did not have time to find out exactly where. I will once again ask for the help of the StackOverFlow masters :)

To summarize what I have now:

• I have an input file that looks like this:

3 2 1 1 1 1 1 1 

Who presents: 3 tasks, 2 stores (cars) and the duration of each work in each store (car). And I want for abstract problems to find the optimal C_max value.

So, for example, it should output this result (sorry for paint.exe xD):

So, to read the abstract files, I create 2 structures: a resource and a problem, which look like this:

 typedef struct _resource { unsigned int numShop; unsigned int numJob; unsigned int value; } Resource; typedef struct _problem { unsigned int nbShops; unsigned int nbJobs; Resource** resources; } Problem; 

Reading is fine, and I have all the information in the input files inside my structures.

I want to convert this optimal problem (find the best solution) into a solution problem (Is this the possible solution?), And for this my goal is to turn the JobShop / FlowShop task into a SAT problem.

• My goal is this: I set the value of C_max to fixed, I am creating a SAT problem, and I will reduce C_max until the SAT solver says that the problem has no solution. The last value with the solution will be the optimal value.

Thanks @Jens Schauder, I have a start to the solution. My boolean variables look like this: s_1_2_3 with the meaning resource one gets used at machine 2 starting from time 3 .

So, if I have J-tasks, M stores, and I put my C_max on the value of C, I will definitely know: J * M * C booleans variables.

Problem: At the moment, my problem with SAT is incorrect. The solution given does not fit.

Here are the limitations that I have now: (V means "OR", another: "AND")

• 

This means that task I can only be in one store during time k

• 

This means that store j can only process one job in time k.

• 

This means that if the task has a duration of more than 1, it should be conditional. Therefore, if one variable is true, the other after the expiration of the task must also be true.

I am not sure if I formulated the problem correctly and / or if I forgot the restriction.

At present, I don’t remember how the Job Shop (Flow Shop is basically the same where jobs have to be in the same order in each store)

Sorry for the very big question, but for this problem it is better to have all the details in order to know what is at stake.

---

EDIT

I will add the source code from 3 contraindications, maybe something is wrong inside, and I do not see that ...

Limit n ° 1:

 /** the job i can be on only 1 shop for a time k */ unsigned int writeConstraintOne(Problem* problem, unsigned int timeMax, FILE* file, char forReal) { unsigned int final = 0; unsigned int max = getNbVariables(problem,timeMax); for(unsigned int i = 0; i < problem->nbShops; i++) { for(unsigned int l = 0; l < problem->nbShops; l++) { for(unsigned int j = 0; j < problem->nbJobs; j++) { for(unsigned int t = 0; t < timeMax; t++) { if(i == l) continue; /** We get the S_i_j_t */ unsigned int A = getIdOfVariable(problem,i,j,t,timeMax); /** We get the S_l_j_t */ unsigned int B = getIdOfVariable(problem,l,j,t,timeMax); final++; /* This fonction will or count the number of clauses, * or write them inside the file. */ if(forReal == 1) { /* It represents -A => B */ fprintf(file,"-%d -%d 0\n",A,B); } } } } } return final; } 

Limit n ° 2:

 /** shop j can handle only 1 job for a time k. */ unsigned int writeConstraintTwo(Problem* problem, unsigned int timeMax, FILE* file, char forReal) { unsigned int final = 0; unsigned int max = getNbVariables(problem,timeMax); for(unsigned int i = 0; i < problem->nbShops; i++) { for(unsigned int l = 0; l < problem->nbJobs; l++) { for(unsigned int j = 0; j < problem->nbJobs; j++) { for(unsigned int t = 0; t < timeMax; t++) { if(j == l) continue; /** We get the S_i_j_t */ unsigned int A = getIdOfVariable(problem,i,j,t,timeMax); /** We get the S_i_l_t */ unsigned int B = getIdOfVariable(problem,i,l,t,timeMax); final++; /* This fonction will or count the number of clauses, * or write them inside the file. */ if(forReal == 1) { /* It represents -A => B */ fprintf(file,"-%d -%d 0\n",A,B); } } } } } return final; } 

Limitation n ° 3:

 /** if the job has a duration more than 1, it has to be contineous. * So if one variable is true, the other after until the end of duration * of the task have to be true also. */ unsigned int writeConstraintThree(Problem* problem, unsigned int timeMax, FILE* file, char forReal) { unsigned int final = 0; unsigned int max = getNbVariables(problem,timeMax); for(unsigned int i = 0; i < problem->nbShops; i++) { for(unsigned int j = 0; j < problem->nbJobs; j++) { for(unsigned int t = 0; t < timeMax; t++) { for(unsigned int k = 0; k < problem->resource[i][j].value-1; k++) { if(k == t) continue; /** We get the S_i_j_t */ unsigned int A = getIdOfVariable(problem,i,j,t,timeMax); /** We get the S_i_j_k */ unsigned int B = getIdOfVariable(problem,i,j,k,timeMax); final+= 2; /* This fonction will or count the number of clauses, * or write them inside the file. */ if(forReal == 1) { fprintf(file,"-%d %d 0\n",B,A); fprintf(file,"-%d %d 0\n",A,B); } } } } } return final; } 

Answer 1

There is an error in the first two equations: you are missing l! = J. Of course, I do not know if this error is in your code.

I think that you also lack the limitation that states: each work must be performed on each machine at least once (you have only one part).

As an additional hint for debugging this: try it with the simplest examples that are possible: 1 machine, 1 job; and work from there to 2 cars, 1 work and 1 car 2 jobs.

With two cars and three jobs, a lot can go wrong.