我正在为一项作业寻求帮助。 我必须(用 C 语言)编写一个算法来求解 union 正规公式 (cnf),但几个小时后我无法让它工作...
我的程序实现了 DPLL ,更准确地说,这是我简化我的 cnf 的部分,在选择要实例化的文字之后,这给我带来了问题。 我不确定我是否很清楚,所以这里有一个例子:
Formula : (a OR b) AND (not-a OR not-b) AND (not-a OR b)
Instantiation : a=TRUE b=FALSE
如果此时我使用我的函数 simplify ,我应该以 (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
最佳答案
Also, I'm on windows 10, compiling with gcc through cygwin, if it's important
实际上它是......我非常确定它与我没有早点检查的事情无关,然后在写这篇文章时它似乎不再那么不重要了。
无论如何,我在 linux 系统上试过,乍一看它似乎工作正常。
抱歉给您带来的不便
关于c - 在 C 中求解合取范式,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/36409782/