HittingClauseSets.hpp File Reference

Plans related to hitting clause-sets. More...

Go to the source code of this file.

Detailed Description

Plans related to hitting clause-sets.

  • Create a new module Satisfiability/Lisp/HittingClauseSets.
  • Move all about hitting cls and ABDs there.
  • And move the uhit_def catalogue there.
    1. See "Checking the uhit_def catalogue" in ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/Basics.mac
  • And then split it into several sub-modules.
    1. "SplittingTrees.mac"
    2. "RepresentingClauseSets.mac"
    3. "Generators.mac"
    4. "TwoSubsumption.mac"
    5. "AssociativeBlockDesigns.mac"
    6. "UhitCatalogue.mac"
    7. "Search.mac" (e.g., searching for special hitting cls via SAT)
Allowed parameter values
  • A fundamental question about boolean hitting clause-sets is to determine the possible parameter-values.
  • Of course, unsatisfiable hitting clause-sets are of high interest, but likely the questions then become much more complicated; see for example todo "Non-singular unsatisfiable hitting clause-sets of given deficiency" below.
  • Possible parameters are:
    1. n, c, l
    2. the lists of variable-degrees, literal-degrees, clause-ranks
    3. minimal/maximal values for these degrees and ranks
    4. the conflict-matrix.
  • The corresponding questions for intersecting hypergraphs should be simpler, and they are also basic here, since the variable-hypergraphs of hitting clause-sets are intersecting.
    1. A basic example is that for a 2-uniform hitting clause-set F we have n(F) <= 1/2 + (1/4 + 2 * c(F))^(1/2), since their variable-hypergraphs are complete graphs.
    2. For c(F) = 3 we obtain n(F) <= 3 (compared to n(F) <= 6 if F would be arbitrary).
    3. This needs to be generalised to arbitrary ranks.
  • Perhaps this function should be an array-function.
  • It would also be nice, if additionally we could give a direct construction.
  • hitting_cls_rep_st(T) represents the boolean function F underlying T in the following ways in case T involves reduction r:
    1. In any case both representations (CNF and DNF) are satisfiability- equivalent.
    2. If r only used forced assignments, then after amendment the DNF-representation yields an equivalent clause-set.
  • This should be documented, and perhaps r-splitting trees using only forced assignments get a proper name.
Decomposing clause-sets into hitting clause-sets
  • DONE Write a function which actually computes the conflict-partition-number of a clause-set (the smallest number of hitting sub-clause-sets which partition the clause-set).
Generators for unsatisfiable hitting clause-sets
  • Topic "Generators" in Satisfiability/Lisp/ConflictCombinatorics/plans/AssociativeBlockDesigns.hpp is concerned with unsatisfiable hitting clause-sets which are uniform and variable-regular (and thus literal-regular).
  • If on the other hand we drop (variable-)regularity (so we are only considering unsatisfiable uniform hitting clause-sets), what constructions are then available?
    1. We can inspect the ABD-constructions, 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 clause-sets?
    1. One could also consider regularity (variable- or literal-regularity) with uniformity.
    2. In any case, the ABD-constructions need to be inspected.
    3. We have three approaches, based on applying partial assignments, applying DP-reductions, and applying 2-subsumption resolution.
  • Questions regarding the minimal possible variable degree of uniform unsatisfiable clause-sets in general are handled in Satisfiability/Lisp/MinimalUnsatisfiability/plans/SmallVariableDegrees.hpp
  • smusat_genhorn_cs: We need statistics-functions, i.e., the three functions nvar_smusat_genhorn, ncl_smusat_genhorn, ncl_list_smusat_genhorn.
