OKlibrary  0.2.1.6
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.

Todo:
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.
Todo:
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.