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 nontrivial is expressed by the disjunction "a(v) <> 0" over all variables v.

The boolean translation of this nonboolean CNF just uses variables a(v,e) for variables v and signs e in {1,0,+1}.

Nontriviality becomes the clause {a(v,0) : v in var(F)}.

The ALOclauses {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 statisticsfunctions.

See the Guangzhou2008talk for more example applications.

Extend the tests.

Via creating a splitting tree for the translated instance, and translating the satisfying assignments, compute all autarkies.

Due to the symmetries we have many satisfying assignments; can we improve on that?

lean_usat_ls:

Generalise the translation, so that one can specifically ask for certain variables to be used by the autarky.

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 AtMostconstraints to restrict the number of clauses not affected by the autarky:

This avoids the problem with the long clause enforcing a nontrivial autarky.

We also need soon a framework where such "constraints" can be used; of course, that's at the heart of "generalised SAT".

This is also useful for the above basic translation.

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 backtranslation, satisfying assignments to autarkies.

DONE Derive an autarkysearchfunction (searching for some nontrivial autarky, using some SATsolver as argument).

DONE Write a generic autarkysearchtest (as a testfunctions, testing functions which return a nontrivial autarky or "false" if none exists).
Definition in file Translations.hpp.