OKlibrary  0.2.1.6
Formulas.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 12.1.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2010 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/Hypergraphs/Lisp/SetSystems.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$00025 00026 00027 /* *********************************** 00028 * Representation of formulas * 00029 *********************************** 00030 */ 00031 00032 /* A "propositional variable" is any term. */ 00033 /* A "propositional literal" is either a variable "v" or "neg(v)" 00034 or "true" or "false". */ 00035 00036 /* A "propositional formula" is a labelled tree, where the labels are either 00037 literals at the leaves or operation-labels at inner nodes, which are 00038 strings "and", "or", "xor", "equiv" representing n-ary operations, 00039 "impl" (binary) and "not" (unary). 00040 */ 00041 /* 00042 The deMorgan-base is "and", "or", "not". 00043 The empty "and" is true, the empty "or" is false, the empty "xor" is false, the 00044 empty "equiv" is true. 00045 */ 00046 00047 /* Remark: Consider [op, x1, ..., xn] where op is "equiv" or "xor": 00048 If n is even then "equiv" is the negation of xor, while for odd n 00049 "equiv" and "xor" or identical. 00050 If op is "equiv", then the evaluation is true iff an even number of the x_i 00051 are false, while if op is "xor" then the evaluation is true iff an odd 00052 number of the x_i are true. 00053 */ 00054 00055 kill(neg)$
00056 tellsimp(neg(false), true)$00057 tellsimp(neg(true), false)$
00058 matchdeclare(negexpr,true)$00059 tellsimp(neg(neg(negexpr)),negexpr); 00060 00061 /* The set of variables of a propositional literal */ 00062 var_prpl(x) := if not atom(x) and op(x) = neg then {first(x)} 00063 elseif x = true or x = false then {} 00064 else {x}$
00065 /* The set of variables of a propositional formula (tree) without empty operations */
00066 var_ft(F) := block([l : length(F)],
00067   if l = 1 then var_prpl(F[1]) else
00068   family_sets_union(setmn(2,l), lambda([i],var_ft(F[i]))))$00069 00070 /* Tests whether literal x is "true" or "false" */ 00071 truefalse_literalp(x) := is(x = true) or is(x = false)$
00072 /* tests whether formula F is "true" or "false" (as is) */
00073 truefalse_ft(F) := is(length(F) = 1) and truefalse_literalp(F[1])$00074 00075 00076 /* ****************************************** 00077 * Basic transformations of formula trees * 00078 ****************************************** 00079 */ 00080 00081 /* Replace equivalences by xor's */ 00082 equivalences2xors(F) := block([l : length(F)], 00083 if F[1] = "equiv" then 00084 if l = 1 then return([true]) 00085 elseif l = 2 then return(equivalences2xors(F[2])) 00086 elseif evenp(l) then 00087 return(cons("xor", makelist(equivalences2xors(F[i]),i,2,l))) 00088 else return(["not", cons("xor", makelist(equivalences2xors(F[i]),i,2,l))]) 00089 else return(cons(F[1], makelist(equivalences2xors(F[i]),i,2,l))))$
00090
00091 /* Eliminate implications */
00092 eliminate_implications_ft(F) := block([l : length(F)],
00093   if l = 3 and F[1] = "impl" then
00094     return(["or", ["not", eliminate_implications_ft(F[2])], eliminate_implications_ft(F[3])])
00095   else return(cons(F[1], map(eliminate_implications_ft, makelist(F[i],i,2,l)))))$00096 00097 /* Evaluating empty n-ary operations */ 00098 evaluate_empty_ft(F) := block([l : length(F)], 00099 if l >= 2 then return(cons(F[1], makelist(evaluate_empty_ft(F[i]),i,2,l))) 00100 elseif F[1] = "and" then return([true]) 00101 elseif F[1] = "or" then return([false]) 00102 elseif F[1] = "xor" then return([false]) 00103 elseif F[1] = "equiv" then return([true]) 00104 else return(F))$
00105
00106 /* Elimination of constants from a formula tree without implications, equivalences
00107    or empty operations (creating possibly unary operations and negations) */
00108 elimination_constants_ft(F) := block([l : length(F)],
00109   if l = 1 then return(F)
00110   else block([R : makelist(elimination_constants_ft(F[i]),i,2,l), C, nc, r],
00111     [C,R] : partition_list(R, truefalse_ft),
00112     if emptyp(C) then return(cons(F[1], R)),
00113     if F[1] = "not" then return([not R[1]]),
00114     nc : length(C),
00115     C : makelist(C[i][1],i,1,nc),
00116     if F[1] = "and" then (
00117       r : every_s(identity, C),
00118       if not r or nc = l-1 then return([r])
00119       else return(cons("and", R)))
00120     elseif F[1] = "or" then (
00121       r : some_s(identity, C),
00122       if r or nc = l-1 then return([r])
00123       else return(cons("or", R)))
00124     else /* now F[1] = "xor" */ (
00125       r : oddp(length(sublist_indices(C, identity))),
00126       if nc = l-1 then return ([r])
00127       elseif not r then return(cons("xor", R))
00128       else return(["not", (cons("xor", R))]))))$00129 00130 /* Eliminating superfluous unary operations */ 00131 eliminate_unary_ft(F) := block([l : length(F)], 00132 if l = 1 then F 00133 elseif l = 2 and F[1] # "not" then eliminate_unary_ft(F[2]) 00134 else cons(F[1], makelist(eliminate_unary_ft(F[i]),i,2,l)))$
00135
00136 /* Move the negations down a formula tree without equivalences or empty operations,
00137    using literals at the leaves, eliminating double negations. */
00138 /* deMorgan-formulas where negations appear only in literals are in
00139    "negation normal form". */
00140 move_negations_down(F) := move_negations_down_rel(F, false)$00141 move_negations_down_rel(F, negated) := block([l : length(F)], 00142 if l = 1 then if negated then return([neg(F[1])]) else return(F) 00143 elseif F[1] = "not" then return(move_negations_down_rel(F[2], not negated)) 00144 elseif negated then 00145 if F[1] = "or" then 00146 return(cons("and", makelist(move_negations_down_rel(F[i], true),i,2,l))) 00147 elseif F[1] = "and" then 00148 return(cons("or", makelist(move_negations_down_rel(F[i], true),i,2,l))) 00149 else /* now F[1] = "xor" */ 00150 return(append(["xor", move_negations_down_rel(F[2], true)], 00151 makelist(move_negations_down_rel(F[i], false),i,3,l))) 00152 else return(cons(F[1], makelist(move_negations_down_rel(F[i], false),i,2,l))))$
00153
00154
00155 /* Basic simplification of a formula-tree */
00156 basic_simplification_ft(F) := move_negations_down(eliminate_unary_ft(elimination_constants_ft(evaluate_empty_ft(eliminate_implications_ft(equivalences2xors(F))))))$00157 00158 00159 /* *********************** 00160 * Partial assignments * 00161 *********************** 00162 */ 00163 00164 /* A "partial assignment" for propositional logic is a set of propositional 00165 literals (to be set to true) 00166 */ 00167 00168 /* Apply a partial assignment to a literal */ 00169 apply_pa_prpl(phi,x) := block([vs : var_prpl(x)], 00170 if vs = {} then return(x), 00171 if elementp(x, phi) then return(true) 00172 elseif elementp(neg(x), phi) then return(false) 00173 else return(x))$
00174
00175 /* Apply a partial assignment to a formula tree (without simplification) */
00176 apply_pa_ft(phi, F) := block([l : length(F)],
00177   if l = 1 then return([apply_pa_prpl(phi,F[1])])
00178   else return(cons(F[1], makelist(apply_pa_ft(phi,F[i]),i,2,l))))$00179 00180 00181 /* ****************** 00182 * Measures * 00183 ****************** 00184 */ 00185 00186 /* number of variables in a formula tree */ 00187 nvar_ft(F) := length(var_ft(F))$
00188
00189 /* number of literal occurrences in a formula tree */
00190 nlitocc_ft(F) := nlvs_l(F)$00191 00192 /* number of binary "and" (interpreted as binary) in formula trees 00193 (typically this makes only sense if F is in negation normal form) */ 00194 nands_ft(F) := block([l : length(F)], 00195 if l = 1 then 0 else 00196 block([s : sum(nands_ft(F[i]),i,2,l)], 00197 if F[1] = "and" then return(l - 2 + s) 00198 else return(s) 00199 ))$
00200
00201 /* cohesion (generalisation of the deficiency) */
00202 cohesion_ft(F) := 1 + nands_ft(F) - nvar_ft(F)$00203 00204 00205 /* ****************** 00206 * Translations * 00207 ****************** 00208 */ 00209 00210 /* For a boolean variable v, prp(v) is the corresponding propositional 00211 variable. */ 00212 kill(prp)$
00213 declare(prp,noun)$00214 prp_var(v) := nounify(prp)(v)$
00215
00216 /* translating a boolean literal into a propositional literal */
00217 boollit_proplit(x) := if x > 0 then prp(x) else not prp(var_l(x))$00218 00219 /* a clause-set as a CNF */ 00220 cls_cnf(F) := cons("and", makelist( 00221 cons("or", map(lambda([x],[boollit_proplit(x)]),listify(C))), C, listify(F)))$
00222 /* a clause-set as a DNF */
00223 cls_dnf(F) := cons("or", makelist(
00224  cons("and", map(lambda([x],[boollit_proplit(x)]),listify(C))), C, listify(F)))$00225 00226 00227 /* **************************** 00228 * Tseitin translation * 00229 **************************** 00230 */ 00231 00232 /* A "path" P for a rooted tree T is a list of natural numbers (>= 1), denoting 00233 the list of branches starting with the root (so the root itself is 00234 represented by the empty list). 00235 */ 00236 00237 /* The variables for the Tseitin translation: tstr(P) is the variable 00238 corresponding to the node reached by path P in the formula tree 00239 */ 00240 kill(tstr)$
00241 declare(tstr,noun)$00242 tstr_var(P) := nounify(tstr)(P)$
00243
00244 /* Given a formula tree F, compute the
00245    list of equivalences for the Tseitin translation */
00246 tseitin_trans_list_rel(F,prefix) := block(
00247   [l : length(F), v : tstr_var(prefix)],
00248   if l = 1 then [["equiv", [v], [F[1]]]]
00249   else block(
00250     [E : ["equiv", [v], cons(F[1],makelist([tstr_var(endcons(i-1,prefix))],i,2,l))]],
00251     return(
00252      cons(E, lappend(
00253       makelist(tseitin_trans_list_rel(F[i], endcons(i-1,prefix)),i,2,l))))))$00254 tseitin_trans_list(F) := tseitin_trans_list_rel(F,[])$
00255
00256 /* Compute the conjunction which represents the original formula */
00257 tseitin_trans_basic(F) := append(["and", [tstr_var([])]], tseitin_trans_list(F))$00258 00259 00260 /* ********** 00261 * Output * 00262 ********** 00263 */ 00264 00265 /* Translate operation-labels into latex-symbols */ 00266 trans_op_latex(string) := 00267 if string="not" then "\\neg" 00268 elseif string="impl" then "\\rightarrow" 00269 elseif string="equiv" then "\\leftrightarrow" 00270 elseif string="xor" then "\\oplus" 00271 elseif string="or" then "\\vee" 00272 elseif string="or" then "\\wedge" 00273 else string$
00274
00275 /* Output a formula tree st as latex-ps-tree to stream s */
00276 tex_ft(s,F) :=
00277   if length(F) = 1 then
00278     if not(atom(F[1])) and op(F[1]) = "not" then printf(s, "~a~a~a", "\\TR{$\\neg ", first(F[1]), "$}")
00279     else printf(s, "~a~a~a", "\\TR{$", F[1], "$}")
00280   else (
00281      printf(s, "~a~a~a", "\\pstree{\\TR{$", trans_op_latex(F[1]), "$}}"),
00282      printf(s, "{"),
00283      for i : 2 thru length(F) do tex_ft(s,F[i]),
00284      printf(s, "}")
00285   )$00286 00287 /* Output a formula tree st as latex-ps-tree to file with name n */ 00288 tex_ft_f(n, F) := (block[s : openw(n)], tex_ft(s, F), close(s))$
00289
00290