OKlibrary  0.2.1.6
Conflicts.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 12.2.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 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 
00022 oklib_include("OKlib/ComputerAlgebra/TestSystem/Lisp/Asserts.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/CombinatorialMatrices/Lisp/Basics.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Hypergraphs.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Pigeonhole.mac")$
00028 
00029 
00030 kill(f)$
00031 
00032 /* *****************
00033    * Constructions *
00034    *****************
00035 */
00036 
00037 okltest_cm_cs(f) := block([F,M],
00038   assert(scomequalp(f({}), emptyscom)),
00039   F : {{}}, M : f(F),
00040   assert(scomequalp(M, zeroscom(F))),
00041   block([alt_cm_cs : lambda([F], 
00042       scprod_scom(1/2, diff_scom(cl_varint_scom_cs(F), cl_int_scom_cs(F))))],
00043     for n : 0 thru (if oklib_test_level = 0 then 2 else 3) do 
00044      block([F : full_fcs(n)[2]],
00045       assert(scomequalp(f(F), alt_cm_cs(F))))),
00046   true)$
00047 
00048 okltest_cg_cs(f) := block([F,G],
00049   assert(f({}) = [{},{}]),
00050   assert(f({{}}) = [{{}},{}]),
00051   true)$
00052 
00053 
00054 /* ************
00055    * Measures *
00056    ************
00057 */
00058 
00059 okltest_nconflicts(f) := block(
00060   assert(f({}) = 0),
00061   assert(f({{}}) = 0),
00062   assert(f({{1},{-1}}) = 1),
00063   assert(f({{1,2},{-1,-2}}) = 2),
00064   for n : 0 thru 4 do
00065     assert(f(uniform_usat_hitting_max(n)) = n/4 * 4^n),
00066   for n : 0 thru 4 do
00067     assert(f(uniform_usat_hitting_min(n)) = 1/2 * (4^n - 2^n)),
00068   true)$
00069 
00070 okltest_rnconflicts(f) := block(
00071   assert(f({}) = 0),
00072   assert(f({{}}) = 0),
00073   assert(f({{1},{-1}}) = 1),
00074   assert(f({{1,2},{-1,-2}}) = 1),
00075   for n : 0 thru 4 do
00076     assert(f(uniform_usat_hitting_max(n)) = binomial(2^n,2)),
00077   for n : 0 thru 4 do
00078     assert(f(uniform_usat_hitting_min(n)) = binomial(2^n,2)),
00079   true)$
00080 
00081 
00082 /* Tests whether f computes the hermitian rank of a clause-set. */
00083 okltest_hermitian_rank_cs(f) := block(
00084   assert(f({}) = 0),
00085   assert(f({{}}) = 0),
00086   assert(f({{1}}) = 0),
00087   assert(f({{1},{-1}}) = 1),
00088   for k : 1 thru 3 do block([F : uniform_usat_hitting_min(k)],
00089     assert(f(F) = 2^k-1),
00090     assert(f(adjoin({},F)) = 2^k-1)
00091   ),
00092   assert(f(weak_php_cs(3,2)) = 3),
00093   if oklib_test_level = 0 then return(true),
00094   for k : 4 thru 5 do
00095     assert(f(uniform_usat_hitting_min(k)) = 2^k - 1),
00096   true)$
00097 
00098 okltest_hermitian_rank_cs_h(f) := block(
00099   assert(okltest_hermitian_rank_cs(buildq([f],lambda([F],f(F,hermitian_rank))))),
00100   assert(okltest_hermitian_rank_cs(buildq([f],lambda([F],f(F,hermitian_rank_charpoly))))),
00101   if oklib_test_level >= 1 then block([oklib_test_level : oklib_test_level-1],
00102     assert(okltest_hermitian_rank_cs(buildq([f],lambda([F],f(F,hermitian_rank_eig)))))
00103   ),
00104   true)$
00105 
00106 /* Tests whether f computes the characteristic polynomial of a clause-set. */
00107 okltest_charpoly_cs(f) := block(
00108   assert(f({}) = 0),
00109   assert(f({{}}) = x),
00110   assert(f({{1}}) = x),
00111   assert(f({{1},{2}}) = x^2),
00112   assert(f({{1},{2},{3}}) = x^3),
00113   assert(f({{-1},{1}}) = x^2 - 1),
00114   true)$
00115 
00116 
00117 /* Tests whether f computes the conflict-partition-number of a clause-set
00118    (the minimal number of hitting sets partitioning the clause-set) */
00119 okltest_partition_number_cs(f) := block(
00120   assert(f({}) = 0),
00121   assert(f({{}}) = 1),
00122   assert(f({{1}}) = 1),
00123   assert(f({{1},{-1}}) = 1),
00124   assert(f({{1},{2}}) = 2),
00125   for k : 0 thru 3 do (
00126     assert(f(uniform_usat_hitting_min(k)) = 1),
00127     assert(f(uniform_usat_hitting_max(k)) = 1),
00128     assert(f(smusat_horn_cs(k)) = 1)),
00129   assert(f(sasg2000[2]) = 1),
00130 true)$
00131 
00132 
00133 /* *********
00134    * Tests *
00135    *********
00136 */
00137 
00138 okltest_graphiccsp(f) := block(
00139   assert(f({}) = true),
00140   assert(f({{}}) = true),
00141   assert(f({{1}}) = true),
00142   assert(f({{1},{-1}}) = true),
00143   assert(f({{},{1}}) = true),
00144   assert(f({{1,2},{-1,-2}}) = false),
00145   true);
00146 
00147 okltest_alon_saks_cs(f) := block(
00148   assert(f({}) = [true,true,0,1,1]),
00149   assert(f({{}}) = [true,true,1,1,1]),
00150   assert(f({{1},{-1}}) = [true,true,2,2,2]),
00151   assert(f({{1,2},{-1,-2}}) = unknown),
00152   true);
00153