function KB3PSAT = BR_PSAT2PSAT3(KB)
% BR_PSAT2PSAT3 - convert a probabilistic CNF KB to a 3CNF probabilistic KB
% On input:
%     KB (KB structure): CNF probabilistic knowledge base
% On output:
%     KB3PSAT (KB structure): 3CNF probabilistic knowledge base
% Call:
%     KB3 = BR_PSAT23PSAT(KB);
% Author:
%     T. Henderson
%     UU
%     Summer 2018
%

KB3PSAT = [];
len_KB3PSAT = 0;
num_clauses = length(KB);
vars = BR_vars(KB,[]);
num_vars = max(vars);

for c = 1:num_clauses
    clause = KB(c).clauses;
    p = KB(c).prob;
    len_clause = length(clause);
    if len_clause<4
        len_KB3PSAT = len_KB3PSAT + 1;
        KB3PSAT(len_KB3PSAT).clauses = clause;
        KB3PSAT(len_KB3PSAT).prob = p;
    else
        num_new_clauses = len_clause - 2;
        len_KB3PSAT = len_KB3PSAT + 1;
        new_vars = [num_vars+1:num_vars+(len_clause-3)];
        num_new_vars = length(new_vars);
        num_times = len_clause - 4;
        pp = BR_3PSAT(KB(c));
        KB3PSAT(len_KB3PSAT).clauses = [clause(1:2),new_vars(1)];
        KB3PSAT(len_KB3PSAT).prob = pp;
        for cc = 1:num_times
            len_KB3PSAT = len_KB3PSAT + 1;
            KB3PSAT(len_KB3PSAT).clauses = [clause(cc+2),...
                -new_vars(cc),new_vars(cc+1)];
            KB3PSAT(len_KB3PSAT).prob = pp;
        end
        len_KB3PSAT = len_KB3PSAT + 1;
        KB3PSAT(len_KB3PSAT).clauses = [clause(end-1:end),-new_vars(end)];
        KB3PSAT(len_KB3PSAT).prob = pp;
        num_vars = num_vars + num_new_vars;
    end
end

%---------------------------------------------------------------
function vars = BR_vars(KB,sentence)
% BR_vars - find list of variables in logical sentences
% On input:
%     KB (nx1 conjunctive normal form vector): conjunctive clauses
%       (i).clauses (1xm vector): disjunctive clause
%     sentence (1x1 conjunctive normal form vector): conjunctive clause
%       (1).clauses (1xk vector): disjunctive clause
% On output:
%     vars (1xp vector): list of variables in KB and sentence
% Call:
%     vars = BR_vars(KB,thm);
% Author:
%     T. Henderson
%     UU
%     Spring 2017
%

vars = [];

for s = 1:length(KB)
    vars = unique([vars,abs(KB(s).clauses)]);
end
for s = 1:length(sentence)
    vars = unique([vars,abs(sentence(s).clauses)]);
end
vars = sort(vars);
