Flow/Job 布尔可满足性 [多项式时间缩减] 第 2 部分

Question

这是我第一个问题的连续性（）。

因为出了点问题，我没能知道具体在哪里。再次求助Whosebug的高手:)

我现在的总结：

我有这样的输入文件：

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-solver 说问题已经解决没有解决方案。具有解决方案的最后一个值将是最佳值。

感谢@Jens Schauder，我有了解决方案的开始。我的布尔变量是这样的：s_1_2_3 with the meaning resource one gets used at machine 2 starting from time 3.

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

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

这是我目前的限制条件：（V 表示 'OR'，另一个：'And'）

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

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

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

我不太确定我对问题的表述是否正确，or/and 如果我忘记了约束。

现在，我还介意作业车间（流水车间基本上是一样的，每个车间的作业必须以相同的顺序排列）

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

编辑

我把上面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 台机器和三个工作，可能出错的地方太多了。

Flow/Job 布尔可满足性 [多项式时间缩减] 第 2 部分

Flow/Job Shop to Boolean satisfiability [Polynomial-time reduction] part 2

c

algorithm

optimization

reduction

sat