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),
00056  Ic : subset(I, lambda([C], subsetp({adjoin(x,C),adjoin(-x,C)}, F))),
00057  Ir : subset(Ic, lambda([C], not _heu(C,F))),
00058  I : setdifference(I,Ir),
00059  union(I,
00060        add_element(x,Ir), add_element(-x,Ir),
00061        add_element(x,setdifference(F0,I)), add_element(-x,setdifference(F1,I))
00062  ))$
00063 /*
00064  Remark: we have hitref_csp(F,stcs2hitref(F,T,_heu)) = true.
00065 */
00066 /* Chosing always the smaller clauses: */
00067 stcs2hitref0(F,T) := stcs2hitref(F,T,lambda([C,F],true))$
00068 /* Chosing always the larger clauses: */
00069 stcs2hitref1(F,T) := stcs2hitref(F,T,lambda([C,F],false))$
00070 
00071