Plans related to the determination of the maximal variable degrees of (typically uniform) minimally unsatisfiable clausesets.
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 clausesets.
 Todo:
 Minimal variabledegree of uniform minimally unsatisfiable clausesets

The basic notions:

We have max_variable_degree_cs.

This is to be minimised for given k over all uniform minimally unsatisfiable clausesets which are kuniform.

The function yielding precise values and bounds shall be called "maxvardegree_umu" ("umu" for "uniform minimally unsatisfiable").

That is, uniformcsp(F) and min_unsat_bydef(F) and max_rank_cs(F)=k => max_variable_degree_cs(F) >= maxvardegree_umu(k).

Better, maxvardegree_umu(k) should be a number, iff the precise value is known, and otherwise a pair [lower_bound, upper_bound].

DONE (we speak of "maxvardegree" now) Let minvardeg_umu(k) for k >= 0 be the minimal possible (maximal) variabledegree of (minimally) unsatisfiable kuniform boolean clausesets F.

We need to implement maxvardegree_umu(k) so that it yields the currently known lower and upper bounds.

We need a table with the best known values.

Then there are several functions for computing upper bounds, which can be invoked for unknown k.

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:

Upper bounds are realised by single examples.

See topic "Pumping up binary clauses" for a method of constructing clausesets, which is directly connected to the NPcompleteness proof.

In [Hoory, Szeider, arXiv, 2004], identical with [Hoory, Szeider, SIAM Discrete Mathematics, 2006], a general construction is discussed; see todo below.

See "Small variabledegrees in MUSAT(1)" in Satisfiability/Lisp/MinimalUnsatisfiability/plans/DeficiencyOne.hpp for methods, which apparently yield the strongest examples currently.

Apparently the examples are rather large, so that also more compressed representations (termbased, or merely stating main parameters), are needed.

For lower bounds one needs algorithms which find quickly a satisfying assignments.

The lower bound k+1 (k >= 1) is realised by matchingsatisfiability.

The restrictions to hitting clausesets F are considered in Satisfiability/Lisp/ConflictCombinatorics/plans/HittingClauseSets.hpp.
 Todo:
 Pumping up binary clauses

See "Translations reducing the number of variableoccurrences" in ComputerAlgebra/Satisfiability/Lisp/ClauseSets/plans/Translations.hpp for the background of the general translations.

Let m(k) be the minimal variabledegree s for a kuniform clauseset F_v, which forces v to be false and where v has variabledegree at most s1. 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 clauseset).

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^(k1) for all k >= 3, simply by expanding the above F_v to higher clauselength using inverse 2subsumption 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) variabledegree 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.