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