OKlibrary  0.2.1.6
HittingClauseSets.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 12.2.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2010, 2011, 2012, 2013 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 
00021 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac")$
00022 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/tests/HittingClauseSets.mac")$
00023 
00024 /* *******************
00025    * Representations *
00026    *******************
00027 */
00028 
00029 okltest_hitting_cls_rep_st(hitting_cls_rep_st);
00030 
00031 /* **************
00032    * Generators *
00033    **************
00034 */
00035 
00036 okltest_uniform_usat_hitting_min(uniform_usat_hitting_min);
00037 
00038 okltest_over_full_hitting_fcs(over_full_hitting_fcs);
00039 
00040 okltest_smusat_horn_cs(smusat_horn_cs);
00041 okltest_smusat_horn_stdfcl(smusat_horn_stdfcl);
00042 okltest_smusat_horn_stdfcs(smusat_horn_stdfcs);
00043 okltest_nvar_smusat_horn(nvar_smusat_horn);
00044 okltest_ncl_smusat_horn(ncl_smusat_horn);
00045 okltest_ncl_list_smusat_horn(ncl_list_smusat_horn);
00046 okltest_nlitocc_smusat_horn(nlitocc_smusat_horn);
00047 okltest_smusat_genhorn_cs(smusat_genhorn_cs);
00048 okltest_sat_genhorn_cs(sat_genhorn_cs);
00049 okltest_ext1_sat_genhorn_cs(ext1_sat_genhorn_cs);
00050 
00051 okltest_sasg2000(sasg2000);
00052 okltest_brouwer1999(brouwer1999);
00053 
00054 okltest_max_var_hitting_def(max_var_hitting_def);
00055 okltest_nvar_max_var_hitting_def(nvar_max_var_hitting_def);
00056 okltest_max_var_hittingdef2_cs(max_var_hittingdef2_cs);
00057 
00058 okltest_all_hitting_extensions_k_fcs(all_hitting_extensions_k_fcs);
00059 okltest_all_reps_hitting_extensions_k_fcs(all_reps_hitting_extensions_k_fcs);
00060 
00061 /* *********
00062    * Tests *
00063    *********
00064 */
00065 
00066 okltest_sat_decision_hitting_cs(sat_decision_hitting_cs);
00067 
00068 okltest_hittingcsp(hittingcsp);
00069 okltest_hitting1rcsp(hitting1rcsp);
00070 okltest_treehittingcsp(treehittingcsp);
00071 
00072 okltest_check_hitting_nsing_def(check_hitting_nsing_def);
00073 
00074 /* **************************************************************
00075    * Necessary conditions for unsatisfiable hitting clause-sets *
00076    **************************************************************
00077 */
00078 
00079 okltest_all_cld_uhit(all_cld_uhit);
00080 okltest_all_cld_uhit_minvd(all_cld_uhit_minvd);
00081 okltest_all_cld_uhit_maxminvd(all_cld_uhit_maxminvd);
00082 
00083 /* ****************************************************
00084    * Representing clause-sets via hitting clause-sets *
00085    ****************************************************
00086 */
00087 
00088 okltest_hitting_decomposition_m_cs(hitting_decomposition_m_cs);
00089 
00090 /* ********************************************************************
00091    * Finding hitting clause-sets with given deficiency "sporadically" *
00092    ********************************************************************
00093 */
00094 
00095 okltest_all_hittinginstances_def(all_hittinginstances_def);
00096 
00097 okltest_all_hitting_DP_reductions_def(all_hitting_DP_reductions_def);
00098 
00099 /* ********************************************************************
00100    * Finding hitting clause-sets with given deficiency systematically *
00101    ********************************************************************
00102 */
00103 
00104 okltest_derived_hitting_cs(derived_hitting_cs);
00105 okltest_derived_hitting_cs_pred(derived_hitting_cs_pred);
00106 okltest_derived_hitting_cs_nsing(derived_hitting_cs_nsing);
00107 okltest_all_derived_hitting_cs_nsing_isoelim(all_derived_hitting_cs_nsing_isoelim);
00108 
00109 /* no specific testing of derived_hitting_cs_pred_isoelim yet,
00110    since the general test is not applicable, since it assumes that all
00111    derived clause-sets are computed, while with isoelim some
00112    isomorphic copies will be removed: */
00113 /* okltest_derived_hitting_cs_pred(derived_hitting_cs_pred_isoelim); */
00114 /* okltest_derived_hitting_cs_nsing(derived_hitting_cs_nsing_isoelim); */
00115 
00116 okltest_all_unsinghitting_def(all_unsinghitting_def);
00117 
00118 /* ***********************************************************
00119    * Finding hitting clause-sets with given n systematically *
00120    ***********************************************************
00121 */
00122 
00123 okltest_all_unsinghitting(all_unsinghitting);
00124 okltest_all_unsinghitting(all_unsinghitting_mvd);
00125 
00126 /* ***************************
00127    * Maximal min-var-degrees *
00128    ***************************
00129 */
00130 
00131 okltest_max_min_var_deg_uhit_def(max_min_var_deg_uhit_def);
00132 
00133 /* *************************
00134    * Resolution complexity *
00135    *************************
00136 */
00137 
00138 okltest_min_nssplittree_isot(min_nssplittree_isot);
00139 if oklib_test_level >= 1 then (
00140   oklib_load("OKlib/ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac"),
00141   okltest_min_nssplittree_def(min_nssplittree_def)
00142 )
00143 else true;
00144 
00145 /* ****************************
00146    * Primes and factorisation *
00147    ****************************
00148 */
00149 
00150 okltest_primeuhitting_p(primeuhitting_p);
00151