OKlibrary  0.2.1.6
Translations.hpp File Reference

Plans for basic clause-set translations. More...

Go to the source code of this file.


Detailed Description

Plans for basic clause-set translations.

Todo:
Translations reducing the lengths of clauses
  • Shortening clauses by introducing new variables.
Todo:
Translations reducing the number of variable-occurrences
  • The basic step for a boolean clause-set F:
    1. Consider a literal x occurring in two different clauses C, D in F.
    2. Introduce a new variable v.
    3. Replace C, D by (C - {x}) + {v}, (D - {x}) + {v}, {-v,x}.
    4. 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
    1. All variables occur at most 3 times.
    2. All original clauses kept their length.
    3. 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:
    1. Consider a variable v occurring m >= 4 times.
    2. For each occurrence of v, introduce a new variable w_i.
    3. Replace each occurrence of v by the corresponding w_i, using the same sign.
    4. Add the equivalence ring (w_1 -> w_2), ..., (w_{m-1} -> 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 k-CNF at the end (with a small variable degree):
    1. First reduce or change the clause-length, by any method, for example reducing the clause-length as in the todo above, or increasing the clause-length by inverse 2-subsumption resolution.
    2. Then reduce the number of literal occurrences by any of the above two methods.
    3. Perhaps integration of these two operations can save variables.
    4. The final (and crucial step) is to expand the new binary clauses to size k:
      • The simplest method is inverse 2-subsumption 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 clause-set F_v, variable-disjoint except of v, which forces v to be false, and such that the variable-degree of F_v is at most s, except of v, which has a variable-degree at most s-1.
      • Such F_v are trivially obtained from any (minimally) unsatisfiable clause-set F which is k-uniform and has variable-degree 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.