uhit_def.hpp File Reference

Plans regarding the catalogue of unsatisfiable non-singular hitting clause-sets. More...

Go to the source code of this file.

Detailed Description

Plans regarding the catalogue of unsatisfiable non-singular hitting clause-sets.

Shall uhit_def be redefined with every loading?
Problems with evaluation
  • If at the time of a definition of an uhit_def-value 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 function-definition is now available).
  • Is this a Maxima-bug? 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_def-catalogue unevaluated, and evaluation only happens when needed.
  • However it seems hard to control: for example in Satisfiability/Lisp/ConflictCombinatorics/testobjects/HittingClauseSets.mac an extra load-command 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.
  • Rename this file to Uhit_def.hpp, and move data/uhit_def.hpp to MinimalUnsatisfiabilility/Uhit_def.hpp.
  • Loading the data-set takes too long:
    1. Some form of oklib_include is needed, which by default is off, and is turned on by some switch.
    2. See "File load and include" in ComputerAlgebra/plans/Maxima.hpp.
    3. Also the tests then need to be activated resp. deactivated. So perhaps the catalogue needs to contain data about activation status.
Connections to other modules
  • Write tests for all functions.
    1. uhit_def : DONE
    2. uhit_n_data : started
    3. uhit_n : started
    4. apply_uhit
    5. collect_uhit_n
    6. classify_candidates_uhit_def
    7. isotype_uhit_def
    8. closure_uhit_def_pass
  • Testing functions which evaluate uhit_def:
    1. Create mock-variations of uhit_def using dynamic binding.
    2. Perhaps we create a list of such mock-variations.
  • DONE At level basic, the test for uhit_def takes too long.
  • We would like to be able to use "uhit_def[k]" for the list or set of all clause-sets of deficiency k in the catalogue.
  • Yet we have all_uhit_def(k).
  • Such accessors need to be rationalised; compare todo "uhit_n" below.
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.
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 clause-sets whose min-var-degree is better than anything in the catalogue.
  • One needs also to combine analyse_isorepo_defset_mvd and analyse_isorepo_defset_imprmvd.
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:
    1. Since we are investigating the maximal min-var-degree for a given deficiency (see "Maximal min-var-degrees" in ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/plans/general.hpp), examples where the bound is attained are interesting.
    2. Also of interest are ABDs.
    3. And examples for minimal and maximal n.
  • We should provide a mechanism for lazy evaluation.
    1. Entries like max_var_hitting_def(58)[2] are just too big to compute every time with oklib_load.
    2. We could just store the terms, and by some function then trigger the evaluation.
    3. Ask on the Maxima mailing list about "lazy evaluation".
ExternalSources for larger data-sets
  • Larger data-sets should be made available as uhit_def*.mac data-sets under ExternalSources, loadable on demand.
    1. These files, as ".tar.bz2"-files, are to be found under ExternalSources/data.
    2. What ending for these files? They are created by save, so apparently ".lisp" is appropriate?
    3. It is the responsibility of the user to unpack these packages.
    4. The path to the directory is known to our Maxima-system.
    5. Perhaps we provide some special load-functions.
    6. 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.
    1. For n=5 add at least deficiencies delta = 4,5.
    2. For n=6 add at least deficiencies delta = 5,6,7.
    3. For n=7 add at least deficiencies delta = 5,6,7.
    4. For n=8 add at least deficiencies delta = 5,6,7.
  • We should integrate the catalogue of MU(k) isomorphism types from http://wwwcs.uni-paderborn.de/cs/ag-klbue/de/research/MinUnsat/index.html .
Reduction by 2-subsumption resolution
  • A second catalogue should be created, which contains only those unsatisfiable hitting clause-sets for which no 2-subsumption 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 non-singularity). Call it uhit_def_nsn2s.
    1. Via
      we obtain the current examples.
    2. We should get much smaller numbers.
  • And also the bigger catalogue uhit_def_n2s, where non-singularity is dropped, is of interest.
    1. The question is whether for given deficiency there are only finitely many cases in uhit_def_n2s?!
    2. From this catalogue all of uhit_def can be created by inverse 2-subsumption resolution.
    3. A representation involves an element F of uhit_def_n2s, a clause-list, and then a partial map from clause-indices to variable-sets, where the latter specify the expansion.
    4. The process of reduction by 2-subsumption-resolution is not confluent, and for a given (non-singular) hitting clause-set F there can exist 2 non-isomorphic hitting clause-sets reduces w.r.t. 2-subsumption-resolution which can be expanded to F.
      1. Obvious examples are given by reducing full_fcs(n).
      2. For full_fcs(n) there exist many representations, the optimal representing full_fcs(n) as the expansion of {{}} by setn(n).
      3. One could use shortest representations.

Definition in file uhit_def.hpp.