这是我的第一个问题的连续性（Flow Shop to Boolean satisfiability [Polynomial-time reduction]）。
因为出了点问题，我没有成功知道到底在哪里。再次向 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;
读数没问题，我的结构内的输入文件中有所有信息。
我想将这个最优问题（找到最佳解决方案）转换为决策问题（这是一个可能的解决方案吗？）为此，我的目标是将 JobShop/FlowShop 问题转换为 SAT 问题。
- 我的目标如下：我将 C_max 的值设置为固定值，我创建了一个 SAT 问题，我将减小 C_max 直到 SAT 求解器说问题没有解决方案。具有解决方案的最后一个值将是最佳值。
感谢@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 表示“或”，另一个：“和”）
这意味着我的工作只能在 1 家商店工作一段时间 k
这意味着商店 j 在时间 k 内只能处理一项工作。
这意味着如果作业的持续时间超过 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;
}