OKlibrary  0.2.1.6
PrimeImplicatesImplicants.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 27.3.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/TestSystem/Lisp/Asserts.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Backtracking/DLL_solvers.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00027 
00028 
00029 kill(f)$
00030 
00031 /* *****************
00032    * Prime clauses *
00033    *****************
00034 */
00035 
00036 okltest_prime_clauses_cs(f) := (
00037   assert(f({}) = {}),
00038   assert(f({{}}) = {{}}),
00039   assert(f({{},{1}}) = {{}}),
00040   assert(f({{1},{-1,2}}) = {{1},{2}}),
00041   assert(f({{1,2},{-2,3},{-1,3}}) = {{1,2},{3}}),
00042   assert(f({{1,2},{-2,3},{-1,3,4}}) = {{1,2},{1,3},{3,4},{-2,3}}),
00043   assert(okltest_min_2resolution_closure_cs(f) = true),
00044   true)$
00045 
00046 
00047 /* *************************************
00048    * Prime-clauses of full clause-sets *
00049    *************************************
00050 */
00051 
00052 okltest_min_2resolution_closure_cs(f) := (
00053   assert(f({}) = {}),
00054   assert(f({{}}) = {{}}),
00055   assert(f({{1}}) = {{1}}),
00056   assert(f({{1},{-1}}) = {{}}),
00057   assert(f({{1,2},{-1,-2}}) = {{1,2},{-1,-2}}),
00058   assert(f({{1,2,3},{1,-2,3},{-1,-2,-3}}) = {{1,3},{-1,-2,-3}}),
00059   for n : 0 thru 3 do
00060     assert(f(full_fcs(n)[2]) = {{}}),
00061   true)$
00062 
00063 
00064 /* ******************************************************
00065    * Minimum equivalent clause-sets of full clause-sets *
00066    ******************************************************
00067 */
00068 
00069 okltest_subsumption_hg_full_cs(f) := (
00070   /* XXX */
00071   true)$
00072 
00073 okltest_rsubsumption_hg_full_cs(f) := (
00074   assert(f({}) = [[{},{}],{}]),
00075   assert(f({{}}) = [[{},{}],{{}}]),
00076   assert(f({{1}}) = [[{},{}],{{1}}]),
00077   assert(f({{-1}}) = [[{},{}],{{-1}}]),
00078   assert(f({{1},{-1}}) = [[{},{}],{{}}]),
00079   /* XXX */
00080   true)$
00081 
00082 /* Testing whether f computes the set of all minimal CNF-representations
00083    (w.r.t. first the number of clauses, and then the number of literals)
00084    of a full CNF clause-set F:
00085 */
00086 okltest_minequiv_cs(f) := (
00087   assert(f({}) = {{}}),
00088   assert(f({{}}) = {{{}}}),
00089   assert(f({{1}}) = {{{1}}}),
00090   assert(f({{1},{-1}}) = {{{}}}),
00091   for n : 0 thru 5 do block([N : setn(n)],
00092     assert(f(singletons(N)) = {singletons(N)})),
00093   assert(f({{1,2},{-1,-2}}) = {{{1,2},{-1,-2}}}),
00094   assert(f({{1,2},{-2,1}}) = {{{1}}}),
00095   assert(f({{1,2},{-2,3}}) = {{{1,2},{-2,3}}}),
00096   /* XXX */
00097   true)$
00098 
00099 
00100 /* *************************************
00101    * Dualisation for full clause-sets  *
00102    *************************************
00103 */
00104 
00105 okltest_dual_min_2resolution_closure_cs(f) := (
00106   assert(f({}) = {{}}),
00107   assert(f({{}}) = {}),
00108   assert(f({{1}}) = {{1}}),
00109   assert(f({{-1}}) = {{-1}}),
00110   assert(f({{1},{-1}}) = {}),
00111   assert(f({{1,2}}) = {{1},{2}}),
00112   assert(f({{1,2},{-1,-2}}) = {{1,-2},{-1,2}}),
00113   assert(f({{1,2},{-1,-2},{-1,2}}) = {{-1,2}}),
00114   assert(f({{1,2},{-1,-2},{-1,2},{1,-2}}) = {}),
00115   assert(f({{1,2,3},{-1,-2,3},{-1,2,-3},{1,-2,-3}}) = {{1,2,3},{-1,-2,3},{-1,2,-3},{1,-2,-3}}),
00116   assert(f({{1,2,3},{-1,-2,3},{-1,2,-3},{1,-2,-3},{1,2,-3}}) = {{1,2,3},{-1,2,-3},{1,-2,-3}}),
00117   assert(f({{-3,-2,1},{-2,-1,3},{-1,2,3}}) = {{-3,-1},{-2,-1},{-2,3},{1,3}}),
00118   for n : 0 thru 3 do
00119     assert(f(full_fcs(n)[2]) = {}),
00120   true)$
00121 
00122 /* Testing whether f computes a repetition-free list of all minimal
00123    DNF-representations (w.r.t. first the number of clauses, and then the
00124    number of literals) of a full CNF clause-set F:
00125 */
00126 okltest_dual_minequiv_cs(f) := block([R],
00127   assert(f({}) = [{{}}]),
00128   assert(f({{}}) = [{}]),
00129   R : f({{-3,-2,1},{-2,-1,3},{-1,2,3}}),
00130   assert(length(R) = 2),
00131   assert(setify(R) = {{{-3,-1},{1,3},{-2,-1}}, {{-3,-1},{-2,3},{1,3}}}),
00132   /* XXX */
00133   true)$
00134 
00135 
00136 /* **************************************************
00137    * Finding contained prime-clauses by SAT solvers *
00138    **************************************************
00139 */
00140 
00141 okltest_contained_prime_implicate(f) := block(
00142  [S : lambda([F],dll_simplest_trivial1(cs_to_fcs(F)))],
00143   assert(f({{}},{},lambda([F],false)) = {}),
00144   assert(f({{}},{1,2,3},lambda([F],false)) = {}),
00145   for n : 1 thru 3 do block([F : full_fcs(n)[2]],
00146     assert(f(F, setn(n), S) = {})),
00147   assert(f({{1}}, {1,2}, S) = {1}),
00148   assert(f({{2}}, {1,2}, S) = {2}),
00149   for n : 1 thru 3 do block([F : disjoin(setn(n), full_fcs(n)[2])],
00150     assert(f(F, comp_sl(setn(n)), S) = {-1})),
00151   true)$
00152 
00153 okltest_replace_by_prime_implicates_hitting(f) := (
00154   assert(f({}) = {}),
00155   assert(f({{}}) = {{}}),
00156   assert(f({{1}}) = {{1}}),
00157   for n : 0 thru 3 do
00158     assert(f(full_fcs(n)[2]) = {{}}),
00159   assert(f({{1,2}}) = {{1,2}}),
00160   assert(f({{1,2},{-1,-2}}) = {{1,2},{-1,-2}}),
00161   true)$
00162 
00163