An (unfinished) implementation of an SAT solver using Constraint Handling Rules

SAT_Solver.pl

:- use_module(library(chr)).
:- initialization(main).
:- chr_constraint is_true(+).
is_true(A) \ is_true(A) <=> true.

:- chr_constraint are_true(+).
are_true(A) \ are_true(A) <=> true.

:- chr_constraint is_false(+).
is_false(A) \ is_false(A) <=> true.

is_true(A),is_false(A) <=> false.

is_true(is_false(A)) <=> is_false(A).

is_true(awake(A)),is_true(asleep(A)) <=> false.

is_true(B) ==> 
	Expr = (((is_true(animal(A)),is_true(alive(A))),
	(is_true(awake(A));is_true(asleep(A))));	
	is_false(animal(A)),is_false(awake(A)),is_false(asleep(A))),
	recursive_search(is_true(B),Expr)| call(Expr).

is_true(B) ==> 
	Expr = (is_true(vehicle(A)),(is_true(plane(A));is_true(car(A));is_true(ship(A)))),
	recursive_search(is_true(B),Expr) | call(Expr).

is_true(B) ==> 
	Expr = (is_true(like_each_other(A,A1)),is_true(likes(A,A1)),is_true(likes(A1,A))),
	recursive_search(is_true(B),Expr) | call(Expr).


are_true([]) <=> true.
are_true([A|B]) <=> is_true(A),are_true(B).

is_true(A) ==> writeln(A).
is_false(A) ==> writeln([A,'is false']).

main :- are_true([awake(bob),plane(derp),likes(bob,bob1)]).

recursive_search(A,A).
recursive_search(A,C) :- member(C,[(A1,B),(A1;B)]),(recursive_search(A,A1);recursive_search(A,B)).
recursive_search(A1,C) :- member(C,[is_false(A),is_true(A)]),(A1=C;recursive_search(A1,A)).