OKlibrary  0.2.1.6
MinVarDegrees.hpp File Reference

Plans regarding the minimal variable-degree of minimally unsatisfiable clause-sets. More...

Go to the source code of this file.


Detailed Description

Plans regarding the minimal variable-degree of minimally unsatisfiable clause-sets.

  • We consider upper bounds (functions nonmersenne in various forms, and strengthenings).
  • We consider lower bounds (like Sma_S2 in various forms).
  • And we provide examples showing that the upper bounds are sharp (or not).
  • Besides the maximal min-var-degree for minimally unsatisfiabible clause-sets of fixed deficiency or sub-classess, we consider related notions like the maximal number of full-clauses (for the classes).
Todo:
Organisation
  • The functions should go to a dedicated file:
    1. Perhaps we should have a submodule MaxVarDegrees.
    2. With files FullClauses.mac, Degrees.mac, NonMersenne.mac.
    3. And perhaps the functionality related to the min-var-degree in ConflictCombinatorics/HittingClauseSets.mac should be moved there, yielding a file HittingClauseSets.mac.
    4. DONE (renamed to MaxVarDegrees.hpp/mac) There is confusion with MinimalUnsatisfiability/plans/SmallVariableDegrees.hpp.
  • See Experimentation/Investigations/plans/MaximiseMinVarDegrees.hpp for the general investigation.
  • Perhaps the considerations regarding hitting clause-sets should go to a module regarding hitting clause-sets ?
    1. The conjecture is that the maximal min-var-degree for a fixed deficiency is the same for all of MU and for the subsets of (unsatisfiable) hitting clause-sets.
    2. See "derived_hitting_cs_pred_isoelim" in ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/plans/HittingClauseSets.hpp for how to find examples.
    3. However we already have the uhit_def-catalogue here.
    4. Above we actually propose to move the functionality from ConflictCombinatorics here (that is, to a submodule).
  • Naming of bounds-functions:
    1. We have fullclauses_dmu and minvardegree_dmu (for all of MU).
    2. In ConflictCombinatorics/HittingClauseSets.mac we have the function max_min_var_deg_uhit_def, which considers just the uhit_def-catalogue.
    3. Perhaps this function should be renamed to minvardegree_uhit_def.
    4. And we should introduce a bounds-function minvardegree_duhit.

Definition in file MinVarDegrees.hpp.