% The dclauses in DL are satisfied by picking Lits.
sat(DL,Lits) :- satpick(DL,[],Lits).

% satpick(DL,P,Lits): the dclauses in DL can be satisfied by
% picking the literals in Lits, given that those in P are taken.
satpick([],P,P).
satpick([D|DL],P1,Lits) :- pickone(D,P1,P2), satpick(DL,P2,Lits).

pickone([L|_],P,P) :- member(L,P).             % L is picked.
pickone([L|_],P,[L|P]) :- \+ member_neg(L,P).  % ~L is not picked.
pickone([_|D],P,P2) :- pickone(D,P,P2).        % Use D instead.

member_neg(A,P) :- member(not(A),P).
member_neg(not(A),P) :- member(A,P).
