Plans regarding the catalogue of unsatisfiable nonsingular hitting clausesets.
More...
Go to the source code of this file.
Detailed Description
Plans regarding the catalogue of unsatisfiable nonsingular hitting clausesets.
 Todo:
 Shall uhit_def be redefined with every loading?
 Todo:
 Problems with evaluation

If at the time of a definition of an uhit_defvalue via an expression, a function in that expression is not yet defined, only later, then when calling e.g. all_uhit_def(k) that expression is not evaluated (even though the functiondefinition is now available).

Is this a Maximabug? I (OK) haven't encountered such behaviour before.

A solution is to use ev(all_uhit_def(k),eval).

Applied with apply_uhit and max_min_var_deg_uhit_def, max_min_var_deg_uhit_def_mem.

Potentially this behaviour could be useful, since one could leave terms in the uhit_defcatalogue unevaluated, and evaluation only happens when needed.

However it seems hard to control: for example in Satisfiability/Lisp/ConflictCombinatorics/testobjects/HittingClauseSets.mac an extra loadcommand had to be inserted to make the test run!

An example session:
(%i1) a[0]:f(0);
(%o1) f(0)
(%i2) f(x):= x+77;
(%o2) f(x):=77+x
(%i3) is(a[0] > 0);
(%o3) unknown
(%i4) is(ev(a[0]) > 0);
(%o4) true
This seems strange behaviour (same for 5.23.2 and 5.24.0). This does not depend on arrays: (%i1) a:f(0);
(%o1) f(0)
(%i2) f(x):= x+77;
(%o2) f(x):=77+x
(%i3) is(a > 0);
(%o3) unknown
(%i4) is(ev(a) > 0);
(%o4) true
(%i5) is(a > 0);
(%o5) unknown
(%i6) a:ev(a);
(%o6) 77
(%i7) is(a > 0);
(%o7) true

Another problem is that some functions used to define members of uhit_def are only partially given; see for example Lisp/MinimalUnsatisfiability/Deficiency2.mac and Lisp/ConflictCombinatorics/HittingClauseSets.mac.
 Todo:
 Organisation

Rename this file to Uhit_def.hpp, and move data/uhit_def.hpp to MinimalUnsatisfiabilility/Uhit_def.hpp.

Loading the dataset takes too long:

Some form of oklib_include is needed, which by default is off, and is turned on by some switch.

See "File load and include" in ComputerAlgebra/plans/Maxima.hpp.

Also the tests then need to be activated resp. deactivated. So perhaps the catalogue needs to contain data about activation status.
 Todo:
 Connections to other modules
 Todo:
 Tests

Write tests for all functions.

uhit_def : DONE

uhit_n_data : started

uhit_n : started

apply_uhit

collect_uhit_n

classify_candidates_uhit_def

isotype_uhit_def

closure_uhit_def_pass

Testing functions which evaluate uhit_def:

Create mockvariations of uhit_def using dynamic binding.

Perhaps we create a list of such mockvariations.

DONE At level basic, the test for uhit_def takes too long.
 Todo:
 uhit_def

We would like to be able to use "uhit_def[k]" for the list or set of all clausesets of deficiency k in the catalogue.

Yet we have all_uhit_def(k).

Such accessors need to be rationalised; compare todo "uhit_n" below.
 Todo:
 uhit_n : DONE

DONE info_data should be computed.

DONE def_data should be computed.

DONE Run through all deficiencies in uhit_def and check whether the given n is contained.

DONE To determine whether the classification is complete, use two functions which compute lower and upper bounds on possible deficiencies for a given n, and then check whether for all these deficiencies the corresponding entries are complete.
 Todo:
 Evaluating the catalogue

DONE (analyse_isorepo_defset_imprmvd) Similar to analyse_isorepo_defset_mvd we need a function, which runs through a repository and keeps those clausesets whose minvardegree is better than anything in the catalogue.

One needs also to combine analyse_isorepo_defset_mvd and analyse_isorepo_defset_imprmvd.
 Todo:
 New entries

For n=5 add deficiencies delta = 14, ..., 27.

It seems unlikely that we can get all for n=5. Nevertheless we should get a good variety, and for that we need a version of all_unsinghitting which starts from a different (random) path.

The general policy about new entries should be that in case there is a large number of entries, and so we cannot have them all, then we should enter "interesting" examples:

Since we are investigating the maximal minvardegree for a given deficiency (see "Maximal minvardegrees" in ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/plans/general.hpp), examples where the bound is attained are interesting.

Also of interest are ABDs.

And examples for minimal and maximal n.

We should provide a mechanism for lazy evaluation.

Entries like max_var_hitting_def(58)[2] are just too big to compute every time with oklib_load.

We could just store the terms, and by some function then trigger the evaluation.

Ask on the Maxima mailing list about "lazy evaluation".
 Todo:
 ExternalSources for larger datasets

Larger datasets should be made available as uhit_def*.mac datasets under ExternalSources, loadable on demand.

These files, as ".tar.bz2"files, are to be found under ExternalSources/data.

What ending for these files? They are created by save, so apparently ".lisp" is appropriate?

It is the responsibility of the user to unpack these packages.

The path to the directory is known to our Maximasystem.

Perhaps we provide some special loadfunctions.

Single data sets can be specified, and also all of them.

Which data is already provided in uhit_def.mac ?

Process n=5,6,7,8.

For n=5 add at least deficiencies delta = 4,5.

For n=6 add at least deficiencies delta = 5,6,7.

For n=7 add at least deficiencies delta = 5,6,7.

For n=8 add at least deficiencies delta = 5,6,7.

We should integrate the catalogue of MU(k) isomorphism types from http://wwwcs.unipaderborn.de/cs/agklbue/de/research/MinUnsat/index.html .
 Todo:
 Reduction by 2subsumption resolution

A second catalogue should be created, which contains only those unsatisfiable hitting clausesets for which no 2subsumption resolution is possible.

The structure of this catalogue is the same as of uhit_def.

The subset of uhit_def is of interest (here we are also asking for nonsingularity). Call it uhit_def_nsn2s.

Via
sublist(apply_uhit(lambda([k,n,i,F],[k,n,i,redtsrp(F)])),lambda([T],T[4]));
we obtain the current examples.

We should get much smaller numbers.

And also the bigger catalogue uhit_def_n2s, where nonsingularity is dropped, is of interest.

The question is whether for given deficiency there are only finitely many cases in uhit_def_n2s?!

From this catalogue all of uhit_def can be created by inverse 2subsumption resolution.

A representation involves an element F of uhit_def_n2s, a clauselist, and then a partial map from clauseindices to variablesets, where the latter specify the expansion.

The process of reduction by 2subsumptionresolution is not confluent, and for a given (nonsingular) hitting clauseset F there can exist 2 nonisomorphic hitting clausesets reduces w.r.t. 2subsumptionresolution which can be expanded to F.

Obvious examples are given by reducing full_fcs(n).

For full_fcs(n) there exist many representations, the optimal representing full_fcs(n) as the expansion of {{}} by setn(n).

One could use shortest representations.
Definition in file uhit_def.hpp.