OKlibrary  0.2.1.6
InverseSingularDP.hpp File Reference

Plans on transforming clause-sets by applying inverse singular DP-reduction. More...

Go to the source code of this file.


Detailed Description

Plans on transforming clause-sets by applying inverse singular DP-reduction.

Todo:
Transfer from Orthogonal.mup
Todo:
More intelligent iteration
  • Compare "Randomised extensions" below.
  • The function it_si_inverse_singulardp_fcs is very simple, and perhaps we can provide more intelligent functionality.
  • The problem is that the parameters p,q,a,b (where "a" now generalises the old variable "nonempty") are fixed in this approach.
  • "Typically", at the beginning only very low values of a are possible (if b > 1).
  • So perhaps a kind of gradient is introduced.
  • Or we try to fullfil the given values of a, b (while p,q are fixed), and if not possible, then we look at the "best" approximation.
  • Different strategies for such a "best approximation" are possible, lowering b, lowering a, or both.
Todo:
Creation of random subsets:
  • Looks as if random_sublist, random_subset_si should go to the submodule on set-systems (or hypergraphs?).
  • random_subset_si is very inefficient:
    1. If the number of s-subsets is large, then the dual approach can be (much) more efficient, searching through all i-subsets of literals which have a common occurrence and checking whether there are actually s such common occurrences.
Todo:
We want three types of extensions:
  • DONE (arbitrary p,q-values) The non-degenerated extensions, characteristic for singular DP-reductions on MU.
  • The saturated extensions, characteristic for singular DP-reductions on SMU.
    1. The condition is that, additionally to p=q=1, for the main clause, given by I in the implementation, there is no other clause, not involved in the extension, such that I subsumes this clause (one could then add -v to this clause).
    2. First we just implement this condition, via "basic_inverse_saturated_singulardp_fcs(FF,G)", and return false if the condition is not fulfilled.
  • The hitting extensions, characteristic for singular DP-reductions on UHIT.
    1. These are special saturated extensions.
    2. The additional criterion is that the intersection must clash with all old clauses except of the choosen one.
    3. Here we have special problems with the control, since in most cases such an extension won't be possible.
Todo:
All isomorphism types of extensions
  • We should have systematic versions, which try to generate all isomorphism types for a given number of steps.
  • Just one step:
    1. All MU-extensions are given by
      • all non-empty sub-clause-sets
      • for the main clause all possibilities between empty and "saturated"
      • then for each side clause as possibilities between the needed literals and all.
    2. The isomorphism types are obtained by removing all isomorphic cases.
    3. All SMU-extensions are given by all non-empty sub-clause-sets which full the additional condition, that their intersection does not subsume any other clause.
    4. All UHIT-extensions are given by those SMU-extensions which full the condition that their intersection clashes with all other clauses.
  • Having all MU-, SMU or UHIT-extensions, one can then choose a random extension, w.r.t. all extensions or all isomorphism types.
  • W.r.t. MU-extensions, this seems infeasible, but there should be substantiallly less SMU- and UHIT-extensions, so that here it should be interesting to choose a random SMU-extension resp. a random UHIT-extension (either treating all extensions equally likely, or treating all isomorphism types as equally likely).
  • Are there more intelligent algorithms to compute all SMU or all UHIT extensions?
    1. For a bit more than ten clauses the simple enumeration should be alright.
    2. We should reduce the problem of finding suitable types of extensions to other problems (of course, SAT, etc.).
    3. Especially UHIT-extensions should be interesting.
      • There is always one, introducing a unit-clause, but the rest might not exist.
      • One should first compute the conflict matrix.
      • Then the common neighbours yield first approximations of what is possible.
    4. One could also investigate fixed parameter tractability.
Todo:
Randomised extensions
  • Compare todo "More intelligent iteration" above.
  • Attractive is, as discussed in todo "All types of extensions", to choose amongst all possible extensions.
  • The two basic problems are
    1. a random extension in one step
    2. the repetition of this process.
    If parameter for a single random extension are involved, then in the course of the iteration these parameters might evolve.
  • For MU-extensions likely to choose amongst all possibilities is infeasible, and thus one needs to introduce parameters.

    1. p, q as we have it.
    2. For the size b of the sub-clause-set one can choose any probability distribution.
    3. Given the size, we choose a random such subset.
    4. And for "a" we choose another probability distribution.
    5. The problem then is that a,b might be inconsistent.
    6. It would be easier to first choose b, then determine the intersection and let a be the size of the intersection.
    7. Then however in many cases the intersection might be empty or very small.

    </ul?

    Todo:
    Investigations
    • The first questions concern the characterisation of MU(delta=2), SMU(delta=2) and UHIT(delta=2) (always looking at all clause-sets, not just the non-singular one).
    • For the two non-singular elements of UHIT(delta=2) we should try to obtain all isomorphism types of extensions for a number of steps.
    • Then we can try to guess the isomorphism types of all of UHIT(delta=2).
      1. The simplest guess is a triple (t,a,b), where t in {2,3} is the major isomorphism type (whether reduction yields musatd2_fcs(2) or musatd2_fcs(3)), where a is the number of variables of degree >= 3, and where b is the number of variables of degree 2.
      2. We need a catalogue where the known examples are entered.
      3. This catalogue could contain lists of known isomorphism types for each (t,a,b).
    • We know them already if the min-var-degreee is at least 3. Here we should write generators.

Definition in file InverseSingularDP.hpp.