在C中解決連接的標準形式

Question

我在尋求幫助。我需要寫一個算法來解決一個連接正規公式（cnf），並且在幾個小時後我不能使它工作...

我的程序實現DPLL，並且更精確，這是我簡化了我的cnf的部分，在選擇一個文字實例化之後，導致了我的問題。 我不知道如果我很清楚，所以這裏有一個例子：

公式：（A或B）和（非A或不-b）和（非A或B）

實例化：A = TRUE b = FALSE

如果我用我的功能在這一點上簡化了，我應該結束了（非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提前如果有人能幫助我在這！另外，我在Windows 10，通過cygwin的用gcc編譯，如果它是很重要的：

GCC的* .c

Answer 1

此外，我在Windows 10，通過用gcc編譯Cygwin的，如果它是重要的

其實這是......我很確信它什麼都沒有做與我沒有早檢查，然後一邊寫帖子似乎並不認爲不重要了。

無論如何，我嘗試在Linux系統上，乍一看它似乎工作正常。

很抱歉給您帶來不便