Plans regarding the minimal variabledegree of minimally unsatisfiable clausesets.
More...
Go to the source code of this file.
Detailed Description
Plans regarding the minimal variabledegree of minimally unsatisfiable clausesets.

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 minvardegree for minimally unsatisfiabible clausesets of fixed deficiency or subclassess, we consider related notions like the maximal number of fullclauses (for the classes).
 Todo:
 Organisation

The functions should go to a dedicated file:

Perhaps we should have a submodule MaxVarDegrees.

With files FullClauses.mac, Degrees.mac, NonMersenne.mac.

And perhaps the functionality related to the minvardegree in ConflictCombinatorics/HittingClauseSets.mac should be moved there, yielding a file HittingClauseSets.mac.

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 clausesets should go to a module regarding hitting clausesets ?

The conjecture is that the maximal minvardegree for a fixed deficiency is the same for all of MU and for the subsets of (unsatisfiable) hitting clausesets.

See "derived_hitting_cs_pred_isoelim" in ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/plans/HittingClauseSets.hpp for how to find examples.

However we already have the uhit_defcatalogue here.

Above we actually propose to move the functionality from ConflictCombinatorics here (that is, to a submodule).

Naming of boundsfunctions:

We have fullclauses_dmu and minvardegree_dmu (for all of MU).

In ConflictCombinatorics/HittingClauseSets.mac we have the function max_min_var_deg_uhit_def, which considers just the uhit_defcatalogue.

Perhaps this function should be renamed to minvardegree_uhit_def.

And we should introduce a boundsfunction minvardegree_duhit.
Definition in file MinVarDegrees.hpp.