OKlibrary  0.2.1.6
Conditions.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 24.4.2009 (Swansea) */
00002 /* Copyright 2009 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/NonBoolean.mac")$
00023 
00024 
00025 /* ***********
00026    * Notions *
00027    ***********
00028 */
00029 
00030 /*
00031  A "condition" is a pair [V,e], where V is a set of "variables", and
00032  e is a function such that for every function f(x) with f(v) in {0,1}
00033  for all v in V we have e(f) in {0,1}.
00034  Abbrv: "cdn"
00035  Question: Should this be "false, true" instead of "0, 1" ?!
00036 */
00037 
00038 /*
00039  A "positive boolean constraint" is a pair [V,G], such that [V,G] is a full
00040  formal clause-set, with the meaning of presenting the underlying
00041  conditions as a DNF.
00042  A "negative boolean constraint" is a pair [V,F], such that [V,F] is a full
00043  formal clause-set, with the meaning of representing the underlying
00044  condition as a CNF.
00045  Abbrv: "pbcst, nbcst"
00046 */
00047 
00048 /*
00049  A "positive constraint" is a pair [V,G], such that [V,G] is a full
00050  formal non-boolean clause-set over V, with the meaning of presenting the 
00051  underlying condition as a DNF.
00052  A "negative constraint" is a pair [V,F], such that [V,F] is a full 
00053  formal non-boolean clause-set over V, with the meaning of presenting the 
00054  underlying condition as a CNF.
00055  Abbrv: "pcst", "ncst"
00056 */
00057 
00058 /*
00059  A "positive boolean DNF-constraint" resp. a "negative boolean CNF-constraint"
00060  allows more generally arbitrary clause-sets (not just full clause-sets).
00061  Abbrv: "pbdnfcst", "nbcnfcst"
00062 */
00063 
00064 /*
00065  And a "positive DNF-constraint" resp. a "negative CNF-constraint" allows
00066  arbitrary non-boolean clause-sets.
00067  Abbrv: "pdnfcst", "ncnfcst"
00068 */
00069 
00070 
00071 /* ***************
00072    * Conversions *
00073    ***************
00074 */
00075 
00076 /* false -> 0, true -> 1: */
00077 mb2b(x) := if x then 1 else 0;
00078 
00079 
00080 /* ****************
00081    * Translations *
00082    ****************
00083 */
00084 
00085 snbl2cdn(x) := block([v:var_snbl(x), e:val_snbl(x), s:sgn_snbl(x), t, ta],
00086  t : if s=+1 then buildq([v,e],mb2b(is(ta(v)=e))) 
00087   elseif s=-1 then buildq([v,e],mb2b(is(ta(v)#e))) else
00088   buildq([s,v,e],mb2b(
00089     if s=+1 then is(ta(v)=e) elseif s=-1 then is(ta(v)#e) else unknown)),
00090  return([{v}, buildq([t], lambda([ta],t))]))$
00091