OKlibrary  0.2.1.6
Basics.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 21.5.2010 (Swansea) */
00002 /* Copyright 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/DataStructures/Lisp/Lists.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/PartialAssignments.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/Basics.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Resolution/Basics.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Backtracking/DLL_solvers.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00028 
00029 
00030 /*
00031   See "Notions" in Satisfiability/Lisp/Primality/plans/general.hpp for
00032   the definitions.
00033 */
00034 
00035 prime_clause_p(C,F) := impliesp_cs(F,C,current_satsolver) and
00036  every_s(lambda([x], not impliesp_cs(F,disjoin(x,C),current_satsolver)), C)$
00037 
00038 dual_prime_clause_p(C,F) := sat_pacs_p(C,F) and 
00039  every_s(lambda([x], not sat_pacs_p(disjoin(x,C),F)), C)$
00040 
00041 prime_cs_p(F) := every_s(lambda([C], prime_clause_p(C,F)), F)$
00042 
00043 maximal_prime_cs_p(F) := prime_cs_p(F) and 
00044  min_elements(union(F,resolvents_cs(F))) = F$
00045