OKlibrary  0.2.1.6
Deficiency2.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 31.5.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 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/Hypergraphs/Lisp/SetSystems.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Reductions/DP-Reductions.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Substitutions.mac")$
00026 /* Below further files are included (delayed, due to circularity-problems). */
00027 
00028 
00029 /* *********************************************************************
00030    * The saturated minimally unsatisfiable clause-sets of deficiency 2 *
00031    *********************************************************************
00032 */
00033 
00034 /* Standard clauses: */
00035 pos_c(n) := setn(n)$
00036 neg_c(n) := setmn(-n,-1)$
00037 imp_c(i,n) := if i < n then {-i,i+1} else {-n,1}$
00038 
00039 /* The standard MUSAT(def=2) non-singular formal clause-sets (where every
00040    literal occurs at least twice) for n >= 2: */
00041 musatd2_cl(n) := append([pos_c(n),neg_c(n)], create_list(imp_c(i,n),i,1,n))$
00042 musatd2_cs(n) := cl2cs(musatd2_cl(n))$
00043 musatd2_fcl(n) := [create_list(i,i,1,n), musatd2_cl(n)]$
00044 musatd2_fcs(n) := fcl2fcs(musatd2_fcl(n))$
00045 /* Statistics: */
00046 nvar_musatd2(n) := n$
00047 ncl_musatd2(n) := n+2$
00048 ncl_list_musatd2(n) := if n=2 then [[2,4]] else
00049  [[2,n],[n,2]]$
00050 nlitocc_musatd2(n) := n*4$
00051 
00052 
00053 
00054 /* *****************************************************
00055    * Unsatisfiable hitting clause-sets of deficiency 2 *
00056    *****************************************************
00057 */
00058 
00059 /* These includes need to be delayed, since data/uhit_def.mac uses musatd2_fcs:
00060 */
00061 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac")$
00062 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/data/uhit_def.mac")$
00063 
00064 /* Every unsatisfiable hitting clause-set F of deficiency 2 is either of
00065    type 2 or type 3, depending on whether elimination of singular variables
00066    yields a clause-set isomorphic to musatd2_fcs(2) or musatd2_fcs(3).
00067 */
00068 
00069 /* Returns 2, 3 or false, where false results iff F is not an unsatisfiable 
00070    hitting clause-set of deficiency 2, while otherwise its type is returned:
00071 */
00072 hittingtype_d2_cs(F) := block([F : sdp_reduction_cs(F), T],
00073  T : classify_candidates_uhit_def([F])[1],
00074  if T=false or T[2]="new" or T[1][1]#2 then false
00075  else T[1][2])$
00076 
00077 /* The set of all isomorphism-types (i.e., representatives) of unsatisfiable 
00078    formal hitting clause-sets of deficiency 2 of type t in {2,3} with 
00079    n variables (where n is an integer):
00080 */
00081 all_reps_uhitd2_t_fcs(t,n) :=
00082  all_reps_hitting_extensions_k_fcs({musatd2_fcs(t)},n-t)$
00083 
00084 /*The set of all isomorphism-types (i.e., representatives) of unsatisfiable 
00085    formal hitting clause-sets of deficiency 2 with n variables (with 
00086    standardised variable names):
00087 */
00088 all_reps_uhitd2_fcs(n) :=
00089  union(all_reps_uhitd2_t_fcs(2,n), all_reps_uhitd2_t_fcs(3,n))$
00090 
00091 /* All unsatisfiable formal hitting clause-sets of deficiency 2 with
00092    n variables (standardised):
00093 */
00094 all_uhitd2_fcs(n) := lunion(map(all_renamings_fcs,all_reps_uhitd2_fcs(n)))$
00095 
00096