2

我正在为一项任务寻求帮助。我必须（用 C 语言）编写一个算法来解决合取正规公式（cnf），几个小时后我无法让它工作......

我的程序实现了DPLL，更准确地说，这是我在选择要实例化的文字之后简化我的 cnf 的部分，这给我带来了问题。我不确定我是否很清楚，所以这里有一个例子：

公式： (a OR b) AND (not-a OR not-b) AND (not-a OR b)

实例化：a=TRUE b=FALSE

如果我此时使用我的函数简化，我应该以 (not-a OR 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;
  }
}

对于长长的代码，我很抱歉，我不知道要关注什么重要的部分。我知道还有其他几个问题，例如未完成的内存释放（我认为）。

除此之外，我在尝试调试问题时发现了几个错误，但我感觉我在纠正旧问题的同时创建了新错误：/

如果有人可以帮助我，请提前谢谢！另外，我在 Windows 10 上，通过 cygwin 使用 gcc 编译，如果重要的话：

gcc *.c

4

1 回答 1

1

另外，我在 Windows 10 上，通过 cygwin 用 gcc 编译，如果它很重要的话

实际上是......我很确定这与我之前没有检查过的那件事无关，然后在写这篇文章时它似乎不再那么不重要了。

无论如何，我在 linux 系统上进行了尝试，乍一看它似乎工作正常。

带来不便敬请谅解

于 2016-04-04T18:37:35.350 回答