OKlibrary  0.2.1.6
DP-Reductions.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 25.4.2008 (Guangzhou) */
00002 /* Copyright 2008, 2009, 2012 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/Satisfiability/Lisp/Resolution/Basics.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Statistics.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Symmetries/Symmetries.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00027 
00028 
00029 /* *************************
00030    * Singular DP-reduction *
00031    *************************
00032 */
00033 
00034 /* Applying elimination of singular literals as long as possible, choosing
00035    always the first singular variable available (in the Maxima-order): */
00036 sdp_reduction_cs(F) := block([S : singular_variables_cs(F)],
00037  if emptyp(S) then return(F) else
00038  return(sdp_reduction_cs(dp_operator_cs(F,first_element(S)))))$
00039 
00040 /* Full reduction regarding 1sDP-reduction (which is confluent): */
00041 onesdp_reduction_cs(F) := block([S : onesingular_variables_cs(F)],
00042  if emptyp(S) then return(F) else
00043  return(onesdp_reduction_cs(dp_operator_cs(F,first_element(S)))))$
00044 
00045 /* Computing a maximal non-1-singular tuple for F, choosing the first
00046    available variables (in the Maxima-order): */
00047 nononesingulartuple_cs(F) := block([S : nononesingular_variables_cs(F), v],
00048  if emptyp(S) then return([]) else (
00049   v : first_element(S),
00050   return(cons(v,nononesingulartuple_cs(dp_operator_cs(F,v))))))$
00051 
00052 /* The set of all fully reduced results obtained by sDP-reduction: */
00053 sdp_set_cs_bydef(F) := block([S : singular_variables_cs(F)],
00054  if emptyp(S) then return({F}) else
00055  return(lunion(map(lambda([v],sdp_set_cs_bydef(dp_operator_cs(F,v))),
00056                    listify(S)))))$
00057 
00058 /* For a list [v_1,...,v_n] of variables and a clause-set F, determine the
00059    maximal 0 <= m <= n such that [v_1,...,v_m] is a singular tuple, and
00060    return [d_1,...,d_m] such that v_i is d_i-singular in
00061    DP_{v_1,...,v_{i-1}}(F):
00062 */
00063 singulartuple_degrees_cs(V,F) := block([result : [], a,b],
00064  for v in V do (
00065   a : literal_degree_cs(F,v), b : literal_degree_cs(F,-v),
00066   if min(a,b)#1 then return(),
00067   result : cons(max(a,b),result),
00068   F : dp_operator_cs(F,v)
00069  ),
00070  reverse(result))$
00071 /* Checking whether V is a singular tuple (list) for clause-set F: */
00072 singulartuple_csp(V,F) := is(length(singulartuple_degrees_cs(V,F))=length(V))$
00073 
00074 /* Checking properties of singular tuples: */
00075 /* Are all entries of the singularity-degree sequence equal to 1: */
00076 onesingulartuple_csp(V,F) :=
00077  every_s(lambda([x], is(x=1)), singulartuple_degrees_cs(V,F))$
00078 /* Are all entries of the singularity-degree sequence not equal to 1: */
00079 nononesingulartuple_csp(V,F) :=
00080  every_s(lambda([x], is(x>1)), singulartuple_degrees_cs(V,F))$
00081 /* Is V totally singular, that is, every permutation is singular: */
00082 totally_singulartuple_csp_bydef(V,F) :=
00083  every_s(lambda([P],singulartuple_csp(P,F)), permutations(V))$
00084 
00085 /* The set of all variable-sets of singular tuples (i.e., singular sets)
00086    for clause-set F:
00087 */
00088 sdpss_cs_bydef(F) :=
00089  adjoin({},
00090   lunion(map(lambda([v],add_element(v,sdpss_cs_bydef(dp_operator_cs(F,v)))),
00091          listify(singular_variables_cs(F)))))$
00092 /* The hypergraph of singular sets of clause-set F: */
00093 sdphg_cs_bydef(F) := [var_cs(F),sdpss_cs_bydef(F)]$
00094 
00095 /* The set of all variable-sets of 1-singular tuples (i.e., 1-singular sets)
00096    for clause-sets F:
00097 */
00098 onesdpss_cs_bydef(F) :=
00099  adjoin({},
00100   lunion(map(lambda([v],add_element(v,onesdpss_cs_bydef(dp_operator_cs(F,v)))),
00101          listify(onesingular_variables_cs(F)))))$
00102 /* The hypergraph of 1-singular sets of clause-set F: */
00103 onesdphg_cs_bydef(F) := [var_cs(F),onesdpss_cs_bydef(F)]$
00104 
00105 /* The set of maximal non-1-singular tuples for F: */
00106 maxnononesdpst_cs_bydef(F) := block([L : nononesingular_variables_cs(F)],
00107  if emptyp(L) then {[]} else
00108  lunion(map(lambda([v],
00109                map(lambda([t],cons(v,t)),
00110                maxnononesdpst_cs_bydef(dp_operator_cs(F,v)))),
00111         listify(L))))$
00112 
00113 /* The number of different reduction-results via sDP: */
00114 sdp_count_cs_bydef(F) := length(sdp_set_cs_bydef(F))$
00115 /* Whether sDP-reduction is confluent: */
00116 cfsdp_csp_bydef(F) := is(sdp_count_cs_bydef(F) = 1)$
00117 
00118 /* The number of isomorphism-classes in sDP(F): */
00119 cfisdp_count_cs_bydef(F) := length(representatives_cs(sdp_set_cs_bydef(F)))$
00120 /* Whether sDP-reduction is confluent modulo isomorphism: */
00121 cfisdp_csp_bydef(F) := is(cfisdp_count_cs_bydef(F) = 1)$
00122 
00123 
00124 /* Predicate for testing whether clause-set F is reduced w.r.t. singular
00125    DP-reduction: */
00126 nonsingular_csp(F) := emptyp(singular_variables_cs(F))$
00127 /* Testing whether clause-set F is reduced w.r.t. 1-singular DP-reduction: */
00128 nononesingular_csp(F) := emptyp(onesingular_variables_cs(F))$
00129 
00130