在 Prolog 中创建 Groebner 基础 SAT 求解器答案

【问题标题】：Creating a Groebner Basis SAT Solver in Prolog在 Prolog 中创建 Groebner 基础 SAT 求解器
【发布时间】：2018-01-24 09:19:41
【问题描述】：

我正在尝试创建一个 SAT 求解器，它通过布尔格罗布纳基的实现从联合范式 (CNF) 转换：

a) 对特定变量的否定，例如-x 将转换为 1+x。
b）添加相同的变量将导致 0。例如x + x = 0。（需要使用 XOR）。
c) 相同变量的乘法将产生相同的变量。例如x*x = x。

目前，我还在想如何开始，因为输入必须是文本文件，就像他们在 SAT 比赛中一样，如下所示：

谢谢。

编辑

parser :-
    open(File, read, Stream),
    read_literals(Stream,Literals),
    close(Stream),
    read_clauses(Literals,[],Clauses),
    write(Clauses).

read_literals(Stream,Literals) :-
    get_char(Stream,C),
    read_literals(C,Stream,Literals).

read_literals(end_of_file,_Stream,Literals) :-
    !,
    Literals = [].

read_literals(' ',Stream,Literals) :-
    !,
    read_literals(Stream,Literals).

read_line_then_literals('\n',Stream,Literals) :-
    !,
    read_literals(Stream,Literals).

read_line_then_literals(_C,Stream,Literals) :- 
    read_line_then_literals(Stream,Literals).

read_literal_then_literals(Stream,As,Literals) :-
    get_char(Stream,C),
    read_literal_then_literals(C,Stream,As,Literals). 

read_literal_then_literals(C,Stream,As,Literals) :-
    digit(C),
    !,
    name(C,[A]),
    read_literal_then_literals(Stream,[A|As],Literals).

read_literal_then_literals(C,Stream,As,Literals) :-
    reverse(As,RevAs),
    name(Literal,RevAs), 
    Literals = [Literal|Rest_Literals],
    read_literals(C,Stream,Rest_Literals).

digit('0').
digit('1').
digit('2').
digit('3').
digit('4').
digit('5').
digit('6').
digit('7').
digit('8').
digit('9').

read_clauses([],[],[]).

read_clauses([0|Literals],Clause,Clauses) :-
    !,
    reverse(Clause,RevClause),
    Clauses=[RevClause|RestClauses],
    read_clauses(Literals,[],RestClauses).

read_clauses([Literal|Literals],Clause,Clauses) :- 
    read_clauses(Literals,[Literal|Clause],Clauses).

【问题讨论】：

嗨，Guy Coder，目前，我找到了一种读取文本文件中字符串的方法。但是，我的主要问题是以 CNF 形式表示的字符串转换为 ANF 形式。您对如何开始/从哪里阅读有什么建议吗？
嗨，Guy Coder，我希望您已经设法解决了您的问题，并感谢您在忙碌的情况下抽出时间回复我。关于向 ANF 的转换，您认为使用 Prolog 可以做到吗？
嗨 Guy Coder，我的工作取得了一些进展。唯一的问题是，目前，当我看到一个负数（例如 -2）时，我想实现一个 not(X) = X - 1 的方法。您认为可以这样做吗？
目前我的代码如下
第 1 部分 parser :- open(File, read, Stream), read_literals(Stream,Literals), close(Stream), read_clauses(Literals,[],Clauses), write(Clauses). read_literals(Stream,Literals):- get_char(Stream,C), read_literals(C,Stream,Literals). read_literals(end_of_file,_Stream,Literals):- !, Literals=[]. read_literals(' ',Stream,Literals):- !, read_literals(Stream,Literals).

标签： prolog sat clpb

【解决方案1】：

要使用 Groebner 基础驱动的 SAT 求解器，在使用通常的整数多项式商方法时，您需要使用布尔逻辑的 George Boole 转换：

a) 否定 ~x 将被转换为 1-x。

b) 合取，析取如下x&y = xy, x v y = x+y-xy。

c) 是的，您需要添加布尔条件 x*(x-1) = 0，即 x 为 0 或 1。但您可以很容易地看到这与说 x*x = x.

但是将多项式系数限制为 0,1 是行不通的，因为例如 Xor 已经需要系数 2：

x xor y = x + y - 2xy

这确实有效，虽然它有点慢。要检查公式 A 是否是重言式，您可以让 Gröbner Basis 算法运行 ~A 加上所有方程 c)。如果结果只是方程 c) 公式一般是有效的。

部分代码：
https://gist.github.com/jburse/99d9a636fd6218bac8c380c093e06287#gistcomment-2032509

另一种方法是使用布尔环和相应的多项式。然后你就不需要陈述条件 c)，因为它是自动满足的。

【讨论】：