Plans related to hitting clausesets.
More...
Go to the source code of this file.
Detailed Description
Plans related to hitting clausesets.
 Todo:
 Organisation

Create a new module Satisfiability/Lisp/HittingClauseSets.

Move all about hitting cls and ABDs there.

And move the uhit_def catalogue there.

See "Checking the uhit_def catalogue" in ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/Basics.mac

And then split it into several submodules.

"SplittingTrees.mac"

"RepresentingClauseSets.mac"

"Generators.mac"

"TwoSubsumption.mac"

"AssociativeBlockDesigns.mac"

"UhitCatalogue.mac"

"Search.mac" (e.g., searching for special hitting cls via SAT)
 Todo:
 Connections
 Todo:
 Allowed parameter values

A fundamental question about boolean hitting clausesets is to determine the possible parametervalues.

Of course, unsatisfiable hitting clausesets are of high interest, but likely the questions then become much more complicated; see for example todo "Nonsingular unsatisfiable hitting clausesets of given deficiency" below.

Possible parameters are:

n, c, l

the lists of variabledegrees, literaldegrees, clauseranks

minimal/maximal values for these degrees and ranks

the conflictmatrix.

The corresponding questions for intersecting hypergraphs should be simpler, and they are also basic here, since the variablehypergraphs of hitting clausesets are intersecting.

A basic example is that for a 2uniform hitting clauseset F we have n(F) <= 1/2 + (1/4 + 2 * c(F))^(1/2), since their variablehypergraphs are complete graphs.

For c(F) = 3 we obtain n(F) <= 3 (compared to n(F) <= 6 if F would be arbitrary).

This needs to be generalised to arbitrary ranks.
 Todo:
 Constructions
 Todo:
 max_var_hitting_def

Perhaps this function should be an arrayfunction.

It would also be nice, if additionally we could give a direct construction.
 Todo:
 Representations

hitting_cls_rep_st(T) represents the boolean function F underlying T in the following ways in case T involves reduction r:

In any case both representations (CNF and DNF) are satisfiability equivalent.

If r only used forced assignments, then after amendment the DNFrepresentation yields an equivalent clauseset.

This should be documented, and perhaps rsplitting trees using only forced assignments get a proper name.
 Todo:
 Decomposing clausesets into hitting clausesets

DONE Write a function which actually computes the conflictpartitionnumber of a clauseset (the smallest number of hitting subclausesets which partition the clauseset).
 Todo:
 Generators for unsatisfiable hitting clausesets

Topic "Generators" in Satisfiability/Lisp/ConflictCombinatorics/plans/AssociativeBlockDesigns.hpp is concerned with unsatisfiable hitting clausesets which are uniform and variableregular (and thus literalregular).

If on the other hand we drop (variable)regularity (so we are only considering unsatisfiable uniform hitting clausesets), what constructions are then available?

We can inspect the ABDconstructions, and see to what degree they are generic, i.e., for assumptions are actually needed and which are transferred to the result.

And what about general unsatisfiable hitting clausesets?

One could also consider regularity (variable or literalregularity) with uniformity.

In any case, the ABDconstructions need to be inspected.

We have three approaches, based on applying partial assignments, applying DPreductions, and applying 2subsumption resolution.

Questions regarding the minimal possible variable degree of uniform unsatisfiable clausesets in general are handled in Satisfiability/Lisp/MinimalUnsatisfiability/plans/SmallVariableDegrees.hpp

smusat_genhorn_cs: We need statisticsfunctions, i.e., the three functions nvar_smusat_genhorn, ncl_smusat_genhorn, ncl_list_smusat_genhorn.
 Todo:
 Generators for satisfiable hitting clausesets

sat_genhorn_cs: We need statisticsfunctions, i.e., the three functions nvar_sat_genhorn, ncl_sat_genhorn, ncl_list_sat_genhorn.
 Todo:
 derived_hitting_cs_pred_isoelim

For monitoring we should make it possible to output the information in monitor_check_dhcpfi_entry only up to a given depth in the search tree.

How to enable continuation after stopping the computation?

The current path needs to be available, so that one can continue with it.

And some given global variable mirrors always its current value.

Setting this value appropriately should also make it possible to jump around in the search tree, and visit "later" parts.

Are there heuristics for choosing the 2subsumption step and the first branch, in order to find instances earlier?

