OKlibrary  0.2.1.6
MinimiseMaxVarDegrees.hpp File Reference

Plans on investigations into the minimum of the max-var-degree of parameterised classes of unsatisfiable clause-sets. More...

Go to the source code of this file.


Detailed Description

Plans on investigations into the minimum of the max-var-degree of parameterised classes of unsatisfiable clause-sets.

Todo:
Low variable-degrees and high clause-lengths
  • The general question considers clause-sets F (boolean and also non-boolean) with minimal clause-length k and maximal variable-degree r. How low can r be so that still unsatisfiable instances are possible?
  • One can restrict the clause-sets to uniform clause-sets.
  • See plans in ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/plans/SmallVariableDegrees.hpp
  • Or one considers only hitting clause-sets; see ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/plans/general.hpp.
  • One can also demand variable- or literal-regularity (see also the considerations for hitting clause-sets).
  • Instead variable- or literal-degrees one can consider the maximal degrees in the common-variable graph or on the conflict-graph (both now are clause-degrees). See again hitting clause-sets.
  • Instead of minimal clause-length one can consider the deficiency.
  • DONE This should become its own module.
Todo:
Unsatisfiable non-singular hitting clause-sets
  • Via lmin(map(max_variable_degree_cs,all_uhit_def(k))) we obtain the mininum of the max-var-degrees for a given deficiency of examples in the catalogue.
  • Let minmaxvd(k) be the minimum of max_variable_degree_cs(F) for all non-singular unsatisfiable hitting clause-sets 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.