%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Knowledge Representation and Reasoning CSC 486/2506, Fall 2006
%
% Sample file for exercise 4, assignment 1 (Prolog implementation)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%




%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% solve_tab_sat(C): C is a list of clauses where each clause is a 
%                   list of literals.
%
% for instance this is possible clause where literals are
% represented with integers:
%
%      [[1, -2], [2, -8], [-5, -4, 3], [5], [4, -2, -6]
%
% YOU SHOULD IMPLEMENT THIS PREDICATE. THE PREDICATE SHOULD PRINT
% "YES" IF C IS SATISFIABLE AND "NO" OTHERWISE
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% this implementation only prints the set of clauses, you should
% implement your program here.
solve_tab_sat(C):- write(C).

%      <<< HERE YOU SHOULD WRITE YOUR PROGRAM TO
%                 TEST SATISFIABILITY USING THE TABLEAU METHOD >>












% Also you will have to implement your code for performing your 
% experiments to confirm (or refute) the easy-hard-easy pattern
% around 4.2n on sets of clauses randomly generated.
% For this YOU will write code to generate clauses in the appropiate
% input format, and you will use solve_tab_sat/1 for stating the
% satifiablity of these random generated clauses.















%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%           OBS: You should not modify anything below 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% tabSat(File): takes a file name, reads its clauses and calls
%               solve_tab_sat/1 with such set of clauses
%
%
% This should work under SWI and Quintus Prolog (tested)
%
% DO NOT CHANGE
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
tabSat(File) :-
        open(File,read,R),	  % Opens the file
        read_clauses(R, Clauses), % Reads the clauses in the file
	close(R),                 % Close the file
        solve_tab_sat(Clauses).   % Call solve_horn_sat with list of clauses


read_clauses(R, LC) :- read(R, C),
	( C = [end] -> LC=[] ; (read_clauses(R,LC2), LC=[C|LC2]) ).