3

Boolean Grobner Bases の実装を使用して、結合正規形 (CNF) から変換する SAT ソルバーを作成しようとしています。

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 Basis 駆動の SAT ソルバーを使用するには、通常の整数多項式商アプローチを使用する場合、ブール論理のジョージ ブール変換を使用する必要があります。

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 がトートロジーであるかどうかを調べるには、グレブナー基底アルゴリズムを ~A とすべての方程式 c) に対して実行させることができます。結果が式 c) のみの場合、その式は一般的に有効です。

一部のコード:
https://gist.github.com/jburse/99d9a636fd6218bac8c380c093e06287#gistcomment-2032509

別のアプローチは、ブール環と対応する多項式を使用することです。条件 c) は自動的に満たされるため、これを記述する必要はありません。

于 2018-11-01T13:37:03.133 に答える