OKlibrary  0.2.1.6
AutarkyMonoid.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 5.7.2008 (Swansea) */
00002 /* Copyright 2008 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00022 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/PartialAssignments.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Algebra/Lisp/Groupoids/Closures.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/RandomClauseSets.mac")$
00027 
00028 
00029 /* The autarky monoid is computed by M = autmon_cs(F), while the set of 
00030    autarkies is A = all_aut_cs(F) = M[1] (and the composition is
00031    compo_pass = M[2]; all_sat_cs(F) is the set of all (total) satisfying
00032    assignments).
00033    Extract the atoms by min_elements(disjoin({},A)) and the maximal autarkies
00034    by max_elements(A).
00035    The indecomposable elements are indecomposable_elements_bydef_grd(M).
00036 */
00037 
00038 /* ********************************
00039    * Analysing the autarky monoid *
00040    ********************************
00041 */
00042 
00043 /* First attempt at analysing the autarky monoid: Computing
00044  - the set of autarkies
00045  - the set of indecomposable autarkies
00046  - the set of atomic autarkies
00047  - the variables involved in any autarky
00048  - the variables involved only in indecomposable autarkies
00049  - the variables involved only in atomic autarkies
00050  - the largest autark subset
00051  - all clauses satisfied by indecomposable autarkies
00052  - all clauses satisfied by atomic autarkies.
00053 */
00054 analyse_autmon(F) := block([M : autmon_cs(F), V,FA, At,VAt,Ft, I,VI,Fi],
00055   V : var_cs(M[1]), FA : scls_V(F,V),
00056   At : min_elements(disjoin({},M[1])), VAt : var_cs(At), Ft : scls_V(F,VAt),
00057   I : indecomposable_elements_bydef_grd(M), VI : var_cs(I), Fi : scls_V(F,VI),
00058   [M[1],I,At,  V,VI,VAt, FA,Fi,Ft])$
00059 
00060 
00061 /* ************
00062    * Examples *
00063    ************
00064 */
00065 
00066 trivial_exmp1_autmon_fcs(n) := [setn(n), {setn(n)}]$
00067 /* The structure of the autarky monoid for
00068     F : trivial_exmp1_autmon_fcs(n)[2]
00069     M : autmon_cs(F)
00070    is as follows:
00071  - There are n minimal autarkies {i}, i.e., 
00072    min_elements(disjoin({},M[1])) = setify(create_list({i},i,1,n)).
00073  - There are 2^n-1 maximal autarkies (the satisfying total assignments) for
00074    n >= 1, while for n=0 we have one; i.e.,
00075    length(max_elements(M[1])) = if n=0 then 1 else 2^n - 1.
00076  - There are 3^n - (2^n - 1) autarkies (exclude all negative assignments), 
00077    i.e.,
00078    length(M[1]) = 3^n - 2^n + 1.
00079  - There are n + n(n-1) + 1 indecomposable autarkies, namely the minimal
00080    autarkies, the autarkies {i,-j}, and the empty autarky.
00081    This yields also a (smallest w.r.t. semigroup-generation) generating set,
00082    i.e.,
00083    length(indecomposable_elements_bydef_grd(M)) = n + n*(n-1) + 1,
00084    is(closure_bydef_grd(M[2], indecomposable_elements_bydef_grd(M)) = M[1]).
00085 */
00086 
00087 trivial_exmp2_autmon_fcs(n) := [setn(2*n), 
00088  setify(create_list({2*i-1,2*i},i,1,n))]$
00089 /* The structure of the autarky monoid for
00090     F : trivial_exmp2_autmon_fcs(n)[2]
00091     M : autmon_cs(F)
00092    is as follows:
00093  - There are 2n minimal autarkies {i}, i.e., 
00094    min_elements(disjoin({},M[1])) = setify(create_list({i},i,1,2*n)).
00095  - There are 3^n satisfying total assignments, which are the
00096    combinations of the three satisfying assignmens {x,y},{-x,y},{y,-x}
00097    for the clauses {x,y}, wherex=2i-1 and y=2i, i.e.,
00098    length(all_sat_cs(F)) = 3^n.
00099  - There are 6^n autarkies, which are the combinations of the 6
00100    autarkies for the clauses {x,y} (see trivial_exmp1_autmon_fcs),
00101    i.e.,
00102    length(M[1]) = 6^n.
00103  - There are 4n+1 indecomposable autarkies, which are the four indecomposable
00104    autarkies for each clause {x,y}, plus the empty autarky, and this yields 
00105    also a (smallest w.r.t. semigroup-generation) generating set, i.e.,
00106    length(indecomposable_elements_bydef_grd(M)) = 4*n+1,
00107    is(closure_bydef_grd(M[2], indecomposable_elements_bydef_grd(M)) = M[1]).
00108 */
00109 
00110 /* *******************************************
00111    * On "sufficient" selections of autarkies *
00112    *******************************************
00113 */
00114 
00115 /* An open problem: Does the following function always return true? */
00116 /* The CONJECTURE is that it does. */
00117 are_indecomposable_autarkies_sufficient_cs(F) := block([A : analyse_autmon(F)],
00118   is(A[8] = A[7]))$
00119 
00120 /* Searching for counter-examples: */
00121 
00122 test_sufficiency_indaut(n,k,c) := block([found : false], 
00123  unless found#false do
00124   block([F : setify(random_fcl(n,k,c)[2]), an],
00125    an : analyse_autmon(F),
00126    if oklib_monitor then
00127      print(F, ":", statistics_cs(F), map(length,an)),
00128    if length(an[8]) < length(an[7]) then
00129      found : F
00130    ),
00131  return(found))$
00132 test_sufficiency_indaut_rcl(n,p,c) := block([found : false], 
00133  unless found#false do
00134   block([F : setify(random_rcl_fcl(n,p,c)[2]), an],
00135    an : analyse_autmon(F),
00136    if oklib_monitor then
00137      print(F, ":", statistics_cs(F), map(length,an)),
00138    if length(an[8]) < length(an[7]) then
00139      found : F
00140    ),
00141  return(found))$
00142 test_sufficiency_indaut_rrcl(n,c) := block([found : false], 
00143  unless found#false do
00144   block([p : random(1.0), F, an],
00145    F : setify(random_rcl_fcl(n,p,c)[2]),
00146    an : analyse_autmon(F),
00147    if oklib_monitor then
00148      print(F, ":", statistics_cs(F), map(length,an)),
00149    if length(an[8]) < length(an[7]) then
00150      found : F
00151    ),
00152  return(found))$
00153 test_sufficiency_indaut_rnrrcl(n,c0) := block([found : false], 
00154  unless found#false do
00155   block([p : random(1.0), c : random(c0), F, an],
00156    F : setify(random_rcl_fcl(n,p,c)[2]),
00157    an : analyse_autmon(F),
00158    if oklib_monitor then
00159      print(F, ":", statistics_cs(F), map(length,an)),
00160    if length(an[8]) < length(an[7]) then
00161      found : F
00162    ),
00163  return(found))$
00164 
00165 
00166 /* **********************
00167    * On autarky duality *
00168    **********************
00169 */
00170 
00171 /* The restricted autarky-closure: */
00172 rautclosure_bydef_cs(F) := all_aut_cs(all_aut_cs(F))$
00173 
00174 rautclosure1_cs(F) := 
00175  adjoin({},closure_bydef_grd(compo_pass,resolution_closure_cs(F)[1]))$
00176 /* An example where rautclosure1_cs(F) < rautclosure_bydef_cs(F):
00177  {{-4,-3,-2,-1},{-4,-1,2,3},{-2,4}}. */
00178 rautclosure2_cs(F) := 
00179  adjoin({},resolution_closure_cs(closure_bydef_grd(compo_pass,F))[1])$
00180 
00181 /* Question: Is always rautclosure2_cs(F) a superset of
00182    rautclosure_bydef_cs(F)? */
00183 /* The CONJECTURE is that this is true. */
00184 experiment_autclosures(n,c0) := block([found : false],
00185  unless found#false do
00186   block([p : random(1.0), c : random(c0), F, F0,F2],
00187    F : setify(random_rcl_fcl(n,p,c)[2]),
00188    F0 : rautclosure_bydef_cs(F),
00189    F2 : rautclosure2_cs(F),
00190 print(map(statistics_cs,[F,F0,F2])),
00191    if not subsetp(F0,F2) then
00192      found : [F,2]
00193    ),
00194  return(found))$
00195