OKlibrary  0.2.1.6
DeficiencyOne.hpp File Reference

Plans regarding minimally unsatisfiable clause-sets of deficiency 1. More...

Go to the source code of this file.


Detailed Description

Plans regarding minimally unsatisfiable clause-sets of deficiency 1.

Todo:
Decision algorithms
  • The two basic decision algorithms for MU(1), by singular DP-reduction or by finding accumulation variables, need to be implemented.
  • Using DP-reduction:
    1. Via sdp_reduction_cs(F) we can reduce the clause-set w.r.t. singular DP-reduction.
    2. The case of degeneration which can happen by sdp_reduction_cs(F) is blocking (i.e., tautological clauses would be produced).
    3. Perhaps it is actually enough to only test whether at the beginning and the end the deficiency is 1, since a case of degeneration will (permanently) lower the deficiency?
    4. But due to blocking more variables could vanish (in clauses which get "lost"), and then the deficiency can also increase.
    5. See "Singular DP-reduction" in Satisfiability/Lisp/Reductions/plans/DP-Reductions.hpp.
  • They also extract a tree representation (see "Tree representations" below).
  • Also for the special cases "saturated" and "marginal" we need decision algorithms.
    1. This can be done by checking each DP-step.
    2. Alternatively, the input can be checked whether it is hitting resp. whether every variable has 1-1-occurrence.
Todo:
Tree representations
  • First task is, given F in MU(1), find some (the first, a random, or all) tree representation of F.
  • The algorithm:
    1. Find a variable v with degree 2.
    2. Find its two occurrences C,D.
    3. Replace C,D in F by their resolvent R, obtaining F'.
    4. Apply the algorithm recursively to F', obtain T'.
    5. In T', replace the leaf labelled with R by a new binary branching on v, with new leaves C,D.
  • Canonicity issues:
    1. Most natural seems to be an ofcs input FF.
    2. The task then is to find the first variable with degree 2, "first" w.r.t. the order given by FF.
    3. For that, we need min_variable_degree_v_ofcs, which returns the first variable with minimal degree.
    4. This can be achieved by first setting the variables in the given order to 0 in the hash-map.
  • A basic question is whether tree representations are unique up to rooted-tree-isomorphism?
    1. The most natural point of view seems not to distinguish between left and right children.
    2. If we do distinguish them (so the trees are what is called "left-right-trees"), then we only consider var-isomorphisms.
Todo:
Pebbling contradictions
  • Consider a directed acyclic graph G, where the set of source vertices is S, and where G has exactly one sink z. Then we get a clause-set in MU(1) by considering the vertices of G as variables, taking all vertices as S as positive unit-clause, for all other vertices v Horn clauses of the form "conjunction of predecessors implies v", plus additionally {-z}.
  • In this way we represent some Horn clause-sets in MU(1). Get we also all Horn claus-sets? It seems not, since apparently smusat_horn_cs(k) can't be obtained in this way. Definitely we always have at least one positive and one negative unit-clause.
  • The general question arises here about the characterisation of all Horn clause-sets in MU(1).
Todo:
Small variable-degrees in MU(1)
  • Motivated by [Hoory, Szeider, TCS 2005] we consider the following decision problem:
    • Input a clause-set F and natural number k, r.
    • It is also assumed that F does not contain pure literals, and and every clause has length at least k.
    • Decide whether it is possible by removal of literal occurrences, one by one, without ever producing a pure literal and such that the minimal clause-length is at least k, to obtain a maximal variable-degree of at most r.
    • The interesting case here is F in SMU(1), where it is guaranteed that the literal-removal-process will never contract clauses (since every clause contains a literal occurring only once).
    • But this procedure is also relevant in general, since the resulting clause-set is always an unsatisfiable clause-set with parameters (k,r) in the typical setting here (i.e., minimal rank >= k, maximal variable-degree <= r).
  • Let's call it "REMLITOCC".
  • The problem is in NP, one likely also NP-complete (also for inputs from SMU(1)).
  • The general question is to find out for given uniform clause-length k what is the smallest possible variable-degree r = f(k)+1 which still allows unsatisfiable F, where in this todo we consider F in MU(1).
  • See ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/SmallVariableDegrees.hpp for the general case F in MU (where f+1 is called "minvardeg_umu").
  • Back to MU(1), i.e., for f only F in MU(1) are considered, and we use f_1 to emphasise this:
    1. Apparently f_1(3)+1 = 4 and f_1(4)+1 = 5 are the only known precise values.
    2. Interesting also the (minimal) clause-numbers for realising the minimal parameter values (since the deficiency is fixed, this is the same as minimising the number of variables used).
    3. [Dubois, DAM 1990] realises (k=3,r=4) with 22 clauses, (k=4,r=6) with 209 clauses, and (k=5,r=11) with 3986 clauses.
    4. [Hoory, Szeider] realise (k=4,r=5) (optimal) and (k=5,r=7), and other values, but one has to investigate the underlying clause-sets (which are not discussed there explicitely).
    5. We should exhibit such examples.
    6. We should implement [Hoory, Szeider]; perhaps also [Dubois, DAM 1990] contains some constructions.
    7. As a name for "f_1+1" perhaps we use "minvardeg_umu_d1".
  • A translation into SAT of course is of interest, directly into CNF, or using active clauses (etc.).
  • There is an obvious greedy algorithm: see below.
