OKlibrary  0.2.1.6
Hardness.mac File Reference

Functions related to the hardness of clause-sets. More...

Go to the source code of this file.


Detailed Description

Functions related to the hardness of clause-sets.

XXX this introduction needs to be updated XXX

The hardness of a clause-set 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.