One can maximise the minvardegree, especially if one is searching for such examples (see "Maximal minvardegrees" in Satisfiability/Lisp/MinimalUnsatisfiability/plans/general.hpp.

This seems reasonably, and should also give a better chance of reaching a low deficiency.

So we should use a heuristics h(F,FP,forb_pairs), which returns [R,G,new_forb_pairs] respectively [new_forb_pairs].

Yet, as a prototype, this is hardcoded into "all_derived_hitting_cs_pred_isoelim_mvd".

Another heuristics would be to maximise the minlitdegree.

We should cleanup handling of V:

Do we assume that no variable gets eliminated, or not?

See all_derived_hitting_cs_isoelim.

We should cleanup all these different versions:

Perhaps we should have a dedicated submodule.

Generalise nearly_full_hitting_fcs:

For n and 0 <= i <= n we can find F with deficiency 2^n  n  i which attain the upper bound on the minvardegree.

i=0 is full_fcs(n), i=1 is nearly_full_hitting_fcs(n).

For i >= 2 we don't have uniqueness.

Finding all cases can be done by derived_hitting_cs_pred_isoelim.

But for getting only the sharp cases it seems necessary not to use the same variable twice.

This should also be sufficient.

So we can speed up the computation.

And then we should have a simple procedure which can find one clauseset for each i.
 Todo:
 Nonsingular unsatisfiable hitting clausesets of given deficiency

Conjecture of XSZ+OK: For fixed deficiency k, there are up to isomorphism only finitely many unsatisfiable hitting clausesets which are reduced w.r.t. singular DPreduction.

In other words, there is a function maxN(k): N > N such that check_hitting_nsing_def(F) = [k] => nvar_cs(F) <= maxN(k).

More precisely, OK+XSZ conjecture the following:

Let N(k,n) be the number of isomorphism types of "clawfree" unsatisfiable hitting clausesets with deficiency k and with n variables.

Obviously for fixed k there is a minimal n s.t. N(k,n) > 0; call this minN(k).

Let a(n) be the smallest n such that 2^n  n >= k. We have minN(k) >= a(n) (due to the completeness of 2subsumption resolution; see below).

We conjecture that for all k we have equality here.

Let maxN(k) be the supremum of n s.t. N(k,n) > 0. So the conjecture states that maxN(k) < inf for all k.

Now we conjecture that maxN(k) = 3 + (k2)*4; see max_var_hitting_def in Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac for the (simple) realising construction.

Furthermore we believe that

The set of n with N(k,n) is exactly the interval {minN(k), ..., maxN(k)}.

For k >= 2 N(k,) is first strictly increasing, and then strictly decreasing on this interval.

And N(k,maxN(k)) = 1.

In Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def.mac one finds a catalogue of clawfree unsatisfiable hitting clausesets for given deficiency.

A main tool are the functions all_unsinghitting_def(k,n) and all_unsinghitting(n), which for given k,n resp. given n determine all isomorphism types of clawfree unsatisfiable hitting clausesets.

The basis idea is that from full_fcs(n) by 2subsumption resolution we can create all hitting clausesets using at most n variables.

Once we have test cases (if the above functions take too long, one can abort the computation and use what has been found until now), then they can be checked against the catalogue via classify_candidates_uhit_def.

Another source is the application of partial assignments to an "interesting" hitting clauseset.

Experiment:
R3 : representatives_cs(map(sdp_reduction_cs,all_hittinginstances_def(brouwer1999[2],3)))$
map(nvar_cs,R3);
{3, 4, 5}
length(R3);
12
classify_candidates_uhit_def(listify(R3));
(see (see ComputerAlgebra/Satisfiability/Lisp/Symmetries/Symmetries.mac for tools for isomorphism testing). It seems that brouwer1999 is rather rich w.r.t. creating various hitting clausesets by applying partial assignments.

Possible this "richness" makes brouwer1999 so special (and hard to find)?

Another source is the application of DPreductions:

Experiment:
dp_inst_brr : all_hitting_DP_reductions_def(brouwer1999[2],3,'dp_inst_br)$
This appears to take a week, and possibly no instance is found, so this appears not to be suitable here.

See Experimentation/Investigations/plans/MaximiseMinVarDegrees.hpp for related investigations into maximising the minvardegree.
 Todo:
 all_cld_uhit_minvd

We should try to strengthen the filtering.

all_cld_uhit_minvd(6,4,9) = {{[2,2],[4,8]}}:

Here we have c = 6 + 4 = 10 = 9 + 1.

The case is impossible since due to the hitting condition the two binary clauses must overlap, but then some variables occurs only 10  2 = 8 times.

all_cld_uhit_minvd(6,5,9) = { {[1,1],[3,1],[4,3],[5,6]}, {[1,1],[3,2],[5,8]}, {[1,1],[4,6],[5,4]}, {[2,3],[5,8]} }

We have here c = 6 + 5 = 11 = 9 + 2.

In the first three cases we can apply singular DPreduction (aka unitclause elimination), reducing the case from (6,5,9) to (6,4,9), which we already know is impossible.

The remaining case {[2,3],[5,8]} is impossible:

The 2clauses must pairwise overlap, and thus there exists a variable not in any of them, which then exists 11  3 times; contradiction.

See Experimentation/Investigations/plans/MaximiseMinVarDegrees.hpp for similar examples.

Likely this function should become an arrayfunction, since due to unitclauses we have a recursion step here.

Perhaps first we only consider the case of filtering out impossible cases for all_cld_uhit_minvd.

If we are only interested in nonsingular cases, then we can drop the cases with unitclauses at all.

Likely we do not obtain a complete (efficient) rulesystem here, but we can have a collection of rules for filtering out cases.

Of course, we also obtain (general) satisfiability problems, for each clauselengthdistribution one problem.

These problems are easier since we only need to handle the hitting condition (not the unsatisfiability condition).

Compare with "Searching for ABD(n,k) (via SAT)" in Lisp/ConflictCombinatorics/plans/AssociativeBlockDesigns.hpp

First we create propagators; this is straightforward, see "Hitting clausesets" in Satisfiability/Lisp/ConstraintProblems/plans/Generators.hpp
Definition in file HittingClauseSets.hpp.