(* ::Package:: *)

BeginPackage["formulas`"]

formulas::usage="Pacote que disponibiliza uma implementa\[CCedilla]\[ATilde]o de f\[OAcute]rmulas proposicionais em forma normal conjuntiva"

randcnf::usage="randcnf[k,n] constr\[OAcute]i uma forma normal conjuntiva aleat\[OAcute]ria com n cl\[AAcute]usulas em k vari\[AAcute]veis"

numclaus::usage="numclaus[cnf] devolve o n\[UAcute]mero de c\[EAcute]lulas da forma normal conjuntiva cnf"

numvars::usage="numvars[cnf] devolve o n\[UAcute]mero de vari\[AAcute]veis da forma normal conjuntiva cnf"

satisfazQ::usage="satisfazQ[cnf,b] verifica se a f\[OAcute]rmula cnf \[EAcute] satisfeita quando \[AGrave] sua i-\[EAcute]sima vari\[AAcute]vel \[EAcute] atribu\[IAcute]do o valor l\[OAcute]gico b[[i]], para 1\[LessEqual]i\[LessEqual]Length[b]"

numsatclaus::usage="numsatclaus[cnf,b] devolve o n\[UAcute]mero de cl\[AAcute]usulas da f\[OAcute]rmula cnf que s\[ATilde]o satisfeitas quando \[AGrave] sua i-\[EAcute]sima vari\[AAcute]vel \[EAcute] atribu\[IAcute]do o valor l\[OAcute]gico b[[i]], para 1\[LessEqual]i\[LessEqual]Length[b]"

Begin["`Private`"]

arbitrary = Function[k, Module[{i, j, m, op},
    i = RandomInteger[{1, k - 2}];
    j = RandomInteger[{i + 1, k - 1}];
    m = RandomInteger[{j + 1, k}];
    op = Function[x, If[x == 0, Identity, Not]];
    First[Map[Function,
      {Apply[Or, 
        Map[Function[p, 
          op[First[p]][
           ToExpression[
            "#" <> ToString[Last[p]]]]], {{RandomInteger[], 
           i}, {RandomInteger[], j}, {RandomInteger[], m}}]]}]]
    ]];

randcnf = Function[{k, n},
   {k, Table[arbitrary[k], {n}]}
   ];

numclaus = Function[cnf, Length[Last[cnf]]];

numvars = First;

satisfazQ = 
  Function[{cnf, w}, 
   Apply[And, Map[Function[f, Apply[f, w]], Last[cnf]]]];

numsatclaus = 
  Function[{cnf, w}, 
  Length[Select[Last[cnf],Function[f, Apply[f, w]]]]];

End[]

EndPackage[]
