Creating a Groebner Basis SAT Solver in Prolog

Question

I am trying to create a SAT solver which converts from Conjunctive Normal Form (CNF) with an implementation of Boolean Grobner Bases:

a) Negation of a particular variable, e.g. -x will be converted to 1+x.
b) Adding the same variable will results in 0. e.g. x + x = 0. (will need to use XOR).
c) Multiplication of the same variable will result in the same variable. e.g. x*x = x.

At the moment, I am still trying to figure out how to start, as the input must be in text file, like those they have in SAT competition, where it is as follows :

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

Thanks.

EDIT

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

To have a Groebner Basis driven SAT solver, when using the usual integer polynomial quotient approach, you would need to use the George Boole translation of Boolean logic:

a) Negation ~x will be converted to 1-x.

b) Conjunction, Disjunction is the following x&y = xy, x v y = x+y-xy.

c) Yes, you need to add the Boole condition x*(x-1) = 0, which says that x is either 0 or 1. But you can easily see that this is the same as saying x*x = x.

But restricting the polynomial coefficients to 0,1 doesn't work, since for example the Xor needs already the coefficient 2:

x xor y = x + y - 2xy

This works indeed, although it is a little slow. To check whether a formula A is a Tautology you can let the Gröbner Basis algorithm run over ~A plus all the equations c). If the result is only the equations c) the formula is generally valid.

For some code:
https://gist.github.com/jburse/99d9a636fd6218bac8c380c093e06287#gistcomment-2032509

An alternative approach would be to use a Boolean ring, and corresponding polynomials. You would then not need to state the condition c), since it is automatically satisfied.