流量/作业车间到布尔可满足[多项式时间减少]第2部分(Flow/Job Shop to Boolea

这是我的第一个问题（的连续性流水车间到布尔可满足性[多项式时间减少] ）。

因为什么是错的，我也没成功，要知道确切位置。我问StackOverflow上的主人的帮助下再次:)

对于我目前拥有的总和，达到：

我有谁是这样的输入文件：

 3 2 1 1 1 1 1 1 
谁代表：3个工作，2个店（机），并在每个店铺（机）每个作业的时间。我想对论文的问题，找到最佳C_max值。

因此，例如，它应该给在输出这个结果（对不起，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;

阅读是没关系的，我有我的结构内部的输入文件中的所有信息。

我想要改造这个优化问题（找到最佳解决方案）为决策问题（这是一个可能的解决方案？），为此，我的目标是改造作业车间/流水作业问题转化为SAT问题。

我的目标是如下：我把C_max的值作为固定的，我创建了一个SAT问题，直到SAT-求解说，这个问题无解，我会减少C_max。最后的价值与解决方案将是最佳值。

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

所以，如果我有Ĵ工作，男店，我把我的C_max到C的值，我会肯定的： J * M * C布尔变量。

问题：现在我的SAT问题是错误的。 给出的解决方案是不行的。

下面是我对现在的约束条件：（V手段“或”，另：“和”）

这意味着这份工作，我可以在只有1个店一时间k

这意味着商店J可以获得只能处理1个作业的时间k。

这意味着，如果作业的持续时间大于1，它必须是contineous。所以，如果一个变量为真，前一后，直到任务的持续时间到底要真也。

我真的不知道，如果我是对这个问题的提法，或/和，如果我忘了约束。

现在，我心里也车间（流水作业的基本相同，其中的工作必须在每个店铺相同的顺序）

对不起，很大的问题，但这种问题，最好把所有的细节就知道它是什么。

编辑

我将添加了上述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;
 }

有一个在头两个等式你给了一个错误：你缺少一个L = J 1。当然，我不知道，如果这个bug是在你的代码。

我想你也缺少约束，上面写着：每个职业都有每个机器上发生至少一次（你只有最多一次部分）。

在用于调试这更暗示：用了可能的最简单的例子来尝试：1个机1组的工作; 和工作从那里到2台，1个作业和1个机2点的工作。

随着2台和三个工作，也得多可能出错。