OKlibrary  0.2.1.6
Cores.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 8.4.2008 (Swansea) */
00002 /* Copyright 2008 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/MinimalUnsatisfiability/Cores.mac")$
00022 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/MinimalUnsatisfiability/tests/Cores.mac")$
00023 
00024 /* *************************************************
00025    * Minimally unsatisfiable cores of minimum size *
00026    *************************************************
00027 */
00028 
00029 okltest_min_size_mus(min_size_mus_bydef);
00030 
00031 okltest_contains_us(contains_us_bydef);
00032 
00033 /* ***********************************
00034    * Computing all irredundant cores *
00035    ***********************************
00036 */
00037 
00038 okltest_all_irr_cores(all_irr_cores_bydef);
00039 okltest_all_min_usat_cores(all_min_usat_cores_bydef);
00040 okltest_all_forced_irr_cores(all_forced_irr_cores_bydef);
00041 
00042 /* *************************************************
00043    * Heuristical search for some irredundant cores *
00044    *************************************************
00045 */
00046 
00047 okltest_first_mus_fcs(first_mus_fcs);
00048 
00049 okltest_first_irr_fcs(first_irr_fcs);
00050 
00051 /* *********************************
00052    * Sampling of irredundant cores *
00053    *********************************
00054 */
00055 
00056 okltest_sample_irr_cores(sample_irr_cores);
00057 
00058 /* ********************************************
00059    * Maximally non-equivalent sub-clause-sets *
00060    ********************************************
00061 */
00062 
00063 okltest_all_max_noneq_scs(all_max_noneq_scs_bydef);
00064 okltest_all_max_sat_scs(all_max_sat_scs_bydef);
00065 okltest_equivalence_checker_scl(equivalence_checker_scl_bydef);
00066 okltest_all_max_neq_scs(all_max_neq_scs_bydef);
00067 
00068 /* ************************************
00069    * Duality between MAXSAT and MUSAT *
00070    ************************************
00071 */
00072 
00073 okltest_all_max_neq_scs_bydual(all_max_neq_scs_bydual);
00074 okltest_all_irr_cores_bydual(all_irr_cores_bydual);
00075