%% Copyright (C) 2005 Igor Stéphan
%% 
%% This program is free software; you can redistribute it and/or
%% modify it under the terms of the GNU General Public License
%% as published by the Free Software Foundation; either version 2
%% of the License, or (at your option) any later version.
%% 
%% This program is distributed in the hope that it will be useful,
%% but WITHOUT ANY WARRANTY; without even the implied warranty of
%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
%% GNU General Public License for more details.
%% 
%% You should have received a copy of the GNU General Public License
%% along with this program; if not, write to the Free Software
%% Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
%% http:%%www.gnu.org/copyleft/gpl.html
%%
%% igor.stephan@univ-angers.fr
%% 

:- use_module('ELIMINATION_BL_QBF_CNF', [elimination_bl_qbf_cnf/3]).
:- use_module('BASE_LITTERALE', [interpretation/2]).
:- use_module(library(clpb)).



% | ?- elimination_bl_qbf_cnf([e(A),e(B),e(C),e(D)],[[~A, ~B, ~C, D],[~A,~B,C,~D],[~A, B,C, ~D],[~A, B,C, D],[A, ~B,~C, D],[A,~B,C,D],[A, B,C, ~D],[A, B,C, D]], _BL), interpretation(_BL, _F), sat(_F), labeling([A,B,C,D]).
% A = 1,
% B = 1,
% C = 0,
% D = 0 ? ;
% A = 0,
% B = 1,
% C = 0,
% D = 1 ? ;
% A = 0,
% B = 0,
% C = 1,
% D = 0 ? ;
% A = 1,
% B = 0,
% C = 1,
% D = 0 ? ;
% A = 0,
% B = 0,
% C = 1,
% D = 1 ? ;
% A = 0,
% B = 1,
% C = 1,
% D = 1 ? ;
% A = 1,
% B = 0,
% C = 1,
% D = 1 ? ;
% A = 1,
% B = 1,
% C = 1,
% D = 1 ? ;
% no

% | ?- elimination_bl_qbf_cnf([a(A),e(B),a(C),e(D)],[[~A, ~B, ~C, D],[~A,~B,C,~D],[~A, B,C, ~D],[~A, B,C, D],[A, ~B,~C, D],[A,~B,C,D],[A, B,C, ~D],[A, B,C, D]], _BL), interpretation(_BL, _F), sat(_F), labeling([A,B,C,D]).
% A = 1,
% B = 1,
% C = 0,
% D = 0 ? ;
% A = 0,
% B = 1,
% C = 0,
% D = 1 ? ;
% A = 0,
% B = 1,
% C = 1,
% D = 1 ? ;
% A = 1,
% B = 1,
% C = 1,
% D = 1 ? ;
% no