OKlibrary  0.2.1.6
FundamentsBranchingHeuristics.dem
Go to the documentation of this file.
00001 /* Oliver Kullmann, 21.1.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 
00026 if oklib_test_demos then
00027  if oklib_test_demos_level < 3 then return()$
00028 
00029 oklib_include("OKlib/ComputerAlgebra/Trees/Lisp/Basics.mac")$
00030 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/BranchingTuples/Basic.mac")$
00031 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/BranchingTuples/Trees.mac")$
00032 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Backtracking/DLL_solvers.mac")$
00033 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Reductions/GeneralisedUCP.mac")$
00034 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Backtracking/OKsolver2002.mac")$
00035 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Pigeonhole.mac")$
00036 oklib_include("OKlib/ComputerAlgebra/Numerical/Lisp/Minimisation.mac")$
00037 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Counting/RandomClauseSets.mac")$
00038 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ConflictCombinatorics/Conflicts.mac")$
00039 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Counting/InclusionExclusion.mac")$
00040 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Hypergraphs.mac")$
00041 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/HashMaps.mac")$
00042 
00043 oklib_include("OKlib/ComputerAlgebra/TestSystem/Lisp/Asserts.mac")$
00044 
00045 
00046 /* **************************************
00047    * Section "A theoretical framework"  *
00048    **************************************
00049 */
00050 
00051 /* Example 1.2.1 */
00052 
00053 for i : -10 thru 10 do print(i,": ", fib(i));
00054 golden_section : solve(x^2=x+1,x);
00055 gs_neg : rhs(golden_section[1]);
00056 gs_pos : rhs(golden_section[2]);
00057 fib_formula(n) := 1/sqrt(5) * (gs_pos^n - gs_neg^n);
00058 for i : -10 thru 10 do print(i,": ", float(fib_formula(i)));
00059 /* round(1/2) = 0, round(3/2) = 2 */
00060 round_cautious(x) := block([fx : floor(x), s],
00061   s : sign(x - fx - 1/2),
00062   if s = zero then error("Ambiguous rounding for ", x)
00063   else if s = pos then fx + 1 else fx)$
00064 for i : 0 thru 10 do
00065   print(i,": ", float(round_cautious(1/sqrt(5) *  gs_pos^i)));
00066 
00067 
00068 /* ************************************************************
00069    * Section "Branching tuples and the canonical projection"  *
00070    ************************************************************
00071 */
00072 
00073 /* Example 1.3.1 */
00074 
00075 append([3,4],[3,2,1]);
00076 bt_composition([3,4],[3,2,1]);
00077 
00078 /* Example 1.3.2 */
00079 
00080 tau_symbolical([1,2]);
00081 tau([1,2]);
00082 tau_hp([1,2],40);
00083 tau_symbolical([2,3,5]);
00084 tau([2,3,5]);
00085 tau_hp([2,3,5],100);
00086 
00087 /* **************************************************************************
00088    * Section "Associating probability distributions with branching tuples"  *
00089    **************************************************************************
00090 */
00091 
00092 /* Example 1.3.3 */
00093 
00094 tauprob([1,2]);
00095 tauprob_symbolical([1,2]);
00096 factor(expand(tauprob_symbolical([1,2])));
00097 tauprob_hp([1,2],40);
00098 tauprob([2,3,5]);
00099 
00100 
00101 /* ***********************************
00102    * Section "Estimating tree sizes  *
00103    ***********************************
00104 */
00105 
00106 /* Example 1.4.1 */
00107 
00108 T_1 : [[[],[]],[]];
00109 T_2 : [[[]]];
00110 T_3 : [[],[],[[],[]]];
00111 
00112 nds(T_1);
00113 lvs(T_1);
00114 nnds(T_1);
00115 nlvs(T_1);
00116 height(T_1);
00117 nds(T_2);
00118 lvs(T_2);
00119 nnds(T_2);
00120 nlvs(T_2);
00121 height(T_2);
00122 nds(T_3);
00123 lvs(T_3);
00124 nnds(T_3);
00125 nlvs(T_3);
00126 height(T_3);
00127 
00128 dst(T_3,[3]);
00129 
00130 lvs(subtree(T_3,[3]));
00131 
00132 
00133 /* Example 1.4.2 */
00134 
00135 T_1_utpd : uniform_tpd(T_1);
00136 T_2_utpd : uniform_tpd(T_2);
00137 T_3_utpd : uniform_tpd(T_3);
00138 
00139 tpd_flatten(T_1_utpd);
00140 tpd_flatten(T_2_utpd);
00141 tpd_flatten(T_3_utpd);
00142 
00143 hm2sm(ipd_rp(T_1_utpd));
00144 hm2sm(ipd_rp(T_2_utpd));
00145 hm2sm(ipd_rp(T_3_utpd));
00146 
00147 lower_bound_nlvs(T_1_utpd);
00148 tpd_moment(T_1_utpd,1);
00149 upper_bound_nlvs(T_1_utpd);
00150 
00151 lower_bound_nlvs(T_2_utpd);
00152 tpd_moment(T_2_utpd,1);
00153 upper_bound_nlvs(T_2_utpd);
00154 
00155 lower_bound_nlvs(T_3_utpd);
00156 tpd_moment(T_3_utpd,1);
00157 upper_bound_nlvs(T_3_utpd);
00158 
00159 
00160 /* Example 1.4.3 */
00161 
00162 T_1_ctpd : canonical_tpd(T_1)[1];
00163 T_2_ctpd : canonical_tpd(T_2)[1];
00164 T_3_ctpd : canonical_tpd(T_3)[1];
00165 
00166 tpd_flatten(T_1_ctpd);
00167 tpd_flatten(T_2_ctpd);
00168 tpd_flatten(T_3_ctpd);
00169 
00170 
00171 /* Example 1.4.4 */
00172 
00173 tpd_moment(T_1_utpd,2);
00174 tpd_variance(T_1_utpd);
00175 
00176 tpd_moment(T_2_utpd,2);
00177 tpd_variance(T_2_utpd);
00178 
00179 tpd_moment(T_3_utpd,2);
00180 tpd_variance(T_3_utpd);
00181 
00182 
00183 /* Example 1.4.5 */
00184 
00185 T_1_bt : [[1,2], [[1,1],[[]],[[]]], [[]]];
00186 tbtp(T_1_bt);
00187 T_3_bt : [[3,5,2], [[]], [[]], [[2,1],[[]],[[]]]];
00188 tbtp(T_3_bt);
00189 T_1_bt_minsum : min_sum_tbt(T_1_bt);
00190 T_1_bt_maxsum : max_sum_tbt(T_1_bt);
00191 assert(T_1_bt_minsum = T_1_bt_maxsum);
00192 T_3_bt_minsum : min_sum_tbt(T_3_bt);
00193 T_3_bt_maxsum : max_sum_tbt(T_3_bt);
00194 assert(T_1_bt = delta_tm(T_1_bt_minsum));
00195 delta_tm(T_3_bt_minsum);
00196 delta_tm(T_3_bt_maxsum);
00197 
00198 
00199 /* Example 1.4.6 */
00200 
00201 T_1_tpd : tauprob_tbt(T_1_bt);
00202 T_1_stpd: fullratsimp(tauprob_symbolical_tbt(T_1_bt));
00203 T_3_tpd : tauprob_tbt(T_3_bt);
00204 
00205 
00206 /* Example 1.4.7 */
00207 
00208 lower_bound_nlvs_tau(T_1_bt);
00209 lower_bound_nlvs(T_1_tpd);
00210 nlvs_l(T_1_tpd);
00211 upper_bound_nlvs(T_1_tpd);
00212 upper_bound_nlvs_tau(T_1_bt);
00213 
00214 lower_bound_nlvs_tau(T_3_bt);
00215 lower_bound_nlvs(T_3_tpd);
00216 nlvs_l(T_3_tpd);
00217 upper_bound_nlvs(T_3_tpd);
00218 upper_bound_nlvs_tau(T_3_bt);
00219 
00220 
00221 /* ******************************************************************
00222    * Section "Axiomatising the canonical order on branching tuples" *
00223    ******************************************************************
00224 */
00225 
00226 /* Example 1.5.1 */
00227 
00228 bth([1,2],2)[1];
00229 bth([1,2],3)[1];
00230 
00231 /* The saturated tuples are: */
00232 bth([1,2],2)[2];
00233 bth([1,2],3)[2];
00234 
00235 /* A single saturated tuple computed greedily: */
00236 satgr8 : bth_saturated_greedy([1,2],8);
00237 length(satgr8);
00238 length(sublist(satgr8, lambda([x],is(x=7))));
00239 length(sublist(satgr8, lambda([x],is(x=8))));
00240 fib(9);
00241 fib(8);
00242 fib(7);
00243 
00244 /* In general, the following functions computes the length of saturated tuples
00245    for integral branching tuples t in two ways: */
00246 sat_length_2_ways(t,s) := [length(bth_saturated_greedy(t,s)),
00247   last(int_seq_bt(t)(s+1))];
00248 
00249 
00250 /* **********************************************************
00251    * Section "How to select distances and measures" *
00252    **********************************************************
00253 */
00254 
00255 /* Example 1.8.1 */
00256 
00257 h_T1bt : ipd_rp(T_1_stpd)$
00258 float(hm2sm(h_T1bt));
00259 tpd_flatten(T_1_stpd);
00260 float(tpd_flatten(T_1_stpd));
00261 fullratsimp(tpd_variance(T_1_stpd));
00262 float(tpd_variance(T_1_stpd));
00263 
00264 h_T3bt : ipd_rp(T_3_tpd)$
00265 float(hm2sm(h_T3bt));
00266 tpd_flatten(T_3_tpd);
00267 tpd_variance(T_3_tpd);
00268 
00269 
00270 /* Example 1.8.2 and 1.8.3 */
00271 
00272 /* The trivial heuristics */
00273 
00274 trivial_ncl_ucp1 : amended_heuristics_lookahead_distances(
00275   generalised_ucp1,
00276   [trivial_distance],
00277   [tau2],
00278   trivial_sat_approx,
00279   [delta_n,delta_c,delta_l])$
00280 trivial_ncl_ast_54 : dll_red_st_dist(
00281   weak_php_fcs(5,4),
00282   trivial_ncl_ucp1,
00283   generalised_ucp1);
00284 
00285 assert(nnds_l(trivial_ncl_ast_54) = 103);
00286 assert(height(l2ult(trivial_ncl_ast_54)) = 8);
00287 assert(levelled_height(l2ult(trivial_ncl_ast_54)) = 3);
00288 
00289 tbt_t_ast_54 : ast2tbt(trivial_ncl_ast_54, 1);
00290 tbt_n_ast_54 : ast2tbt(trivial_ncl_ast_54, 2);
00291 tbt_c_ast_54 : ast2tbt(trivial_ncl_ast_54, 3);
00292 tbt_l_ast_54 : ast2tbt(trivial_ncl_ast_54, 4);
00293 
00294 tpd_t_ast_54 : tauprob_tbt(tbt_t_ast_54);
00295 tpd_n_ast_54 : tauprob_tbt(tbt_n_ast_54);
00296 tpd_c_ast_54 : tauprob_tbt(tbt_c_ast_54);
00297 tpd_l_ast_54 : tauprob_tbt(tbt_l_ast_54);
00298 
00299 assert_float_equal(tpd_variance(tpd_t_ast_54), 3336.0);
00300 assert_float_equal(tpd_variance(tpd_n_ast_54), 121710.5758316126);
00301 assert_float_equal(tpd_variance(tpd_c_ast_54), 29857.78137771181);
00302 assert_float_equal(tpd_variance(tpd_l_ast_54), 38701.49861318067);
00303 
00304 assert_float_equal(upper_bound_nlvs_tau(tbt_t_ast_54), 256.0);
00305 assert_float_equal(upper_bound_nlvs_tau(tbt_n_ast_54), 1043653.908038483);
00306 assert_float_equal(upper_bound_nlvs_tau(tbt_c_ast_54), 201830.0227763765);
00307 assert_float_equal(upper_bound_nlvs_tau(tbt_l_ast_54), 120414.1082378856);
00308 
00309 
00310 /* Delta(n) as heuristics */
00311 
00312 n_clt_ucp1 : amended_heuristics_lookahead_distances(generalised_ucp1, [delta_n], [tau2], trivial_sat_approx, [delta_c,delta_l,trivial_distance])$
00313 n_clt_ast_54 : dll_red_st_dist(weak_php_fcs(5,4), n_clt_ucp1, generalised_ucp1);
00314 
00315 assert(nnds_l(n_clt_ast_54) = 71);
00316 assert(height(l2ult(n_clt_ast_54)) = 7);
00317 assert(levelled_height(l2ult(n_clt_ast_54)) = 3);
00318 
00319 tbt_nn_ast_54 : ast2tbt(n_clt_ast_54, 1);
00320 tbt_nc_ast_54 : ast2tbt(n_clt_ast_54, 2);
00321 tbt_nl_ast_54 : ast2tbt(n_clt_ast_54, 3);
00322 tbt_nt_ast_54 : ast2tbt(n_clt_ast_54, 4);
00323 
00324 tpd_nn_ast_54 : tauprob_tbt(tbt_nn_ast_54);
00325 tpd_nc_ast_54 : tauprob_tbt(tbt_nc_ast_54);
00326 tpd_nl_ast_54 : tauprob_tbt(tbt_nl_ast_54);
00327 tpd_nt_ast_54 : tauprob_tbt(tbt_nt_ast_54);
00328 
00329 assert_float_equal(tpd_variance(tpd_nn_ast_54), 21963.20063203072);
00330 assert_float_equal(tpd_variance(tpd_nc_ast_54), 6777.794153245422);
00331 assert_float_equal(tpd_variance(tpd_nl_ast_54), 8703.973094479255);
00332 assert_float_equal(tpd_variance(tpd_nt_ast_54), 1216.0);
00333 
00334 assert_float_equal(upper_bound_nlvs_tau(tbt_nn_ast_54), 150923.8661445005);
00335 assert_float_equal(upper_bound_nlvs_tau(tbt_nc_ast_54), 62181.59240217086);
00336 assert_float_equal(upper_bound_nlvs_tau(tbt_nl_ast_54), 41122.97764837247);
00337 assert_float_equal(upper_bound_nlvs_tau(tbt_nt_ast_54), 128.0);
00338 
00339 
00340 /* Delta(c) as heuristics */
00341 
00342 c_nlt_ucp1 : amended_heuristics_lookahead_distances(generalised_ucp1, [delta_c], [tau2], trivial_sat_approx, [delta_n,delta_l,trivial_distance])$
00343 c_nlt_ast_54 : dll_red_st_dist(weak_php_fcs(5,4), c_nlt_ucp1, generalised_ucp1);
00344 
00345 assert(nnds_l(c_nlt_ast_54) = 49);
00346 assert(height(l2ult(c_nlt_ast_54)) = 7);
00347 assert(levelled_height(l2ult(c_nlt_ast_54)) = 3);
00348 
00349 tbt_cc_ast_54 : ast2tbt(c_nlt_ast_54, 1);
00350 tbt_cn_ast_54 : ast2tbt(c_nlt_ast_54, 2);
00351 tbt_cl_ast_54 : ast2tbt(c_nlt_ast_54, 3);
00352 tbt_ct_ast_54 : ast2tbt(c_nlt_ast_54, 4);
00353 
00354 tpd_cc_ast_54 : tauprob_tbt(tbt_cc_ast_54);
00355 tpd_cn_ast_54 : tauprob_tbt(tbt_cn_ast_54);
00356 tpd_cl_ast_54 : tauprob_tbt(tbt_cl_ast_54);
00357 tpd_ct_ast_54 : tauprob_tbt(tbt_ct_ast_54);
00358 
00359 assert_float_equal(tpd_variance(tpd_cc_ast_54), 7787.909873270139);
00360 assert_float_equal(tpd_variance(tpd_cn_ast_54), 27672.21496842504);
00361 assert_float_equal(tpd_variance(tpd_cl_ast_54), 8632.885062774241);
00362 assert_float_equal(tpd_variance(tpd_ct_ast_54), 591.0);
00363 
00364 assert_float_equal(upper_bound_nlvs_tau(tbt_cc_ast_54), 1835346.792423415);
00365 assert_float_equal(upper_bound_nlvs_tau(tbt_cn_ast_54), 2.619514500649467E+7);
00366 assert_float_equal(upper_bound_nlvs_tau(tbt_cl_ast_54), 603346.2305311395);
00367 assert_float_equal(upper_bound_nlvs_tau(tbt_ct_ast_54), 128.0);
00368 
00369 
00370 /* Delta(l) as heuristics */
00371 
00372 l_nct_ucp1 : amended_heuristics_lookahead_distances(generalised_ucp1, [delta_l], [tau2], trivial_sat_approx, [delta_n,delta_c,trivial_distance])$
00373 l_nct_ast_54 : dll_red_st_dist(weak_php_fcs(5,4), l_nct_ucp1, generalised_ucp1);
00374 
00375 assert(nnds_l(l_nct_ast_54) = 45);
00376 assert(height(l2ult(l_nct_ast_54)) = 9);
00377 assert(levelled_height(l2ult(l_nct_ast_54)) = 3);
00378 
00379 tbt_ll_ast_54 : ast2tbt(l_nct_ast_54, 1);
00380 tbt_ln_ast_54 : ast2tbt(l_nct_ast_54, 2);
00381 tbt_lc_ast_54 : ast2tbt(l_nct_ast_54, 3);
00382 tbt_lt_ast_54 : ast2tbt(l_nct_ast_54, 4);
00383 
00384 tpd_ll_ast_54 : tauprob_tbt(tbt_ll_ast_54);
00385 tpd_ln_ast_54 : tauprob_tbt(tbt_ln_ast_54);
00386 tpd_lc_ast_54 : tauprob_tbt(tbt_lc_ast_54);
00387 tpd_lt_ast_54 : tauprob_tbt(tbt_lt_ast_54);
00388 
00389 assert_float_equal(tpd_variance(tpd_ll_ast_54), 65665.08598951569);
00390 assert_float_equal(tpd_variance(tpd_ln_ast_54), 407777.1493197185);
00391 assert_float_equal(tpd_variance(tpd_lc_ast_54), 47323.01217783934);
00392 assert_float_equal(tpd_variance(tpd_lt_ast_54), 1551.0);
00393 
00394 assert_float_equal(upper_bound_nlvs_tau(tbt_ll_ast_54), 9396594.315155165);
00395 assert_float_equal(upper_bound_nlvs_tau(tbt_ln_ast_54), 9.075102530316168E+8);
00396 assert_float_equal(upper_bound_nlvs_tau(tbt_lc_ast_54), 1.243424793136493E+7);
00397 assert_float_equal(upper_bound_nlvs_tau(tbt_lt_ast_54), 512.0);
00398 
00399 
00400 /* The weighted number of clauses as heuristics */
00401 
00402 wnc_nclt_ucp1 : amended_heuristics_lookahead_distances(
00403   generalised_ucp1,
00404   [wn_newclauses(weightingscheme_OKsolver2002)],
00405   [tau2],
00406   trivial_sat_approx,
00407   [delta_n,delta_c,delta_l,trivial_distance])$
00408 wnc_nclt_ast_54 : dll_red_st_dist(
00409   weak_php_fcs(5,4),
00410   wnc_nclt_ucp1,
00411   generalised_ucp1);
00412 
00413 assert(nnds_l(wnc_nclt_ast_54) = 47);
00414 assert(height(l2ult(wnc_nclt_ast_54)) = 10);
00415 assert(levelled_height(l2ult(wnc_nclt_ast_54)) = 3);
00416 
00417 tbt_wncwnc_ast_54 : ast2tbt(wnc_nclt_ast_54, 1);
00418 tbt_wncn_ast_54 : ast2tbt(wnc_nclt_ast_54, 2);
00419 tbt_wncc_ast_54 : ast2tbt(wnc_nclt_ast_54, 3);
00420 tbt_wncl_ast_54 : ast2tbt(wnc_nclt_ast_54, 4);
00421 tbt_wnct_ast_54 : ast2tbt(wnc_nclt_ast_54, 5);
00422 
00423 tpd_wncwnc_ast_54 : tauprob_tbt(tbt_wncwnc_ast_54);
00424 tpd_wncn_ast_54 : tauprob_tbt(tbt_wncn_ast_54);
00425 tpd_wncc_ast_54 : tauprob_tbt(tbt_wncc_ast_54);
00426 tpd_wncl_ast_54 : tauprob_tbt(tbt_wncl_ast_54);
00427 tpd_wnct_ast_54 : tauprob_tbt(tbt_wnct_ast_54);
00428 
00429 assert_float_equal(tpd_variance(tpd_wncwnc_ast_54), 3.4394359770340516E+8);
00430 assert_float_equal(tpd_variance(tpd_wncn_ast_54), 3.615624833939703E+7);
00431 assert_float_equal(tpd_variance(tpd_wncc_ast_54), 1730952.892499223);
00432 assert_float_equal(tpd_variance(tpd_wncl_ast_54), 1872320.636555014);
00433 assert_float_equal(tpd_variance(tpd_wnct_ast_54), 2968.0);
00434 
00435 assert_float_equal(upper_bound_nlvs_tau(tbt_wncwnc_ast_54), 1.910402952727581E+78);
00436 assert_float_equal(upper_bound_nlvs_tau(tbt_wncn_ast_54), 1.890496564547904E+14);
00437 assert_float_equal(upper_bound_nlvs_tau(tbt_wncc_ast_54), 9.850640859775653E+10);
00438 assert_float_equal(upper_bound_nlvs_tau(tbt_wncl_ast_54), 2.481139355236184E+10);
00439 assert_float_equal(upper_bound_nlvs_tau(tbt_wnct_ast_54), 1024.0);
00440 
00441 
00442 /* Delta(l) as heuristics for weak_php_fcs(6,5) */
00443 
00444 l_nct_ast_65 : dll_red_st_dist(weak_php_fcs(6,5), l_nct_ucp1, generalised_ucp1);
00445 
00446 assert(nnds_l(l_nct_ast_65) = 219);
00447 assert(height(l2ult(l_nct_ast_65)) = 16);
00448 assert(levelled_height(l2ult(l_nct_ast_65)) = 4);
00449 
00450 tbt_ll_ast_65 : ast2tbt(l_nct_ast_65, 1);
00451 tbt_ln_ast_65 : ast2tbt(l_nct_ast_65, 2);
00452 tbt_lc_ast_65 : ast2tbt(l_nct_ast_65, 3);
00453 tbt_lt_ast_65 : ast2tbt(l_nct_ast_65, 4);
00454 
00455 tpd_ll_ast_65 : tauprob_tbt(tbt_ll_ast_65);
00456 tpd_ln_ast_65 : tauprob_tbt(tbt_ln_ast_65);
00457 tpd_lc_ast_65 : tauprob_tbt(tbt_lc_ast_65);
00458 tpd_lt_ast_65 : tauprob_tbt(tbt_lt_ast_65);
00459 
00460 assert_float_equal(tpd_variance(tpd_ll_ast_65), 3.874019989410695E+8);
00461 assert_float_equal(tpd_variance(tpd_ln_ast_65), 1.401235525398172E+10);
00462 assert_float_equal(tpd_variance(tpd_lc_ast_65), 1.7926669098571474E+8);
00463 assert_float_equal(tpd_variance(tpd_lt_ast_65), 311868.0);
00464 
00465 assert_float_equal(upper_bound_nlvs_tau(tbt_ll_ast_65), 1.263199352585657E+14);
00466 assert_float_equal(upper_bound_nlvs_tau(tbt_ln_ast_65), 4.745043472858466E+15);
00467 assert_float_equal(upper_bound_nlvs_tau(tbt_lc_ast_65), 3.227130302471304E+14);
00468 assert_float_equal(upper_bound_nlvs_tau(tbt_lt_ast_65), 65536.0);
00469 
00470 
00471 
00472 
00473 
00474 
00475 /* Example 1.8.4 */
00476 
00477 /* Minimising the variances */
00478 
00479 /* The weighted number of clauses as heuristics for weak_php_fcs(6,5) */
00480 
00481 ok2002_ncl234_ucp1 : amended_heuristics_lookahead_distances(
00482   generalised_ucp1,
00483   [wn_newclauses_2(weightingscheme_OKsolver2002), delta_n],
00484   [tau2],
00485   trivial_sat_approx,
00486   [delta_n,delta_c,delta_l,n_newclauses(2),n_newclauses(3),n_newclauses(4)])$
00487 ok2002_ncl234_ast_65 : dll_red_st_dist(
00488   weak_php_fcs(6,5),
00489   ok2002_ncl234_ucp1,
00490   generalised_ucp_ple1);
00491 
00492 assert(nnds_l(ok2002_ncl234_ast_65) = 77);
00493 assert(height(l2ult(ok2002_ncl234_ast_65)) = 12);
00494 assert(levelled_height(l2ult(ok2002_ncl234_ast_65)) = 3);
00495 
00496 assert(count_inf_branches(ok2002_ncl234_ast_65,6) = 23);
00497 col_ok2002_ncl234_ast_65 : collapse_inf_branches(ok2002_ncl234_ast_65, 6);
00498 
00499 assert(nnds_l(col_ok2002_ncl234_ast_65) = 31);
00500 assert(height(l2ult(col_ok2002_ncl234_ast_65)) = 9);
00501 assert(levelled_height(l2ult(col_ok2002_ncl234_ast_65)) = 2);
00502 
00503 tbt_wnc_ok2002_ncl234_ast_65 : ast2tbt(col_ok2002_ncl234_ast_65, 1);
00504 tbt_n_ok2002_ncl234_ast_65 : ast2tbt(col_ok2002_ncl234_ast_65, 3);
00505 tbt_c_ok2002_ncl234_ast_65 : ast2tbt(col_ok2002_ncl234_ast_65, 4);
00506 tbt_l_ok2002_ncl234_ast_65 : ast2tbt(col_ok2002_ncl234_ast_65, 5);
00507 
00508 tpd_wnc_ok2002_ncl234_ast_65 : tauprob_tbt(tbt_wnc_ok2002_ncl234_ast_65);
00509 tpd_n_ok2002_ncl234_ast_65 : tauprob_tbt(tbt_n_ok2002_ncl234_ast_65);
00510 tpd_c_ok2002_ncl234_ast_65 : tauprob_tbt(tbt_c_ok2002_ncl234_ast_65);
00511 tpd_l_ok2002_ncl234_ast_65 : tauprob_tbt(tbt_l_ok2002_ncl234_ast_65);
00512 
00513 assert_float_equal(tpd_variance(tpd_wnc_ok2002_ncl234_ast_65), 242775.8846080581);
00514 assert_float_equal(tpd_variance(tpd_n_ok2002_ncl234_ast_65), 4274916.597124265);
00515 assert_float_equal(tpd_variance(tpd_c_ok2002_ncl234_ast_65), 213026.3762745041);
00516 assert_float_equal(tpd_variance(tpd_l_ok2002_ncl234_ast_65), 307364.6985536006);
00517 
00518 assert_float_equal(upper_bound_nlvs_tau(tpd_wnc_ok2002_ncl234_ast_65), 1595.856418802932);
00519 assert_float_equal(upper_bound_nlvs_tau(tpd_n_ok2002_ncl234_ast_65), 61.85207603853764);
00520 assert_float_equal(upper_bound_nlvs_tau(tpd_c_ok2002_ncl234_ast_65), 100.8063825114651);
00521 assert_float_equal(upper_bound_nlvs_tau(tpd_l_ok2002_ncl234_ast_65), 92.08543943298893);
00522 
00523 
00524 minvarn(x) := tpd_variance(tauprob_tbt(
00525   x * tbt_wnc_ok2002_ncl234_ast_65 + (1-x) * tbt_n_ok2002_ncl234_ast_65));
00526 plot2d(minvarn, [x,0,1]);
00527 approx_min_varn : min_scanning(minvarn, [[0,1]], 100)[2][1];
00528 assert_float_equal(approx_min_varn, 1);
00529 
00530 roundd(x,d) := float(round(x*10^d)/10^d);
00531 
00532 minvarc(x) := tpd_variance(tauprob_tbt(
00533   x * tbt_wnc_ok2002_ncl234_ast_65 + (1-x) * tbt_c_ok2002_ncl234_ast_65));
00534 plot2d(minvarc, [x,0,1]);
00535 approx_min_varc : min_scanning(minvarc, [[0,1]], 100)[2][1];
00536 approx_min_varc : min_scanning(minvarc, [[approx_min_varc-0.1,min(approx_min_varc+0.1,1)]], 100)[2][1];
00537 approx_min_varc : min_scanning(minvarc, [[approx_min_varc-0.01,min(approx_min_varc+0.01,1)]], 100)[2][1];
00538 assert_float_equal(approx_min_varc, 0.9543999999999999);
00539 approx_min_varc : roundd(approx_min_varc, 4);
00540 assert_float_equal(approx_min_varc, 0.9544);
00541 
00542 minvarl(x) := tpd_variance(tauprob_tbt(
00543   x * tbt_wnc_ok2002_ncl234_ast_65 + (1-x) * tbt_l_ok2002_ncl234_ast_65));
00544 plot2d(minvarl, [x,0,1]);
00545 approx_min_varl : min_scanning(minvarl, [[0,1]], 100)[2][1];
00546 approx_min_varl : min_scanning(minvarl, [[approx_min_varl-0.1,min(approx_min_varl+0.1,1)]], 100)[2][1];
00547 approx_min_varl : min_scanning(minvarl, [[approx_min_varl-0.01,min(approx_min_varl+0.01,1)]], 100)[2][1];
00548 assert_float_equal(approx_min_varl, 0.985);
00549 
00550 tpbt_w2_ok2002_ncl234_ast_65 : ast2tbt(col_ok2002_ncl234_ast_65, 6);
00551 tpbt_w3_ok2002_ncl234_ast_65 : ast2tbt(col_ok2002_ncl234_ast_65, 7);
00552 tpbt_w4_ok2002_ncl234_ast_65 : ast2tbt(col_ok2002_ncl234_ast_65, 8);
00553 
00554 minvarw23(x,y) := tpd_variance(tauprob_tbt(
00555   x * tpbt_w2_ok2002_ncl234_ast_65 + y * (1-x) * tpbt_w3_ok2002_ncl234_ast_65 +
00556   (1 - x - y * (1-x)) * tpbt_w4_ok2002_ncl234_ast_65))$
00557 plot3d(minvarw23, [x,0.1,0.9], [y,0.1,0.9]);
00558 approx_min_varw23 : min_scanning(minvarw23, [[0.1,0.9], [0.1,0.9]], 30)[2];
00559 approx_min_varw23 : min_scanning(minvarw23,
00560   [[approx_min_varw23[1]-0.1,approx_min_varw23[1]+0.1],
00561   [approx_min_varw23[2]-0.1,approx_min_varw23[2]+0.1]],
00562   30)[2];
00563 approx_min_varw23 : min_scanning(minvarw23,
00564   [[approx_min_varw23[1]-0.01,approx_min_varw23[1]+0.01],
00565   [approx_min_varw23[2]-0.01,approx_min_varw23[2]+0.01]],
00566   30)[2];
00567 assert_float_equal(approx_min_varw23[1],0.7146666666666667);
00568 assert_float_equal(approx_min_varw23[2], 0.358);
00569 approx_min_varw23[1] : roundd(approx_min_varw23[1], 4);
00570 assert_float_equal(approx_min_varw23[1],0.7147);
00571 
00572 /* For unconstrained optimisation one could use x = exp(lambda)/(1+exp(lambda)) and
00573    y = exp(mu)/(1+exp(mu)), where now lambda, mu are arbitrary real numbers
00574    (this also takes care of openness).
00575 */
00576 
00577 approx_min_varw : [
00578  approx_min_varw23[1],
00579  approx_min_varw23[2] * (1-approx_min_varw23[1]),
00580  1 - approx_min_varw23[1] - approx_min_varw23[2] * (1-approx_min_varw23[1])];
00581 approx_min_varw : approx_min_varw / approx_min_varw[1];
00582 approx_min_varw[2] : roundd(approx_min_varw[2],3);
00583 approx_min_varw[3] : roundd(approx_min_varw[3],3);
00584 assert_float_equal(approx_min_varw[1], 1);
00585 assert_float_equal(approx_min_varw[2], 0.143);
00586 assert_float_equal(approx_min_varw[3], 0.256);
00587 
00588 
00589 
00590 /* Optimised heuristics: clause-weights (using Delta(l) as secondary heuristics) */
00591 
00592 weightingscheme_special(k) :=
00593   if k >= 2 and k <= 4 then approx_min_varw[k-1]
00594   else error("Only clause-lengths 2,3,4 allowed!")$
00595 
00596 ok2002_php65_ucp1 : amended_heuristics_lookahead_distances(
00597   generalised_ucp1,
00598   [wn_newclauses_2(weightingscheme_special), delta_l],
00599   [tau2],
00600   trivial_sat_approx,
00601   [])$
00602 ok2002_php65_ast_65 : dll_red_st_dist(
00603   weak_php_fcs(6,5),
00604   ok2002_php65_ucp1,
00605   generalised_ucp_ple1);
00606 
00607 assert(nnds_l(ok2002_php65_ast_65) = 67);
00608 assert(height(l2ult(ok2002_php65_ast_65)) = 12);
00609 assert(levelled_height(l2ult(ok2002_php65_ast_65)) = 3);
00610 
00611 assert(count_inf_branches(ok2002_php65_ast_65, 0) = 13);
00612 col_ok2002_php65_ast_65 : collapse_inf_branches(ok2002_php65_ast_65, 0);
00613 
00614 assert(nnds_l(col_ok2002_php65_ast_65) = 41);
00615 assert(height(l2ult(col_ok2002_php65_ast_65)) = 11);
00616 assert(levelled_height(l2ult(col_ok2002_php65_ast_65)) = 2);
00617 
00618 
00619 /* Optimised heuristics: clause-weights (using, as originally, Delta(n) as secondary heuristics) */
00620 
00621 ok2002n_php65_ucp1 : amended_heuristics_lookahead_distances(
00622   generalised_ucp1,
00623   [wn_newclauses_2(weightingscheme_special), delta_n],
00624   [tau2],
00625   trivial_sat_approx,
00626   [])$
00627 ok2002n_php65_ast_65 : dll_red_st_dist(
00628   weak_php_fcs(6,5),
00629   ok2002n_php65_ucp1,
00630   generalised_ucp_ple1);
00631 
00632 assert(nnds_l(ok2002n_php65_ast_65) = 67);
00633 assert(height(l2ult(ok2002n_php65_ast_65)) = 12);
00634 assert(levelled_height(l2ult(ok2002n_php65_ast_65)) = 3);
00635 
00636 assert(count_inf_branches(ok2002n_php65_ast_65, 0) = 13);
00637 col_ok2002n_php65_ast_65 : collapse_inf_branches(ok2002n_php65_ast_65, 0);
00638 
00639 assert(nnds_l(col_ok2002n_php65_ast_65) = 41);
00640 assert(height(l2ult(col_ok2002n_php65_ast_65)) = 11);
00641 assert(levelled_height(l2ult(col_ok2002n_php65_ast_65)) = 2);
00642 
00643 
00644 /* Optimised heuristics: Linear combination of weighted clauses and Delta(l) */
00645 
00646 ok2002wl_php65_ucp1 : amended_heuristics_lookahead_distances(
00647   generalised_ucp1,
00648   [lambda([F0,F1],
00649     approx_min_varl * wn_newclauses_2(weightingscheme_OKsolver2002)(F0,F1)
00650     + (1-approx_min_varl) * delta_l(F0,F1)),
00651    delta_n],
00652   [tau2],
00653   trivial_sat_approx,
00654   [])$
00655 ok2002wl_php65_ast_65 : dll_red_st_dist(
00656   weak_php_fcs(6,5),
00657   ok2002wl_php65_ucp1,
00658   generalised_ucp_ple1);
00659 
00660 assert(nnds_l(ok2002wl_php65_ast_65) = 79);
00661 assert(height(l2ult(ok2002wl_php65_ast_65)) = 9);
00662 assert(levelled_height(l2ult(ok2002wl_php65_ast_65)) = 3);
00663 
00664 assert(count_inf_branches(ok2002wl_php65_ast_65, 0) = 25);
00665 col_ok2002wl_php65_ast_65 : collapse_inf_branches(ok2002wl_php65_ast_65, 0);
00666 
00667 assert(nnds_l(col_ok2002wl_php65_ast_65) = 29);
00668 assert(height(l2ult(col_ok2002wl_php65_ast_65)) = 6);
00669 assert(levelled_height(l2ult(col_ok2002wl_php65_ast_65)) = 2);
00670 
00671 
00672 /* Optimised heuristics: Linear combination of weighted clauses and Delta(c) */
00673 
00674 ok2002wc_php65_ucp1 : amended_heuristics_lookahead_distances(
00675   generalised_ucp1,
00676   [lambda([F0,F1],
00677     approx_min_varc * wn_newclauses_2(weightingscheme_OKsolver2002)(F0,F1)
00678     + (1-approx_min_varc) * delta_c(F0,F1)),
00679    delta_n],
00680   [tau2],
00681   trivial_sat_approx,
00682   [])$
00683 ok2002wc_php65_ast_65 : dll_red_st_dist(
00684   weak_php_fcs(6,5),
00685   ok2002wc_php65_ucp1,
00686   generalised_ucp_ple1);
00687 
00688 assert(nnds_l(ok2002wc_php65_ast_65) = 79);
00689 assert(height(l2ult(ok2002wc_php65_ast_65)) = 9);
00690 assert(levelled_height(l2ult(ok2002wc_php65_ast_65)) = 3);
00691 
00692 assert(count_inf_branches(ok2002wc_php65_ast_65, 0) = 25);
00693 col_ok2002wc_php65_ast_65 : collapse_inf_branches(ok2002wc_php65_ast_65, 0);
00694 
00695 assert(nnds_l(col_ok2002wc_php65_ast_65) = 29);
00696 assert(height(l2ult(col_ok2002wc_php65_ast_65)) = 6);
00697 assert(levelled_height(l2ult(col_ok2002wc_php65_ast_65)) = 2);
00698 
00699 
00700 /* Example 1.8.5 */
00701 
00702 /* Minimising the tau-upper bounds */
00703 
00704 mintaun(x) := upper_bound_nlvs_tau(
00705   x * tbt_wnc_ok2002_ncl234_ast_65 + (1-x) * tbt_n_ok2002_ncl234_ast_65);
00706 plot2d(mintaun, [x,0.1,0.9]);
00707 approx_min_taun : min_scanning(mintaun, [[0,1]], 100)[2][1];
00708 approx_min_taun : min_scanning(mintaun, [[approx_min_taun-0.1,approx_min_taun+0.1]], 100)[2][1];
00709 assert_float_equal(approx_min_taun, 0.492);
00710 
00711 mintauc(x) := upper_bound_nlvs_tau(
00712   x * tbt_wnc_ok2002_ncl234_ast_65 + (1-x) * tbt_c_ok2002_ncl234_ast_65);
00713 plot2d(mintauc, [x,0.2,0.95]);
00714 approx_min_tauc : min_scanning(mintauc, [[0,1]], 100)[2][1];
00715 approx_min_tauc : min_scanning(mintauc, [[approx_min_tauc-0.05,approx_min_tauc+0.05]], 100)[2][1];
00716 assert_float_equal(approx_min_tauc, 0.891);
00717 
00718 
00719 mintaul(x) := upper_bound_nlvs_tau(
00720   x * tbt_wnc_ok2002_ncl234_ast_65 + (1-x) * tbt_l_ok2002_ncl234_ast_65);
00721 plot2d(mintaul, [x,0.2,0.99]);
00722 approx_min_taul : min_scanning(mintaul, [[0,1]], 100)[2][1];
00723 approx_min_taul : min_scanning(mintaul, [[approx_min_taul-0.05,approx_min_taul+0.05]], 100)[2][1];
00724 assert_float_equal(approx_min_taul, 0.949);
00725 
00726 
00727 mintauw23(x,y) := upper_bound_nlvs_tau(
00728   x * tpbt_w2_ok2002_ncl234_ast_65 + y * (1-x) * tpbt_w3_ok2002_ncl234_ast_65 +
00729   (1 - x - y * (1-x)) * tpbt_w4_ok2002_ncl234_ast_65)$
00730 plot3d(mintauw23, [x,0.2,0.7], [y,0.2,0.7]);
00731 
00732 approx_min_tauw23 : min_scanning(mintauw23, [[0.1,0.9], [0.1,0.9]], 30)[2];
00733 approx_min_tauw23 : min_scanning(mintauw23,
00734   [[approx_min_tauw23[1]-0.1,approx_min_tauw23[1]+0.1],
00735   [approx_min_tauw23[2]-0.1,approx_min_tauw23[2]+0.1]],
00736   30)[2];
00737 approx_min_tauw23 : min_scanning(mintauw23,
00738   [[approx_min_tauw23[1]-0.01,approx_min_tauw23[1]+0.01],
00739   [approx_min_tauw23[2]-0.01,approx_min_tauw23[2]+0.01]],
00740   30)[2];
00741 assert_float_equal(approx_min_tauw23[1],0.384);
00742 assert_float_equal(approx_min_tauw23[2], 0.6233333333333334);
00743 approx_min_tauw23[2] : roundd(approx_min_tauw23[2], 4);
00744 assert_float_equal(approx_min_tauw23[2],0.6233);
00745 
00746 approx_min_tauw : [
00747  approx_min_tauw23[1],
00748  approx_min_tauw23[2] * (1-approx_min_tauw23[1]),
00749  1 - approx_min_tauw23[1] - approx_min_tauw23[2] * (1-approx_min_tauw23[1])];
00750 approx_min_tauw : approx_min_tauw / approx_min_tauw[1];
00751 approx_min_tauw[2] : roundd(approx_min_tauw[2],4);
00752 approx_min_tauw[3] : roundd(approx_min_tauw[3],4);
00753 assert_float_equal(approx_min_tauw[1], 1);
00754 assert_float_equal(approx_min_tauw[2], 0.9999);
00755 assert_float_equal(approx_min_tauw[3], 0.6043);
00756 
00757 
00758 /* Optimised heuristics: clause-weights (using, as originally, Delta(n) as secondary heuristics) */
00759 
00760 weightingscheme_special_t(k) :=
00761   if k >= 2 and k <= 4 then approx_min_tauw[k-1]
00762   else error("Only clause-lengths 2,3,4 allowed!")$
00763 
00764 ok2002nt_php65_ucp1 : amended_heuristics_lookahead_distances(
00765   generalised_ucp1,
00766   [wn_newclauses_2(weightingscheme_special_t), delta_n],
00767   [tau2],
00768   trivial_sat_approx,
00769   [])$
00770 ok2002nt_php65_ast_65 : dll_red_st_dist(
00771   weak_php_fcs(6,5),
00772   ok2002nt_php65_ucp1,
00773   generalised_ucp_ple1);
00774 
00775 assert(nnds_l(ok2002nt_php65_ast_65) = 79);
00776 assert(height(l2ult(ok2002nt_php65_ast_65)) = 9);
00777 assert(levelled_height(l2ult(ok2002nt_php65_ast_65)) = 3);
00778 
00779 assert(count_inf_branches(ok2002nt_php65_ast_65, 0) = 25);
00780 col_ok2002nt_php65_ast_65 : collapse_inf_branches(ok2002nt_php65_ast_65, 0);
00781 
00782 assert(nnds_l(col_ok2002nt_php65_ast_65) = 29);
00783 assert(height(l2ult(col_ok2002nt_php65_ast_65)) = 6);
00784 assert(levelled_height(l2ult(col_ok2002nt_php65_ast_65)) = 2);
00785 
00786 
00787 /* Optimised heuristics: Linear combination of weighted clauses and Delta(n) */
00788 
00789 ok2002wnt_php65_ucp1 : amended_heuristics_lookahead_distances(
00790   generalised_ucp1,
00791   [lambda([F0,F1],
00792     approx_min_taun * wn_newclauses_2(weightingscheme_OKsolver2002)(F0,F1)
00793     + (1-approx_min_taun) * delta_c(F0,F1)),
00794    delta_n],
00795   [tau2],
00796   trivial_sat_approx,
00797   [])$
00798 ok2002wnt_php65_ast_65 : dll_red_st_dist(
00799   weak_php_fcs(6,5),
00800   ok2002wnt_php65_ucp1,
00801   generalised_ucp_ple1);
00802 
00803 assert(nnds_l(ok2002wnt_php65_ast_65) = 79);
00804 assert(height(l2ult(ok2002wnt_php65_ast_65)) = 9);
00805 assert(levelled_height(l2ult(ok2002wnt_php65_ast_65)) = 3);
00806 
00807 assert(count_inf_branches(ok2002wnt_php65_ast_65, 0) = 25);
00808 col_ok2002wnt_php65_ast_65 : collapse_inf_branches(ok2002wnt_php65_ast_65, 0);
00809 
00810 assert(nnds_l(col_ok2002wnt_php65_ast_65) = 29);
00811 assert(height(l2ult(col_ok2002wnt_php65_ast_65)) = 6);
00812 assert(levelled_height(l2ult(col_ok2002wnt_php65_ast_65)) = 2);
00813 
00814 
00815 /* Optimised heuristics: Linear combination of weighted clauses and Delta(c) */
00816 
00817 ok2002wct_php65_ucp1 : amended_heuristics_lookahead_distances(
00818   generalised_ucp1,
00819   [lambda([F0,F1],
00820     approx_min_tauc * wn_newclauses_2(weightingscheme_OKsolver2002)(F0,F1)
00821     + (1-approx_min_tauc) * delta_c(F0,F1)),
00822    delta_n],
00823   [tau2],
00824   trivial_sat_approx,
00825   [])$
00826 ok2002wct_php65_ast_65 : dll_red_st_dist(
00827   weak_php_fcs(6,5),
00828   ok2002wct_php65_ucp1,
00829   generalised_ucp_ple1);
00830 
00831 assert(nnds_l(ok2002wct_php65_ast_65) = 79);
00832 assert(height(l2ult(ok2002wct_php65_ast_65)) = 9);
00833 assert(levelled_height(l2ult(ok2002wct_php65_ast_65)) = 3);
00834 
00835 assert(count_inf_branches(ok2002wct_php65_ast_65, 0) = 25);
00836 col_ok2002wct_php65_ast_65 : collapse_inf_branches(ok2002wct_php65_ast_65, 0);
00837 
00838 assert(nnds_l(col_ok2002wct_php65_ast_65) = 29);
00839 assert(height(l2ult(col_ok2002wct_php65_ast_65)) = 6);
00840 assert(levelled_height(l2ult(col_ok2002wct_php65_ast_65)) = 2);
00841 
00842 
00843 /* Optimised heuristics: Linear combination of weighted clauses and Delta(l) */
00844 
00845 ok2002wlt_php65_ucp1 : amended_heuristics_lookahead_distances(
00846   generalised_ucp1,
00847   [lambda([F0,F1],
00848     approx_min_taul * wn_newclauses_2(weightingscheme_OKsolver2002)(F0,F1)
00849     + (1-approx_min_taul) * delta_l(F0,F1)),
00850    delta_n],
00851   [tau2],
00852   trivial_sat_approx,
00853   [])$
00854 ok2002wlt_php65_ast_65 : dll_red_st_dist(
00855   weak_php_fcs(6,5),
00856   ok2002wlt_php65_ucp1,
00857   generalised_ucp_ple1);
00858 
00859 assert(nnds_l(ok2002wlt_php65_ast_65) = 79);
00860 assert(height(l2ult(ok2002wlt_php65_ast_65)) = 9);
00861 assert(levelled_height(l2ult(ok2002wlt_php65_ast_65)) = 3);
00862 
00863 assert(count_inf_branches(ok2002wlt_php65_ast_65, 0) = 25);
00864 col_ok2002wlt_php65_ast_65 : collapse_inf_branches(ok2002wlt_php65_ast_65, 0);
00865 
00866 assert(nnds_l(col_ok2002wlt_php65_ast_65) = 29);
00867 assert(height(l2ult(col_ok2002wlt_php65_ast_65)) = 6);
00868 assert(levelled_height(l2ult(col_ok2002wlt_php65_ast_65)) = 2);
00869 
00870 
00871 /* ***********************************
00872    * Section "The order of branches" *
00873    ***********************************
00874 */
00875 
00876 /* Example 1.9.1 */
00877 
00878 F0 : weak_php_fcs(3,2);
00879 F1 : weak_php_fcs(3,3);
00880 
00881 assert(probsatrand(F0[2]) = 19683 / 262144);
00882 assert_float_equal(log(probsatrand(F0[2])), logprobrand(F0[2]));
00883 assert(probsatrand(F1[2]) = 6751269 / 134217728);
00884 assert_float_equal(log(probsatrand(F1[2])), logprobrand(F1[2]));
00885 
00886 assert(1 - firstorder_sat_approx(F0[2]) = 9/4);
00887 assert(1 - firstorder_sat_approx(F1[2]) = 21/8);
00888 
00889 assert(independence_number_m_cs(F0[2]) = 6);
00890 assert(hermitian_defect_cs(F0[2]) = 6);
00891 assert(1 - rest(satprob_seqap_mcind_trrs(F0[2]),1) = [9/4, 3/8, 5/4, 59/64, 65/64, 1]);
00892 
00893 assert(independence_number_m_cs(F1[2]) = 9);
00894 assert(hermitian_defect_cs(F1[2]) = 9);
00895 assert(1 - rest(satprob_seqap_mcind_trrs(F1[2]),1) = [21/8, -33/64, 1045/512, 107/256, 157/128, 469/512, 257/256, 505/512, 253/256]);
00896 
00897 1 - float(rest(satprob_seqap_mcind_trrs(weak_php_cs(4,3)),1));
00898 
00899 assert(max_degree_cvg_cs(F0[2]) = 4);
00900 assert(1 / locallemma_satapprox(F0[2]) = 4 * 1/4);
00901 assert(max_degree_cvg_cs(F1[2]) = 6);
00902 assert(1 / locallemma_satapprox(F1[2]) = 6 * 1/4);
00903 
00904 assert(1 / locallemmasum_satapprox(F0[2]) = 3 * 1 + 6 * (2 * 1/4 + 2 * 1/4));
00905 assert(1 / locallemmasum_satapprox(F1[2]) = 3 * 3/2 + 9 * (2 * 1/4 + 2 * 1/8));
00906