Todo:
The heuristical function remlitocc_greedy
  • The procedure needs to be randomised.
  • Just to find an example for (k=3,r=5) from uniform_usat_hitting_min(m) doesn't work for m <= 14.
  • Are these instances in MU(1) so large?
  • Or should we start from different elements F in SMU(1) ?
  • Or is the heuristic so weak?
    1. For comparison, we need a precise decision algorithm.
Todo:
Creating marginal elements of MU(1)
  • One can create such elements with si_inverse_singulardp_fcs(FF,p,0,a,b).
  • What is the scope of marginal_musat1(k) ?
    1. Perhaps, once we have realised the systematic generation of marginal elements of MU(1) below, we remove this function.
    2. Or, if we randomise it, and start with arbitrary saturated elements, then we obtain a random element of MMU(1) in some sense; perhaps this is worth to study.
  • In [Kullmann, 2008] it is shown that the marginal elements of MU(1) are exactly those whose conflict graph is a tree (and all trees are realisable in this way).
    1. So a good way to create random elements of MMU(1) for a given number c of clauses is to create a random tree T with c vertices, and to construct the correspond F(T) in MMU(1).
    2. F(T) corresponds to the trivial biclique partition of T; compare "Translations to clause-sets" in ComputerAlgebra/Graphs/Lisp/BicliquePartitions/plans/general.hpp.
    3. Generators for trees are in ComputerAlgebra/Graphs/Lisp/Trees/Generators.mac.
    4. Via counting of isomorphism types of trees ("unlabelled trees") we thus obtain the number of isomorphism types of F in MMU(1) with a given number of variables. These counting functions should be implemented in module Graphs.
    5. If we only allow var-isomorphisms, what then is the number of isomorphism types?
  • For a given F in SMU(1), perhaps the marginal F' obtainable from F via literal-removal correspond exactly to the spanning trees of F? So if F has c clauses, then exactly c^(c-2) different marginal clause-sets are obtainable? Are these isomorphic iff the conflict-graphs are isomorphic?
  • One should test how SAT-solvers (with the appropriate preprocessing) react to MU(1): SMU(1) definitely should be easy, also the marginal elements (since they can be solved by UCP), but close to the marginal there could be harder elements?
Todo:
Creating saturated elements of MU(1)
  • F in SMU(1) has a unique tree representation (see above).
  • F, F' in SMU(1) are isomorphic iff their tree representations (as rooted trees) are isomorphic, while they are var-isomorphic iff their tree representations are isomorphic as left-right-trees (i.e., here we differentiate between "left" and "right").
  • So interesting things to do in Graphs/Trees are to enumerate/sample all binary trees with and without distinguishing left and right (for example there are 2 different such unlabelled structures with 5 vertices if distinguishing between left and right, and only one if not).
Todo:
Creating all F in MU(1) with var(F) = V
  • For a given set V of variables, all elements F in MU(1) with exactly this set of variables is to be listed.
  • And canonical representatives of isomorphism classes.
  • To get the elements of SMU(1), one just creates the binary trees where the inner nodes are labelled with unique elements from V.
    1. We have all2i_rt and rt2lrt_il in ComputerAlgebra/Trees/Lisp/Basics.mac.
  • Given the elements of SMU(1), one can then consider all "thinning outs" (removing literal occurrences with creating pure literals):
    1. In this way some clause-sets are created several times, but this seems hard to avoid.
    2. If there are m occurrences of a literal x, then from 0 to m-1 of these occurrences can be removed.

Definition in file DeficiencyOne.hpp.