function pp = BR_3PSAT(C)
% BR_2PSAT - converts a CNF clause of length k to a set of clauses each of
%     which has at most 3 terms (disjuncts)
% On input:
%     C (KB structure element): one element of a KB
%       C.clauses (vector): disjunction
%       C.prob (float): probability of clause
% On output:
%     pp (float): probability of new clauses
% Call:
%     pp = BR_3PSAT(KB(1));
% Author:
%     T. Henderson
%     UU
%     Fall 2018
%

k = length(C.clauses);
p = C.prob;
kp = k - 2;
Nv = 2*k - 3;
Ncc = 2^Nv;
Nt = 2^(2*k-4) + 2^(2*k-5) + 2^(2*k-6);
Nf = Ncc - Nt;
No = (kp-1)*(kp-2)*2^(kp-3);
Nand = Ncc - (kp*Nf-No);
pa = p/Nand;
pn = (1-p)/(Ncc-Nand);
pp = p + (Nt-Nand)*pn;
res = [k,kp,Nv,Ncc,Nt,Nf,No,Nand]';
resp = [p,pa,pn,pp]';
