OKlibrary  0.2.1.6
HittingProofSystem.mac
Go to the documentation of this file.
```00001 /* Oliver Kullmann, 21.2.2012 (Swansea) */
00002 /* Copyright 2012 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/Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac")\$
00024 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")\$
00025
00026
00027 /* ****************************************
00028    * The notion of a "hitting refutation" *
00029    ****************************************
00030 */
00031
00032 /* Checking that G is a hitting refutation of clause-set F: */
00033 hitref_csp(F,G) := cs_p(G) and hittingcsp(G) and
00034  sat_decision_hitting_cs(G)=false and rl_subsetp(F,G)\$
00035
00036
00037 /* ********************************************
00038    * Hitting refutations from splitting trees *
00039    ********************************************
00040 */
00041
00042 /* For an unsatisfiable (boolean) clause-set F and a splitting tree T for F,
00043    compute a hitting refutation of F (see
00044    Satisfiability/Lisp/ConflictCombinatorics/testobjects/HittingProofSystem.mac
00045    ), using the heuristics _heu:
00046    _heu(C,F) is applied in case {C,C+{x},C+{-x}} <= F, and if true, then
00047    C is chosen, if false, then C+{x},C+{-x} are chosen.
00048    sp_p(T,F) must hold true.
00049 */
00050 stcs2hitref(F,T,_heu) := if T=[false] then {{}}
00051 else block([x,T0,T1,F0,F1,I,Ic,Ir],
00052  [x,T0,T1] : T,
00053  F0 : stcs2hitref(apply_pa_cs({-x},F), T0, _heu),
00054  F1 : stcs2hitref(apply_pa_cs({x},F), T1, _heu),
00055  I : intersection(F0,F1,F),
00057  Ir : subset(Ic, lambda([C], not _heu(C,F))),
00058  I : setdifference(I,Ir),
00059  union(I,