Plans on investigations into the minimum of the maxvardegree of parameterised classes of unsatisfiable clausesets.
More...
Go to the source code of this file.
Detailed Description
Plans on investigations into the minimum of the maxvardegree of parameterised classes of unsatisfiable clausesets.
 Todo:
 Low variabledegrees and high clauselengths

The general question considers clausesets F (boolean and also nonboolean) with minimal clauselength k and maximal variabledegree r. How low can r be so that still unsatisfiable instances are possible?

One can restrict the clausesets to uniform clausesets.

See plans in ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/plans/SmallVariableDegrees.hpp

Or one considers only hitting clausesets; see ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/plans/general.hpp.

One can also demand variable or literalregularity (see also the considerations for hitting clausesets).

Instead variable or literaldegrees one can consider the maximal degrees in the commonvariable graph or on the conflictgraph (both now are clausedegrees). See again hitting clausesets.

Instead of minimal clauselength one can consider the deficiency.

DONE This should become its own module.
 Todo:
 Unsatisfiable nonsingular hitting clausesets

Via lmin(map(max_variable_degree_cs,all_uhit_def(k))) we obtain the mininum of the maxvardegrees for a given deficiency of examples in the catalogue.

Let minmaxvd(k) be the minimum of max_variable_degree_cs(F) for all nonsingular unsatisfiable hitting clausesets of deficiency k.

The most basic question is whether minmaxvd(k) must grow with k.

We know minmaxvd(2) = 4.

We have examples showing minmaxvd(3) <= 6.

And also minmaxvd(4) <= 6.

And minmaxvd(5) <= 8.

minmaxvd(6) <= 9.

minmaxvd(7) <= 10.

minmaxvd(8) <= 11.

minmaxvd(8) <= 13.
Definition in file MinimiseMaxVarDegrees.hpp.