OKlibrary  0.2.1.6
Basics.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 28.12.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/Hypergraphs/Lisp/SetSystems.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00024 
00025 
00026 /* *****************************
00027    * The notion of a reduction *
00028    *****************************
00029 */
00030 
00031 /* 
00032   A "reduction" for CNF clause-sets (and its variations) is a map
00033   r: CLS -> CLS such that for all F in CLS, r(F) is satisfiability
00034   equivalent to F
00035 */
00036 
00037 weakest_reduction_cs(F) := F$
00038 /* Taking a SAT solver S as parameter (which returns true of false): */
00039 strongest_reduction_cs(F,S_) := if S_(cs2fcs(F)) then {} else {{}}$
00040 
00041 
00042 /* ***************************
00043    * Subsumption elimination *
00044    ***************************
00045 */
00046 
00047 /* Removes all subsumed clauses from clause-set F: */
00048 subsumption_elimination_cs(F) := min_elements(F)$
00049