Generators for satisfiable hitting clause-sets
  • sat_genhorn_cs: We need statistics-functions, i.e., the three functions nvar_sat_genhorn, ncl_sat_genhorn, ncl_list_sat_genhorn.
  • 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?
    1. The current path needs to be available, so that one can continue with it.
    2. And some given global variable mirrors always its current value.
    3. 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 2-subsumption step and the first branch, in order to find instances earlier?
    1. One can maximise the min-var-degree, especially if one is searching for such examples (see "Maximal min-var-degrees" in Satisfiability/Lisp/MinimalUnsatisfiability/plans/general.hpp.
    2. This seems reasonably, and should also give a better chance of reaching a low deficiency.
    3. So we should use a heuristics h(F,FP,forb_pairs), which returns [R,G,new_forb_pairs] respectively [new_forb_pairs].
    4. Yet, as a prototype, this is hardcoded into "all_derived_hitting_cs_pred_isoelim_mvd".
    5. Another heuristics would be to maximise the min-lit-degree.
  • We should clean-up handling of V:
    1. Do we assume that no variable gets eliminated, or not?
    2. See all_derived_hitting_cs_isoelim.
  • We should clean-up all these different versions:
    1. Perhaps we should have a dedicated sub-module.
  • Generalise nearly_full_hitting_fcs:
    1. For n and 0 <= i <= n we can find F with deficiency 2^n - n - i which attain the upper bound on the min-var-degree.
    2. i=0 is full_fcs(n), i=1 is nearly_full_hitting_fcs(n).
    3. For i >= 2 we don't have uniqueness.
    4. 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.
    5. And then we should have a simple procedure which can find one clause-set for each i.
Non-singular unsatisfiable hitting clause-sets of given deficiency
  • Conjecture of XSZ+OK: For fixed deficiency k, there are up to isomorphism only finitely many unsatisfiable hitting clause-sets which are reduced w.r.t. singular DP-reduction.
  • 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:
    1. Let N(k,n) be the number of isomorphism types of "claw-free" unsatisfiable hitting clause-sets with deficiency k and with n variables.
    2. Obviously for fixed k there is a minimal n s.t. N(k,n) > 0; call this minN(k).
    3. Let a(n) be the smallest n such that 2^n - n >= k. We have minN(k) >= a(n) (due to the completeness of 2-subsumption resolution; see below).
    4. We conjecture that for all k we have equality here.
    5. 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.
    6. Now we conjecture that maxN(k) = 3 + (k-2)*4; see max_var_hitting_def in Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac for the (simple) realising construction.
    7. 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 claw-free unsatisfiable hitting clause-sets for given deficiency.
    1. 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 claw-free unsatisfiable hitting clause-sets.
    2. The basis idea is that from full_fcs(n) by 2-subsumption resolution we can create all hitting clause-sets using at most n variables.
    3. 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.
    4. Another source is the application of partial assignments to an "interesting" hitting clause-set.
      • Experiment:
        R3 : representatives_cs(map(sdp_reduction_cs,all_hittinginstances_def(brouwer1999[2],3)))$
          {3, 4, 5}
        (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 clause-sets by applying partial assignments.
      • Possible this "richness" makes brouwer1999 so special (and hard to find)?
    5. Another source is the application of DP-reductions:
      • 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 min-var-degree.
  • We should try to strengthen the filtering.
    • all_cld_uhit_minvd(6,4,9) = {{[2,2],[4,8]}}:
      1. Here we have c = 6 + 4 = 10 = 9 + 1.
      2. 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]} }
      1. We have here c = 6 + 5 = 11 = 9 + 2.
      2. In the first three cases we can apply singular DP-reduction (aka unit-clause elimination), reducing the case from (6,5,9) to (6,4,9), which we already know is impossible.
      3. The remaining case {[2,3],[5,8]} is impossible:
        • The 2-clauses 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 array-function, since due to unit-clauses we have a recursion step here.
    1. Perhaps first we only consider the case of filtering out impossible cases for all_cld_uhit_minvd.
    2. If we are only interested in non-singular cases, then we can drop the cases with unit-clauses at all.
  • Likely we do not obtain a complete (efficient) rule-system here, but we can have a collection of rules for filtering out cases.
  • Of course, we also obtain (general) satisfiability problems, for each clause-length-distribution one problem.
    1. These problems are easier since we only need to handle the hitting condition (not the unsatisfiability condition).
    2. Compare with "Searching for ABD(n,k) (via SAT)" in Lisp/ConflictCombinatorics/plans/AssociativeBlockDesigns.hpp
    3. First we create propagators; this is straight-forward, see "Hitting clause-sets" in Satisfiability/Lisp/ConstraintProblems/plans/Generators.hpp

Definition in file HittingClauseSets.hpp.