OKlibrary  0.2.1.6
PartialAssignments.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 5.7.2008 (Swansea) */
00002 /* Copyright 2008, 2011, 2012, 2013 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/ClauseSets/BasicOperations.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00024 
00025 
00026 /* ****************************************
00027    * The notion of a "partial assignment" *
00028    ****************************************
00029 */
00030 
00031 /*
00032  A "partial boolean assignment" is a boolean clause, interpreted
00033  as setting its elements to true.
00034 */
00035 
00036 pa_p(phi) := c_p(phi)$
00037 
00038 /* ***********************************
00039    * Enumerating partial assignments *
00040    ***********************************
00041 */
00042 
00043 /* The set of all partial assignments over a set of variables: */
00044 all_pass(V) := if emptyp(V) then {{}} else
00045  block([e : choose_element(V), S],
00046   S : all_pass(disjoin(e,V)),
00047   return(union(S,
00048            map(lambda([phi],adjoin(e,phi)),S),
00049            map(lambda([phi],adjoin(-e,phi)),S))))$
00050 /* Now V is a list, and returned is a list (in lexicographical
00051    order, when representing a partial assignment as a total function
00052    in list-representation, using the linear order on V, and using the
00053    order "undefined" < false < true on the values): */
00054 all_pass_l(V) := if emptyp(V) then [{}] else
00055  block([e : first(V), S],
00056   S : all_pass_l(rest(V)),
00057   return(append(S,
00058            map(lambda([phi],adjoin(-e,phi)),S),
00059            map(lambda([phi],adjoin(e,phi)),S))))$
00060 /* This time only those partial assignments with domain size n. */
00061 all_pass_n(V,n) := if n < 0 then {}
00062  elseif n=0 then {{}}
00063  elseif emptyp(V) then {}
00064  else block([e : choose_element(V), S0, S1],
00065    V : disjoin(e,V),
00066    S0 : all_pass_n(V,n-1),
00067    S1 : all_pass_n(V,n),
00068    return(union(S1,
00069             map(lambda([phi],adjoin(e,phi)),S0),
00070             map(lambda([phi],adjoin(-e,phi)),S0))))$
00071 
00072 /* The set of all total assignments over a set or list V of variables: */
00073 all_tass(V) := setify(all_tass_l(V))$
00074 /* Given V as a list, return a list, using lexicographical order over
00075    [-v_1,v_1,-v_2,v_2,...,-v_n,v_n] for V = [v_1,...,v_n]:
00076 */
00077 all_tass_l(V) := map(setify, cartesian_product_l(map(lambda([v],[-v,v]),V)))$
00078 /* Remark: If V is actually a set, then we obtain listify(all_tass(V)), that
00079    is, lexicographical order over [-v_n,...,-v_1,v_1,...,v_n].
00080 */
00081 
00082 
00083 /* ********************
00084    * Basic operations *
00085    ********************
00086 */
00087 
00088 /* The variables in a partial assignment: */
00089 var_pa(phi) := var_c(phi)$
00090 
00091 /* Restricting a partial assignment phi to a set V of variables.
00092    (V does not need to be a subset of var_pa(phi).) */
00093 restr_pa(phi,V) := subset(phi, lambda([x], elementp(var_l(x),V)))$
00094 /* Remove variables in V from phi: */
00095 restr_c_pa(phi,V) := subset(phi, lambda([x], not elementp(var_l(x),V)))$
00096 
00097 /* The composition of partial assignments (first phi, then psi): */
00098 compo_pass(psi,phi) := union(phi, setdifference(psi,comp_sl(phi)))$
00099 
00100 
00101 /* **********
00102    * Output *
00103    **********
00104 */
00105 
00106 oklib_plain_include("stringproc")$
00107 
00108 /* Prints the partial assignment phi in Dimacs-format: */
00109 print_pa(phi) := print_nlb(sconcat("v ", dimacs_c_string(phi), "0"))$
00110 /* Output a partial assignment phi to a file: */
00111 output_pa(phi,file) := with_stdout(file, print_pa(phi))$
00112 
00113 
00114 /* ********************************
00115    * Applying partial assignments *
00116    ********************************
00117 */
00118 
00119 /* Apply a partial assignment to a boolean clause-set. */
00120 /* RENAME: apply_pa_cs */
00121 apply_pa(phi,F) := setdifference2(remove_non_disjoint(F,phi), comp_sl(phi))$
00122 apply_pa_cs(phi,F) := apply_pa(phi,F)$
00123 apply_pa_cl(phi,F) := block([comp_phi : comp_sl(phi)],
00124   map(lambda([C],setdifference(C,comp_phi)),
00125       sublist(F,lambda([C],disjointp(C,phi)))))$
00126 /* RENAME: apply_pa_fcs */
00127 apply_pa_f(phi,FF) := [setdifference(var_cs_f(FF), var_pa(phi)),
00128   apply_pa_cs(phi, clauses_f(FF))]$
00129 apply_pa_fcs(phi,FF) := apply_pa_f(phi,FF)$
00130 
00131 /* In-place modification, argument _F passed by name; returns "true": */
00132 apply_pa_ip_cl(phi,_F) := block([comp_phi : comp_sl(phi)],
00133   _F :: sublist(ev(_F),lambda([C],disjointp(C,phi))),
00134   _F :: map(lambda([C],setdifference(C,comp_phi)),ev(_F)),
00135   true)$
00136 
00137 
00138 /* ****************************************************
00139    * Analysing partial assignments for satisfyingness *
00140    ****************************************************
00141 */
00142 
00143 /* Tests whether a partial assignment satisfies a clause: */
00144 sat_pac_p(phi,C) := not disjointp(phi,C)$
00145 
00146 /* Test for a satisfying assignment w.r.t. a clause-set: */
00147 /* RENAME: sat_pacs_p */
00148 satisfyingpap(phi,F) := every_s(lambda([C],sat_pac_p(phi,C)),F)$
00149 sat_pacs_p(phi,F) := satisfyingpap(phi,F)$
00150 sat_paocs_p(phi,F) :=  every_s(lambda([C],sat_pac_p(phi,C)),F)$
00151 sat_pacl_p(phi,F) := every_s(lambda([C],sat_pac_p(phi,C)),F)$
00152 /* RENAME: sat_pafcs_p */
00153 /* Test for a satisfying assignment w.r.t. a formal clause-set: */
00154 satisfyingpafp(phi,FF) := sat_pacs_p(phi,FF[2])$
00155 sat_pafcs_p(phi,FF) := satisfyingpafp(phi,FF)$
00156 sat_paofcs_p(phi,FF) := sat_paocs_p(phi,FF[2])$
00157 sat_pafcl_p(phi,FF) := sat_pacl_p(phi,FF[2])$
00158 
00159 /* The set of satisfied clauses for a partial assignment w.r.t. a clause-set:
00160 */
00161 /* RENAME: sat_pa_cs */
00162 sat_pa(phi,F) := subset(F, lambda([C], sat_pac_p(phi,C)))$
00163 sat_pa_cs(phi,F) := sat_pa(phi,F)$
00164 /* RENAME: sat_pa_fcs */
00165 sat_paf(phi,FF) := sat_pa(phi,FF[2])$
00166 sat_pa_fcs(phi,FF) := sat_paf(phi,FF)$
00167 
00168 
00169 /* ************************************************
00170    * Analysing partial assignments for autarkness *
00171    ************************************************
00172 */
00173 
00174 /* Test for a weak autarky w.r.t. a clause-set: */
00175 waut_pacs_p(phi,F) := is(subsetp(apply_pa_cs(phi,F),F))$
00176 
00177 /* Test for an autarky w.r.t. a clause-set: */
00178 aut_pacs_p(phi,F) := block([cphi : comp_sl(phi)],
00179   every_s(lambda([C], disjointp(cphi,C) or not disjointp(phi,C)), F))$
00180 aut_paocs_p(phi,F) := block([cphi : comp_sl(phi)],
00181   every_s(lambda([C], disjointp(cphi,C) or not disjointp(phi,C)), F))$
00182 aut_paofcs_p(phi,FF) := block([cphi : comp_sl(phi)],
00183   every_s(lambda([C], disjointp(cphi,C) or not disjointp(phi,C)), FF[2]))$
00184 
00185 
00186 /* ********************************************
00187    * Complete analysis of partial assignments *
00188    ********************************************
00189 */
00190 
00191 /* The set of satisfied, falsified, untouched and critical (original) clauses
00192    for a partial assignment phi w.r.t. a clause-set F. */
00193 /* These four sets constitute a partioning of F:
00194     - if F contains {}, then this belongs to the falsified clauses;
00195     - a critical clause is a touched but neither satisfied nor
00196       falsified clause.
00197 */
00198 /* RENAME: analyse_pa_cs */
00199 analyse_pa(phi,F) := block([V : var_c(phi), s : {}, f : {}, u : {}, c : {}],
00200  for C in F do block([r : apply_pa_cs(phi,{C})],
00201   if r = {} then s : adjoin(C,s)
00202   elseif r = {{}} then f : adjoin(C,f)
00203   elseif disjointp(var_c(C), V) then u : adjoin(C,u)
00204   else c : adjoin(C,c)),
00205  return([s,f,u,c]))$
00206 analyse_pa_cs(phi,F) := analyse_pa(phi,F)$
00207 /* RENAME: analyse_pa_fcs */
00208 analyse_paf(phi,FF) := analyse_pa_cs(phi,FF[2])$
00209 analyse_pa_fcs(phi,FF) := analyse_paf(phi,FF)$
00210 
00211 
00212 /* ************************************
00213    * All satisfying assignments bydef *
00214    ************************************
00215 */
00216 
00217 /* The set of all satisfying total assignments of a clause-set F
00218     w.r.t. a set or list V of variables: */
00219 /* RENAME: all_sattass_cs */
00220 all_sat_tass(F,V) := subset(all_tass(V), lambda([phi],sat_pacs_p(phi,F)))$
00221 all_sattass_cs(F,V) := all_sat_tass(F,V)$
00222 /* For a list V of variables, using that order for the enumeration: */
00223 all_sattass_ocs(F,V) := sublist(all_tass_l(V),
00224   lambda([phi], sat_paocs_p(phi,F)))$
00225 all_sat_cs(F) := all_sattass_cs(F,var_cs(F))$
00226 all_sat_fcs(FF) := all_sattass_cs(FF[2],FF[1])$
00227 all_sat_ofcs(FF) := all_sattass_ocs(FF[2],FF[1])$
00228 
00229 
00230 /* ***********************
00231    * All autarkies bydef *
00232    ***********************
00233 */
00234 
00235 /* The set of all autarkies of a clause-set F: */
00236 all_aut_cs(F) := subset(all_pass(var_cs(F)), lambda([phi],aut_pacs_p(phi,F)))$/* As a repetition-free list, where for the order of partial assignments the
00237   order as the variables occur in the clauses is determinative: */
00238 all_aut_ocs(F) := sublist(all_pass_l(ovar_ocs(F)), lambda([phi],aut_paocs_p(phi,F)))$
00239 all_aut_ofcs(FF) := sublist(all_pass_l(FF[1]), lambda([phi],aut_paofcs_p(phi,FF)))$
00240 
00241 /* The autarky monoid of a clause-set: */
00242 autmon_cs(F) := [all_aut_cs(F), compo_pass, {}]$
00243 /* The "listified" autarky monoid of an ordered clause-set: */
00244 autmon_ocs(F) := [all_aut_ocs(F), compo_pass, {}]$
00245