Plans on transforming clausesets by applying inverse singular DPreduction.
More...
Go to the source code of this file.
Detailed Description
Plans on transforming clausesets by applying inverse singular DPreduction.
 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 setsystems (or hypergraphs?).

random_subset_si is very inefficient:

If the number of ssubsets is large, then the dual approach can be (much) more efficient, searching through all isubsets 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,qvalues) The nondegenerated extensions, characteristic for singular DPreductions on MU.

The saturated extensions, characteristic for singular DPreductions on SMU.

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).

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 DPreductions on UHIT.

These are special saturated extensions.

The additional criterion is that the intersection must clash with all old clauses except of the choosen one.

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:

All MUextensions are given by

all nonempty subclausesets

for the main clause all possibilities between empty and "saturated"

then for each side clause as possibilities between the needed literals and all.

The isomorphism types are obtained by removing all isomorphic cases.

All SMUextensions are given by all nonempty subclausesets which full the additional condition, that their intersection does not subsume any other clause.

All UHITextensions are given by those SMUextensions which full the condition that their intersection clashes with all other clauses.

Having all MU, SMU or UHITextensions, one can then choose a random extension, w.r.t. all extensions or all isomorphism types.

W.r.t. MUextensions, this seems infeasible, but there should be substantiallly less SMU and UHITextensions, so that here it should be interesting to choose a random SMUextension resp. a random UHITextension (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?

For a bit more than ten clauses the simple enumeration should be alright.

We should reduce the problem of finding suitable types of extensions to other problems (of course, SAT, etc.).

Especially UHITextensions should be interesting.

There is always one, introducing a unitclause, but the rest might not exist.

One should first compute the conflict matrix.

Then the common neighbours yield first approximations of what is possible.

One could also investigate fixed parameter tractability.
 Todo:
 Randomised extensions
Definition in file InverseSingularDP.hpp.