Создание SAT Солвера на основе Groebner в Прологе

Question

Я пытаюсь создать SAT-решатель, который конвертирует из конъюнктивной нормальной формы (CNF) с помощью реализации логических баз Гробнера:

а) отрицание конкретной переменной, например -x будет преобразован в 1+x,
б) Добавление той же переменной приведет к 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). 

Answer 1

Чтобы использовать SAT-решатель на основе Groebner Basis, при использовании обычного подхода с целочисленным полиномиальным отношением вам потребуется использовать булеву логику Джорджа Буля:

а) Отрицание ~ х будет преобразовано в 1-х.

б) Конъюнкция, дизъюнкция - это x & y = xy, xvy = x + yx y.

c) Да, вам нужно добавить условие Boole x*(x-1) = 0, которое говорит, что x равно 0 или 1. Но вы можете легко увидеть, что это то же самое, что сказать x*x = x.

Но ограничение полиномиальных коэффициентов до 0,1 не работает, поскольку, например, Xor уже нужен коэффициент 2:

x xor y = x + y - 2xy

Это действительно работает, хотя и немного медленно. Чтобы проверить, является ли формула A тавтологией, вы можете позволить алгоритму Грёбнера-Базиса работать над ~A плюс все уравнения c). Если результатом являются только уравнения в) формула в целом верна.

Для некоторого кода:
https://gist.github.com/jburse/99d9a636fd6218bac8c380c093e06287

Альтернативным подходом было бы использование булева кольца и соответствующих полиномов. Тогда вам не нужно будет указывать условие с), поскольку оно автоматически выполняется.