3

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).
piyo_kuro
  • 105
  • 9
  • Hi Guy Coder, at the moment, I have found a way to read the strings in the text file. However, my main problem is to convert the strings which are represented in CNF form into ANF form. Do you have any suggestions on how to start / where to read so I can do a little more codes? – piyo_kuro Aug 16 '17 at 12:51
  • Hi Guy Coder, I do hope you have managed to solve your problem and thank you for taking your time to reply me despite you are busy. Regarding the conversion to ANF, do you think it is possible to do it using Prolog? – piyo_kuro Aug 18 '17 at 14:30
  • Hi Guy Coder, I had some progress with my work. The only problem is that at the moment, when I see a negative number (e.g. -2), I want to implement a method where not(X) = X - 1. Do you think it is possible to do so? – piyo_kuro Aug 21 '17 at 11:35
  • At the moment my code is as follows – piyo_kuro Aug 21 '17 at 21:54
  • part 1 `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).` – piyo_kuro Aug 21 '17 at 21:56
  • part 2 `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).` – piyo_kuro Aug 21 '17 at 21:58
  • part 3 ` 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').` – piyo_kuro Aug 21 '17 at 21:59
  • part 4 `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).` – piyo_kuro Aug 21 '17 at 21:59
  • How does `File` get passed to the predicate `Parser`? Can you give a few examples of the input with the expected output? What uses the predicate `read_literal_then_literals`? Is all of the code here? – Guy Coder Aug 22 '17 at 15:20
  • the File is actually replaced by the address of the cnf file. – piyo_kuro Aug 26 '17 at 10:50

1 Answers1

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.