On investigations regarding the nested translations.
More...
Go to the source code of this file.
Detailed Description
On investigations regarding the nested translations.
The standard nested translation is computed by nbfclud2fcl_standnest(FF) at Maximalevel.
 Todo:
 Strong form

The task is to add binary clauses, in order to strengthen inference.

For k+1 values in the domain, a maximal set of binary clauses (to be added to the "remainder") is computed by:
add_bincl_nec(smusat_horn_stdfcs(k)[2],{},dll_simplest_trivial2);

There are various maximal sets of addable binary clauses, but their numbers seems to be (constantly) k*(k1)/2:
for k : 0 thru 8 do print(k,length(add_bincl_nec(smusat_horn_stdfcs(k)[2],{},dll_simplest_trivial2)));
0 0
1 0
2 1
3 3
4 6
5 10
6 15
7 21
8 28

One needs to understand how these solutions arise, and how to choose one of them.

The simplest case is k=2, where we have two possibilities: {{1,2}} and {{2,1}} (where smusat_horn_stdfcs(2) = [{1,2},{{2,1},{1,2},{1}}]).

k=3

smusat_horn_stdfcs(3) = [{1,2,3},{{3,2,1},{2,1,3},{1,2},{1}}]

{{1,2},{1,3},{2,3}} is a possible extension.

So it seems one maximal solution for smusat_horn_stdfcs(k) is powerset(set(k),2) (which has size k*(k1)/2); the following tests all yield "true":
for k : 0 thru 5 do block(
[V : create_list(i,i,1,5),
D : create_list(i,i,1,k+1), Vt, TR_strong],
Vt : standnest_TV(D),
TR_strong : buildq([Vt],lambda([v], listify(powerset(setify(Vt(v)),2)))),
print(k, gennest_nbfcl2fcl_p(V,lambda([v],D),dll_simplest_trivial2, standnest_T(D),TR_strong,standnest_TV(D))))$

And the proof that after addition of all positive binary clauses all of the clauses of smusat_horn_stdfcs(k) are still necessary is simple: Consider the k+1 total assignment which set at most one variable to false (and all other to true): these assignments falsify exactly the k+1 clauses from smusat_horn_stdfcs(k) respectively, and satisfy all other clauses.
 Todo:
 The order of Horn clauses

Yet we considered only "standard" weak and strong nested translations, where the goal is to minimise the number of literal occurrences, and thus the shorter clauses are used for the smaller arithmetic progressions (since the number of arithmetic progressions decreases with increasing progression size).

However this creates long clauses. One would use the opposite order if the goal is to avoid having long clauses (this would have a tendency to make the translated clauses equal in size).
 Todo:
 The reduced forms

The weak reduced translation is obtained from the strong nested translation by performing subsumptionresolution with the additional 2clauses (and the resolvents), and then discarding these 2clauses, while for the strong reduced translation they are kept.

For the fully symmetry problem greentao_3(3,3,3) (see Investigations/RamseyTheory/GreenTaoProblems/plans/GreenTao_33.hpp) the OKsolver actually nodes considerably more time for the strong reduced form than for the logarithmic translation, while from the latter by two subsumptionresolutionsteps per variable we get the strong reduced form. This should be just idiosyncratic for the OKsolver_2002's heuristic, but in general there is the problem, to which value to associate the long clause of the reduced translation. Compare "The order of Horn clauses" above.
Definition in file NestedTranslation.hpp.