OKlibrary
0.2.1.6

Functions related to the hardness of clausesets. More...
Go to the source code of this file.
Functions related to the hardness of clausesets.
XXX this introduction needs to be updated XXX
The hardness of a clauseset F is the minimum k >= 0 such that all clauses C which follow from F can be detected via r_k.
That is, the minimum k >= 0 for which for all clauses C with F = C we have generalised_ucp(apply_pa(comp_sl(C),F),k) = {{}}.
See "Hardness of boolean function representations" in Experimentation/Investigations/BooleanFunctions/plans/general.hpp.
Use by
oklib_load("OKlib/ComputerAlgebra/Satisfiability/Lisp/Reductions/Hardness.mac");
Definition in file Hardness.mac.