OKlibrary  0.2.1.6
MaxVarDegrees.hpp File Reference

Plans related to the determination of the maximal variable degrees of (typically uniform) minimally unsatisfiable clause-sets. More...

Go to the source code of this file.


Detailed Description

Plans related to the determination of the maximal variable degrees of (typically uniform) minimally unsatisfiable clause-sets.

Todo:
Minimal variable-degree of uniform minimally unsatisfiable clause-sets
  • The basic notions:
    1. We have max_variable_degree_cs.
    2. This is to be minimised for given k over all uniform minimally unsatisfiable clause-sets which are k-uniform.
    3. The function yielding precise values and bounds shall be called "maxvardegree_umu" ("umu" for "uniform minimally unsatisfiable").
    4. That is, uniformcsp(F) and min_unsat_bydef(F) and max_rank_cs(F)=k => max_variable_degree_cs(F) >= maxvardegree_umu(k).
    5. Better, maxvardegree_umu(k) should be a number, iff the precise value is known, and otherwise a pair [lower_bound, upper_bound].
    6. DONE (we speak of "maxvardegree" now) Let minvardeg_umu(k) for k >= 0 be the minimal possible (maximal) variable-degree of (minimally) unsatisfiable k-uniform boolean clause-sets F.
  • We need to implement maxvardegree_umu(k) so that it yields the currently known lower and upper bounds.
    1. We need a table with the best known values.
    2. Then there are several functions for computing upper bounds, which can be invoked for unknown k.
    3. Once we computed such an upper bound, then we might wish to store it (especially if the computation was rather expensive); how to do this?
  • We also need witnesses for the upper and lower bounds:
    1. Upper bounds are realised by single examples.
    2. See topic "Pumping up binary clauses" for a method of constructing clause-sets, which is directly connected to the NP-completeness proof.
    3. In [Hoory, Szeider, arXiv, 2004], identical with [Hoory, Szeider, SIAM Discrete Mathematics, 2006], a general construction is discussed; see todo below.
    4. See "Small variable-degrees in MUSAT(1)" in Satisfiability/Lisp/MinimalUnsatisfiability/plans/DeficiencyOne.hpp for methods, which apparently yield the strongest examples currently.
    5. Apparently the examples are rather large, so that also more compressed representations (term-based, or merely stating main parameters), are needed.
    6. For lower bounds one needs algorithms which find quickly a satisfying assignments.
    7. The lower bound k+1 (k >= 1) is realised by matching-satisfiability.
  • The restrictions to hitting clause-sets F are considered in Satisfiability/Lisp/ConflictCombinatorics/plans/HittingClauseSets.hpp.
Todo:
Pumping up binary clauses
  • See "Translations reducing the number of variable-occurrences" in ComputerAlgebra/Satisfiability/Lisp/ClauseSets/plans/Translations.hpp for the background of the general translations.
  • Let m(k) be the minimal variable-degree s for a k-uniform clause-set F_v, which forces v to be false and where v has variable-degree at most s-1. Then we have maxvardegree_umu(k) <= m(k), as follows by the satisfiability- equivalence of the general transformation (pumping up binary clauses by such a helper clause-set).
  • Perhaps m(k) is easier to determine than maxvardegree_umu(k). Or do we have maxvardegree_umu(k) = m(k) ???
  • In [Tovey, 1984, DAM] such an F_v for k=3, s=4 is given, which is implemented as "tovey84" in Satisfiability/Lisp/MinimalUnsatisfiability/MinVariableDegrees.mac
  • Due to m(3) <= 4 we get m(k) <= 2^(k-1) for all k >= 3, simply by expanding the above F_v to higher clause-length using inverse 2-subsumption resolution (using new variables each time).
Todo:
Implementing [Hoory, Szeider, SIAM Discrete Mathematics, 2006]
  • In Section 4, Definition 4.1, Lemma 4.2, rules 1,2, and the variation on page 527 top, a general (nondeterministic) construction is introduced, which we should implement.
  • Then (page 527) the two special families from Sections 2, 3 are derived; again we should implement this.
  • Let maxvardegree_umu_hs(k) be the minimal (maximal) variable-degree obtainable by this construction (in the article called "f_2(k) + 1").
  • At the end of Section 4 a simple algorithm is presented for computing maxvardegree_umu_hs(k), which we should implement.
  • Likely the formulas constructed are minimally unsatisfiable?
  • What are their parameters (deficiency, number of variables)?
  • How regular are these formulas?

Definition in file MaxVarDegrees.hpp.