Translations.hpp File Reference

Plans on autarky search via translation to other problems. More...

Go to the source code of this file.

Detailed Description

Plans on autarky search via translation to other problems.

Basic translation
  • Implement the basic translation, which just translates the boolean F into a G with variables over {-1,0,1}.
  • That is, for every old boolean variable v we obtain a new variable a(v) with domain {-1,0,+1}, every positive literal v becomes "a(v) <> -1", and every negative literal -v becomes "a(v) <> 1".
  • So every clause of F yields a clause of G; this is yet not strong enough, since we must forbid that a clause C in F contains falsified literals but no satisfied literals. For this we need |C| many clauses of length |C| which express that if a literal becomes false then some other literal becomes true. So we actually need monosigned literals.
  • Having those "autarky clauses", we do not need the direct translations of the original clauses.
  • The requirement that the autarky is non-trivial is expressed by the disjunction "a(v) <> 0" over all variables v.
  • The boolean translation of this non-boolean CNF just uses variables a(v,e) for variables v and signs e in {-1,0,+1}.
  • Non-triviality becomes the clause {a(v,0) : v in var(F)}.
  • The ALO-clauses {a(v,-1), a(v,0), a(v,+1)} for all v in var(F) are needed, and since we use monosigned literals, also the AMO clauses {-a(v,e), -a(v,e')} are needed.
Translation to SAT according to Liffiton and Sakallah
  • We need the usual accompanying statistics-functions.
  • See the Guangzhou-2008-talk for more example applications.
  • Extend the tests.
  • Via creating a splitting tree for the translated instance, and translating the satisfying assignments, compute all autarkies.
    1. Due to the symmetries we have many satisfying assignments; can we improve on that?
  • lean_usat_ls:
    1. Generalise the translation, so that one can specifically ask for certain variables to be used by the autarky.
    2. One can also ask for a set of clauses (or a single clause) to be satisfied.
  • Create a demo.
  • The solver of Liffiton/Sakallah uses AtMost-constraints to restrict the number of clauses not affected by the autarky:
    1. This avoids the problem with the long clause enforcing a non-trivial autarky.
    2. We also need soon a framework where such "constraints" can be used; of course, that's at the heart of "generalised SAT".
    3. This is also useful for the above basic translation.
    4. Liffiton/Sakallah start searching for as many satisfied clauses as possible --- for hard instances the opposite direction should be favourable (given that smaller autarkies exist!).
  • DONE Extend the documentation on the meaning of the variables.
  • DONE Implement the back-translation, satisfying assignments to autarkies.
  • DONE Derive an autarky-search-function (searching for some non-trivial autarky, using some SAT-solver as argument).
  • DONE Write a generic autarky-search-test (as a testfunctions, testing functions which return a non-trivial autarky or "false" if none exists).

Definition in file Translations.hpp.