これが私の最初の質問の続きです（フローショップからブール充足可能性へ[多項式時間削減]）。
何かが間違っていて、正確な場所を知ることができなかったからです。もう一度、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 問題を作成し、SAT ソルバーが問題に解決策がないことを示すまで C_max を減らします。解のある最後の値が最適値になります。
@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」を意味し、他の：「そして」を意味します）
これは、私が一度に 1 つのショップでしか働けないことを意味します k
つまり、ショップ j は、時間 k に 1 つのジョブしか処理できません。
つまり、ジョブの期間が 1 を超える場合は、継続的でなければなりません。したがって、1 つの変数が true の場合、タスクの期間が終了するまで他の変数も true である必要があります。
問題の定式化について私が正しいかどうか、または/および制約を忘れたかどうかはよくわかりません。
今のところ、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;
}