Plans regarding minimally unsatisfiable clausesets of deficiency 1.
More...
Go to the source code of this file.
Detailed Description
Plans regarding minimally unsatisfiable clausesets of deficiency 1.
 Todo:
 Decision algorithms

The two basic decision algorithms for MU(1), by singular DPreduction or by finding accumulation variables, need to be implemented.

Using DPreduction:

Via sdp_reduction_cs(F) we can reduce the clauseset w.r.t. singular DPreduction.

The case of degeneration which can happen by sdp_reduction_cs(F) is blocking (i.e., tautological clauses would be produced).

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?

But due to blocking more variables could vanish (in clauses which get "lost"), and then the deficiency can also increase.

See "Singular DPreduction" in Satisfiability/Lisp/Reductions/plans/DPReductions.hpp.

They also extract a tree representation (see "Tree representations" below).

Also for the special cases "saturated" and "marginal" we need decision algorithms.

This can be done by checking each DPstep.

Alternatively, the input can be checked whether it is hitting resp. whether every variable has 11occurrence.
 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:

Find a variable v with degree 2.

Find its two occurrences C,D.

Replace C,D in F by their resolvent R, obtaining F'.

Apply the algorithm recursively to F', obtain T'.

In T', replace the leaf labelled with R by a new binary branching on v, with new leaves C,D.

Canonicity issues:

Most natural seems to be an ofcs input FF.

The task then is to find the first variable with degree 2, "first" w.r.t. the order given by FF.

For that, we need min_variable_degree_v_ofcs, which returns the first variable with minimal degree.

This can be achieved by first setting the variables in the given order to 0 in the hashmap.

A basic question is whether tree representations are unique up to rootedtreeisomorphism?

The most natural point of view seems not to distinguish between left and right children.

If we do distinguish them (so the trees are what is called "leftrighttrees"), then we only consider varisomorphisms.
 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 clauseset in MU(1) by considering the vertices of G as variables, taking all vertices as S as positive unitclause, 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 clausesets in MU(1). Get we also all Horn claussets? 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 unitclause.

The general question arises here about the characterisation of all Horn clausesets in MU(1).
 Todo:
 Small variabledegrees in MU(1)

Motivated by [Hoory, Szeider, TCS 2005] we consider the following decision problem:

Input a clauseset 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 clauselength is at least k, to obtain a maximal variabledegree of at most r.

The interesting case here is F in SMU(1), where it is guaranteed that the literalremovalprocess will never contract clauses (since every clause contains a literal occurring only once).

But this procedure is also relevant in general, since the resulting clauseset is always an unsatisfiable clauseset with parameters (k,r) in the typical setting here (i.e., minimal rank >= k, maximal variabledegree <= r).

Let's call it "REMLITOCC".

The problem is in NP, one likely also NPcomplete (also for inputs from SMU(1)).

The general question is to find out for given uniform clauselength k what is the smallest possible variabledegree 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:

Apparently f_1(3)+1 = 4 and f_1(4)+1 = 5 are the only known precise values.

Interesting also the (minimal) clausenumbers for realising the minimal parameter values (since the deficiency is fixed, this is the same as minimising the number of variables used).

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

[Hoory, Szeider] realise (k=4,r=5) (optimal) and (k=5,r=7), and other values, but one has to investigate the underlying clausesets (which are not discussed there explicitely).

We should exhibit such examples.

We should implement [Hoory, Szeider]; perhaps also [Dubois, DAM 1990] contains some constructions.

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?

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

Perhaps, once we have realised the systematic generation of marginal elements of MU(1) below, we remove this function.

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

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

F(T) corresponds to the trivial biclique partition of T; compare "Translations to clausesets" in ComputerAlgebra/Graphs/Lisp/BicliquePartitions/plans/general.hpp.

Generators for trees are in ComputerAlgebra/Graphs/Lisp/Trees/Generators.mac.

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.

If we only allow varisomorphisms, what then is the number of isomorphism types?

For a given F in SMU(1), perhaps the marginal F' obtainable from F via literalremoval correspond exactly to the spanning trees of F? So if F has c clauses, then exactly c^(c2) different marginal clausesets are obtainable? Are these isomorphic iff the conflictgraphs are isomorphic?

One should test how SATsolvers (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 varisomorphic iff their tree representations are isomorphic as leftrighttrees (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.

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

In this way some clausesets are created several times, but this seems hard to avoid.

If there are m occurrences of a literal x, then from 0 to m1 of these occurrences can be removed.
Definition in file DeficiencyOne.hpp.