Cで結ばれた正規形を解く

Question

私は代入の助けを求めています。私は（Cで）積標準式（CNF）を解決し、かなりの数時間後、私はそれを動作させることができないアルゴリズムを記述する必要が ...

私のプログラムはDPLLを実装し、より正確にそれはインスタンス化するリテラルを選択した直後に私のcnfを単純化する部分です。それが問題になります。 私はので、ここで非常に明確だ場合の例ではわからない：

式：（AまたはB）AND（ない-Aまたはない-B）AND（ない-AまたはB）

インスタンス：

FALSE = TRUE B =私は私の関数は、この時点で簡素化を使用する場合、私は（ない-AまたはB）不満足なもので終わる必要がありますが、それはすべての句が満たされていることを私に伝えます。ここで

は（それは管理が容易に見えたとして私は、代わりにリテラルの文字の整数を使用）、私が定義したデータ型です：

#define TRUE 1 
#define FALSE 0 
#define UNDEF -1 

typedef int literal; 

typedef int* interpretation; 

typedef struct node { 
    literal lit; 
    struct node* next; 
} * clause; 

typedef struct _formula { 
    clause c; 
    struct _formula* next; 
} * formula; 

typedef struct _cnf { 
    int nb_lit; 
    formula f; 
} * cnf; 

そして、ここで私の簡素化機能がある

void simplify(cnf F, interpretation I) { 
    clause pred, curr; 
    int skip,b=FALSE; 
    formula form, parentForm; 
    form = F->f; 
    parentForm = form; 

    // Iterating through each clause of the formula 
    while (form != NULL) { 
    curr = form->c; 
    pred = curr; 
    skip = FALSE; 
    while (curr != NULL && !skip) { 
     b = FALSE; 
     // If a literal appears as true and has benn interpreted as true 
     if (curr->lit > 0 && I[curr->lit] == TRUE) { 
     // We remove the current clause from the formula 
     if (parentForm == form) { 
      F->f = form->next; 
      free(form); 
      form = F->f; 
      parentForm = form; 
     } else { 
      parentForm->next = form->next; 
      free(form); 
      form = parentForm->next; 
     } 
     skip = TRUE; 
     } 
     // Same goes with false 
     if (curr->lit < 0 && I[-curr->lit] == FALSE) { 
     if (parentForm == form) { 
      F->f = form->next; 
      free(form); 
      form = F->f; 
      parentForm = form; 
     } else { 
      parentForm->next = form->next; 
      free(form); 
      form = parentForm->next; 
     } 
     skip = TRUE; 
     } 

     // However if a literal appears as true and is interpreted as false (or 
     // the opposite) 
     if (curr->lit > 0 && I[curr->lit] == FALSE) { 
     // We remove it from the clause 
     if(pred == curr) 
     { 
      curr = curr->next; 
      free(pred); 
      form->c = curr; 
      pred = curr; 
      b=TRUE; 
     } 
     else 
     { 
      pred->next = curr->next; 
      free(curr); 
      pred = curr; 
     } 
     } 
     else if (curr->lit < 0 && I[-curr->lit] == TRUE) { 
     if(pred == curr) 
     { 
      curr = curr->next; 
      free(pred); 
      form->c = curr; 
      pred = curr; 
      b=TRUE; 
     } 
     else 
     { 
      pred->next = curr->next; 
      free(curr); 
      pred = curr; 
     } 
     } 

     pred = curr; 
     if(!b) curr = curr->next; 
    } 
    parentForm = form; 
    if(!skip) form = form->next; 
    } 
} 

コードの長さが長いのは残念ですが、どのような重要な部分に焦点を当てるのか正確にはわかりません。私はいくつかの他の問題が残っていることを知っています。完全ではない記憶を解放するようなものです（私は思います）。/

Thxをを事前に誰もがこの上で私を助けることができる場合：それとは別に、私の問題をデバッグしようとしているときに、私はいくつかのエラーを発見したが、私は古いものを補正しながら、私は新しいものを作成する気持ちを持って

！それが重要だ場合にも、私は、cygwinの経由gccでコンパイルし、窓10によ：

GCCの* .c

Answer 1

また、私はを通じてgccでコンパイルし、窓10によcygwinの、それは重要だ場合、実際

それだった...私はそれが私が先にチェックしていなかった、と記事を書いている間、それは重要でないことを思えなかったということとは何の関係もないだろうそう確信していましたもう

とにかく、私はLinuxシステムで試してみましたが、一見するとうまくいくようです。

不便