c - Flow/Job Shop 到 bool 可满足性 [多项式时间缩减] 第 2 部分

Question

这是我第一个问题 (Flow Shop to Boolean satisfiability [Polynomial-time reduction]) 的连续性。

因为出了点问题，我没能知道确切的位置。再次求助StackOverFlow的高手:)

我现在的总结:

• 我有这样的输入文件:

3 2
1 1 1
1 1 1

Who represents : 3 jobs, 2 shops (machines), and the duration of each job on each shop (machine). And I want for theses problems, to find the optimum C_max value.

例如，它应该在输出中给出这个结果(对 paint.exe xD 感到抱歉):

为了阅读这些文件，我创建了 2 个结构:资源和问题，如下所示:

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;

读取没问题，我的结构中有输入文件中的所有信息。

我想将这个最优问题(找到最佳解决方案)转化为决策问题(这是一个可能的解决方案吗？)为此，我的目标是将 JobShop/FlowShop 问题转化为 SAT 问题。

• 我的目标如下:我将 C_max 的值设置为固定值，我创建了一个 SAT 问题，并且我将减少 C_max 直到 SAT 求解器表明该问题无解。具有解决方案的最后一个值将是最优值。

感谢@Jens Schauder，我有了解决方案的开始。我的 bool 变量是这样的:s_1_2_3，意思是资源一从时间 3 开始在机器 2 上使用。

因此，如果我有 J 个工作，M 个商店，并且我将 C_max 的值设为 C，我肯定会得到:J * M * C bool 变量。

问题:目前我的 SAT 问题是错误的。给出的解决方案不行。

这是我现在的限制条件:(V 表示“或”，另一个:“和”)

• >

这意味着工作 i 一次只能在 1 个商店工作 k

• >

这意味着商店 j 在时间 k 内只能处理 1 个工作。

• >

这意味着如果作业的持续时间超过 1，则它必须是连续的。因此，如果一个变量为真，则直到任务持续时间结束后的另一个变量也必须为真。

我不太确定我对问题的表述是否正确，或者/以及我是否忘记了约束条件。

现在，我还介意 Job Shop(Flow Shop 基本上是相同的，每个商店的作业必须以相同的顺序排列)

很抱歉问了这么大的问题，但是对于这种问题，最好有所有的细节来了解它是关于什么的。

---

编辑

我把上面3个约束的源码加进去，可能里面有问题，没看出来是什么……

约束 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;
 }

约束 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;
 }

约束 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

您给出的前两个等式中存在错误:您缺少 l != j。当然，我不知道这个错误是否也存在于您的代码中。

我认为您还缺少一个约束条件:每项工作必须在每台机器上至少发生一次(您只有最多一次的部分)。

关于调试的更多提示:用最简单的例子尝试:1 台机器，1 个工作；然后从那里工作到 2 台机器，1 个工作和 1 台机器 2 个工作。

有 2 台机器和三个工作，可能会出错的地方太多了。