OKlibrary  0.2.1.6
DLL_solvers.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 17.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/Satisfiability/Lisp/Generators/Pigeonhole.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Counting/InclusionExclusion.mac")$
00025 
00026 
00027 kill(f)$
00028 
00029 /* ********************************
00030    * Generic test for SAT solvers *
00031    ********************************
00032 */
00033 
00034 /* Input is (just) a formal clause-set. */
00035 
00036 /* Just returning true/false: */
00037 okltest_SATsolver(f) := block(
00038   assert(f([{},{}]) = true),
00039   assert(f([{},{{}}]) = false),
00040   assert(f([{1},{}]) = true),
00041   assert(f([{1},{{}}]) = false),
00042   assert(f([{1},{{1}}]) = true),
00043   assert(f([{1},{{1},{-1}}]) = false),
00044   for n : 0 thru 3 do
00045     assert(f(full_fcs(n)) = false),
00046   for n : 0 thru 3 do (
00047     assert(f(weak_php_fcs(n,n)) = true),
00048     assert(f(weak_php_fcs(n+1,n)) = false)
00049   ),
00050   true)$
00051 
00052 /* Instead of "true" a satisfying partial assignment is returned: */
00053 okltest_SATsolver_spa(f) := block(
00054   assert(okltest_SATsolver(buildq([f],lambda([FF],block([res:f(FF)],
00055     if setp(res) then true else false))))),
00056   assert(f([{},{}]) = {}),
00057   assert(f([{1},{{1}}]) = {1}),
00058   assert(f([{1,2},{{1,2},{1,-2},{-1,2}}]) = {1,2}),
00059   true)$
00060 
00061 /* **********************************
00062    * Backtracking without reduction *
00063    **********************************
00064 */
00065 
00066 okltest_dll_simplest(f) := block(
00067   okltest_SATsolver(buildq([f],lambda([FF],f(FF,dll_heuristics_first_formal)))),
00068   true)$
00069 
00070 okltest_dll_simplest_spa(f) := block(
00071   okltest_SATsolver_spa(buildq([f],lambda([FF],f(FF,dll_heuristics_first_formal)))),
00072   true)$
00073 
00074 
00075 /* ***********************************
00076    * Backtracking with r_k-reduction *
00077    ***********************************
00078 */
00079 
00080 
00081 /* *****************************************
00082    * Backtracking with arbitrary reduction *
00083    *****************************************
00084 */
00085 
00086 
00087 /* *******************************
00088    * Simple heuristics for DLL   *
00089    *******************************
00090 */
00091 
00092 okltest_choose_most_sat_literal_h(f) := (
00093   block([h : f(lambda([FF], 1))],
00094    assert(h([{1},{}]) = -1),
00095    assert(h([{1},{{}}]) = -1),
00096    assert(h([{1,2},{{}}]) = -2),
00097    assert(h([{1,2},{{1,2}}]) = -2)
00098   ),
00099   block([h : f(lambda([FF],satprob_mcind_trrs(FF[2])))],
00100    assert(h([{1},{}]) = -1),
00101    assert(h([{1},{{}}]) = -1),
00102    assert(h([{1,2},{{}}]) = -2),
00103    assert(h([{1,2},{{1,2}}]) = 1),
00104    assert(h([{1,2},{{1},{1,2}}]) = 1)
00105   ),
00106   true)$
00107 
00108 okltest_johnson_heuristic(f) := (
00109   assert(f([{1},{}]) = -1),
00110   assert(f([{1},{{}}]) = -1),
00111   assert(f([{1},{{1}}]) = 1),
00112   assert(f([{1},{{1},{-1}}]) = -1),
00113   assert(f([{1,2},{{1,2},{1}}]) = 1),
00114   true)$
00115 
00116 okltest_dll_heuristics_max_lit_tb(f) := block(
00117   for n : 0 thru 3 do
00118     for m : 0 thru 3 do
00119       assert(f(n,m)(cs_to_fcs({{1,2},{1},{1,2,3}})) = 1),
00120   for n : 1 thru 3 do
00121     for m : 2 thru 3 do
00122       assert(not f(n,m)(cs_to_fcs({{-1,-2,-3},{1,-2,-3},{1,2,3}})) = 1),
00123 true)$
00124 
00125 
00126 /* ****************************
00127    * Heuristics via distances *
00128    ****************************
00129 */
00130 
00131 okltest_ast2tbt(f) := block([L,i,x],
00132   assert(f([L],i) = [L]),
00133   assert(f([[x,[[1,2]]], [L], [L]], 1) = [ [1,2], [L], [L] ]),
00134   assert(f([[x,[[3,8],[4,5]]], [L], [L]], 2) = [ [4,5], [L],[L]]),
00135   assert(f([[x,[[3,8],[4,5]]], [[x,[[1,2],[55,66]]], [L], [false]], [true]], 1) = [ [3,8], [[1,2],[L],[false]], [true] ]),
00136   true)$
00137 
00138 okltest_check_inf_branches_ast(f) := block([L,x,m,d],
00139   assert(f([L],m) = []),
00140   assert(f([[x, [[inf,d],[d,inf]]], [L], [L]], 0) = false),
00141   assert(f([[x, [[inf,d],[d,inf]]], [L], [L]], 1) = []),
00142   assert(f([[x, [[d,d]]], [L], [L]],0) = []),
00143   assert(f([[x, [[d,inf]]], [L], [[x,[[d,d]]], [L],[L]]],0) = [[x,[[d,inf]]], [2], 3]),
00144   assert(f([[x, [[inf,inf]]], [L], [[x,[[d,d]]], [L],[L]]],0) = [[x,[[inf,inf]]], [1,2], 1, 3]),
00145   assert(f([[[x],[[d,d]]], [[x,[[inf,d]]], [[x,[[d,d]]],[L],[L]],[L]], [[x,[[d,inf]]], [L],[[x,[[inf,inf]]],[L],[L]]]], 0) = [[x,[[inf,d]]],[1],3, [x,[[d,inf]]],[2],3]),
00146   /* XXX */
00147   true)$
00148 
00149 okltest_collapse_inf_branches_ast(f) := block([L,L1,L2,m,x],
00150   assert(f([L],m) = [L]),
00151   assert(f([ [x,[[d,d]]], [L],[L]], 0) = [ [x,[[d,d]]], [L],[L]]),
00152   assert(f([ [x,[[inf,d]]], [L1],[L2]], 0) = [L2]),
00153   assert(f([ [x,[[inf,d],[d,inf]]], [L1],[L2]], 1) = [L2]),
00154   assert(f([ [x,[[inf,d]]], [L], [[x,[[d,inf]]], [L1],[L2]]], 0) = [L1]),
00155   assert(f([ [x,[[d,d]]], [L], [[x,[[d,inf]]], [L1],[L2]]], 0) = [ [x,[[d,d]]], [L], [L1]]),
00156   /* XXX */
00157   true)$
00158 
00159 
00160 /* *************
00161    * Distances *    
00162    *************
00163 */
00164 
00165 
00166 /* ***************
00167    * Projections *
00168    ***************
00169 */
00170 
00171 
00172 /* *********************************
00173    * Satisfiability approximations *
00174    *********************************
00175 */
00176 
00177 okltest_locallemma_satapprox(f) := block(
00178   assert(f({}) = inf),
00179   assert(f({{}}) = minf),
00180   assert(f({{1}}) = inf),
00181   assert(f({{1},{2}}) = inf),
00182   assert(f({{},{1},{2}}) = minf),
00183   assert(f({{1},{-1}}) = 2),
00184   assert(f({{1,2}}) = inf),
00185   assert(f({{1,2},{-1,2}}) = inf),
00186   assert(f({{1,2},{-1,2},{1,-2}}) = 2),
00187   assert(f({{1,2},{-1,2},{1,-2},{-1,-2}}) = 4/3),
00188   assert(f({{1,2,3}}) = inf),
00189   assert(f({{1,2,3},{-1,2,3}}) = inf),
00190   assert(f({{1,2,3},{-1,2,3},{1,-2,3}}) = inf),
00191   assert(f({{1,2,3},{-1,2,3},{1,-2,3},{1,2,-3}}) = 8/3),
00192   assert(f({{-1,-2,-3,-4},{1,4},{2,4},{3,4}}) = 4/3),
00193   for n : 0 thru 4 do
00194     assert(f(full_fcs(n)[2]) = if n = 0 then minf else  1 / ((2^n - 1) * 2^(-n))),
00195   true)$
00196 
00197 okltest_locallemmasum_satapprox(f) := block(
00198   /* XXX */
00199   true)$
00200