3

我正在尝试创建一个 SAT 求解器，它通过 Boolean Grobner Bases 的实现从结合范式 (CNF) 转换：

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

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

p cnf 3 4 
1 3 -2 0
3 1 0
-1 2 0
2 3 1 0

谢谢。

编辑

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).
4

1 回答 1

1

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

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

b) 合取，析取如下x&y = x y, xvy = x+yx y。

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)，因为它是自动满足的。

于 2018-11-01T13:37:03.133 回答