prolog - 在Prolog中创建Groebner Basis SAT解算器

我正在尝试创建一个SAT解算器，该解算器使用布尔Grobner Bases的实现从合取范式（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).

最佳答案

要使用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öbnerBasis算法在〜A以及所有方程c）之上运行。如果结果仅是方程式c），则该公式通常有效。

对于一些代码：
https://gist.github.com/jburse/99d9a636fd6218bac8c380c093e06287#gistcomment-2032509

一种替代方法是使用布尔环和相应的多项式。然后，您将无需陈述条件c），因为它会自动满足。

关于prolog - 在Prolog中创建Groebner Basis SAT解算器，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/45710034/