Plans for basic clauseset translations.
More...
Go to the source code of this file.
Detailed Description
Plans for basic clauseset translations.
 Todo:
 Translations reducing the lengths of clauses

Shortening clauses by introducing new variables.
 Todo:
 Translations reducing the number of variableoccurrences

The basic step for a boolean clauseset F:

Consider a literal x occurring in two different clauses C, D in F.

Introduce a new variable v.

Replace C, D by (C  {x}) + {v}, (D  {x}) + {v}, {v,x}.

In effect, we eliminated one occurrence of literal x, and we introduced a new variable v occurring (2,1).

Performing this basic step iteratedly for all literals such that the underlying variable occurs at least 4 times (so we never need to consider the newly introduced variables), we obtain F' such that

All variables occur at most 3 times.

All original clauses kept their length.

All new clauses are binary.

Alternatively, by [Tovey, 1984, DAM] we obtain a different general translation, which for a variable v in F occurring at least 4 times removes all occurrences at once as follows:

Consider a variable v occurring m >= 4 times.

For each occurrence of v, introduce a new variable w_i.

Replace each occurrence of v by the corresponding w_i, using the same sign.

Add the equivalence ring (w_1 > w_2), ..., (w_{m1} > w_m), (w_m > w_1).
This translation has the same 3 properties as the above translation, and additionally when considering only the new binary clauses, then every variable occurs only 2 times.

There is also interest in obtaining also a uniform kCNF at the end (with a small variable degree):

First reduce or change the clauselength, by any method, for example reducing the clauselength as in the todo above, or increasing the clauselength by inverse 2subsumption resolution.

Then reduce the number of literal occurrences by any of the above two methods.

Perhaps integration of these two operations can save variables.

The final (and crucial step) is to expand the new binary clauses to size k:

The simplest method is inverse 2subsumption resolution, but this introduces too many literal occurrences.

A more powerful general method (used by [Tovey, 1984, DAM]) is to expand a clause C simply by new variables v to the desired length k, and then to add for each new variable v a dedicated clauseset F_v, variabledisjoint except of v, which forces v to be false, and such that the variabledegree of F_v is at most s, except of v, which has a variabledegree at most s1.

Such F_v are trivially obtained from any (minimally) unsatisfiable clauseset F which is kuniform and has variabledegree at most s (by removing one clause).

See "Pumping up binary clauses" in ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/plans/general.hpp for dedicated constructions of such F_v.
Definition in file Translations.hpp.