OKlibrary  0.2.1.6
RandomClauseSets.mac
Go to the documentation of this file.
```00001 /* Oliver Kullmann, 5.7.2008 (Swansea) */
00002 /* Copyright 2008, 2009, 2010, 2011, 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/DataStructures/Lisp/Lists.mac")\$
00024 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")\$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")\$
00026 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")\$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac")\$
00028 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Strings.mac")\$
00029
00030
00031 /* *********************************
00032    * The fixed clause-length model *
00033    *********************************
00034 */
00035
00036
00037 /* Computing a random repetition-free sublist of a given length k;
00038    V is a list, repetitions determine the chance of being elected, but the
00039    result is repetition-free. */
00040 /* Prerequisites: 0 <= k <= length(unique(V)). */
00041 random_k_sublist_l(V,k) := block([res : []],
00042   thru k do block([x : random_element(V)],
00043     res : cons(x,res),
00044     V : delete(x,V)),
00045   return(reverse(res)))\$
00046
00047 /* Using the Maxima pseudo-random generator, compute random clause-lists
00048    with n variables, clause-length k and c clauses: */
00049 /* Prerequisites: n,k,c >= 0, k <= n. */
00050 random_fcl(n,k,c) := block([V : create_list(i,i,1,n), F : []],
00051   thru c do block([C : random_k_sublist_l(V,k)],
00052     for i : 1 thru k do
00053       if random(2) = 1 then C[i] : -C[i],
00054     F : cons(setify(C),F)),
00055   return([V,reverse(F)]))\$
00056 random_fcs(n,k,c) := fcl2fcs(random_fcl(n,k,c))\$
00057
00058 output_random_fcl(n,k,c,filename) := output_fcl_v(
00059  sconcat("Pseudo-random clause-list created by Maxima::output_random_fcl(",n,",",k,",",c,").
00060 c ", created_by_OKlib()),
00061  random_fcl(n,k,c),filename,[])\$
00062 output_random_fcl_stdname(n,k,c) := output_random_fcl(n,k,c,sconcat("Random_",n,"_",k,"_",c,".cnf"))\$
00063 /* Convenience instantiation, specifying density and seed: */
00064 output_random_fcl_ds_stdname(n,k,density,seed) := (set_random(seed),
00065  output_random_fcl_stdname(n,k,round(density*n)))\$
00066
00067
00068 /* **********************************
00069    * The random clause-length model *
00070    **********************************
00071 */
00072
00073 /* Creating random clause-sets in the "random clause-length" model,
00074    where a parameter p governs the probability of inclusion of
00075    a variable (so with probability 1-p the variable is not included).
00076 */
00077 /* For p=1 every clause is full, for p=0 every clause is empty,
00078    and for p=2/3 every clause has the same probability. */
00079 /* The average clause-length is p * n (thus if the average shall be k,
00080    then set p = k/n). */
00081 /* Prerequisites: n,c >= 0, 0 <= p <= 1. */
00082 random_rcl_fcl(n,p,c) :=
00083  block([V : create_list(i,i,1,n), F : []],
00084   thru c do block([C : create_list(i,i,1,n)],
00085     for i : 1 thru n do
00086       if random(1.0) >= p then C[i] : 0
00087       else
00088         if random(2) = 1 then C[i] : -C[i],
00089     F : cons(setdifference(setify(C),{0}),F)),
00090   return([V,reverse(F)]))\$
00091 random_rcl_fcs(n,p,c) := fcl2fcs(random_rcl_fcl(n,p,c))\$
00092
00093
00094 /* **********************************
00095    * The OKgenerator (based on AES) *
00096    **********************************
00097 */
00098
00099 /* The underlying literal generator for boolean literals: */
00100 OKlitgenerator_l(s,k,n,p,c) := block(
00101  [x : mod(aes_int(n * 2^96 + p * 2^64 + c, s * 2^64 + k,10), 2*n)],
00102   if x < n then x+1 else n-1-x)\$
00103 /* The possible inputs are those where OKlitgenerator_l_p(s,k,n,p,c)
00104    is true:
00105 */
00106 OKlitgenerator_l_p(s,k,n,p,c) :=
00107  integerp(s) and is(0 <= s and s < 2^64) and
00108  integerp(k) and is(0 <= k and k < 2^64) and
00109  integerp(n) and is(1 <= n and n < 2^31) and
00110  integerp(p) and is(0 <= p and p < 2^31) and
00111  integerp(c) and is(0 <= c and c < 2^64)\$
00112
00113 /* Creating (pseudo-)random boolean formal clause-lists with
00114  - seed s
00115  - formula number k
00116  - number of variables n
00117  - clause-length list P (strictly ascending)
00118  - clause-number list C (according to P).
00119 For the precise input-prerequisites see OKgenerator_fcl_p.
00120 */
00121 OKgenerator_fcl(s,k,n,P,C) := block([m : length(P)],
00122  if m > 1 then
00123    return([create_list(i,i,1,n),
00124            lappend(map(lambda([p,c],
00125                        OKgenerator_fcl(s,k,n,[p],[c])[2]), P, C))]),
00126  block([F : [], N : setn(n), p : P[1], c : C[1]],
00127    for i : 1 thru c do block([C : [], V : N],
00128      for j : 1 thru p do block(
00129       [x : OKlitgenerator_l(s, k, n-j+1, p, (i-1)*p+j-1)],
00130        C : cons(signum(x) * listify(V)[abs(x)], C),
00131        V : disjoin(abs(x), V)
00132      ),
00133    F : cons(setify(C),F)
00134   ),
00135  return([create_list(i,i,1,n), reverse(F)])))\$
00136
00137 /* Testing the inputs: */
00138 OKgenerator_fcl_p(s,k,n,P,C) :=
00139  integerp(s) and is(0 <= s and s < 2^64) and
00140  integerp(k) and is(0 <= k and k < 2^64) and
00141  integerp(n) and is(1 <= n and n < 2^31) and
00142  listp(P) and listp(C) and block([m : length(P)],
00143   is(m = length(C)) and is(1 <= m and m < 2^31) and
00144   strictascending_p(P) and
00145   every_s(lambda([p],is(1 <= p and p < 2^31)),P) and
00146   every_s(lambda([c],is(1 <= c and c < 2^32)),C))\$
00147
00148
00149 /* The underlying literal generator: */
00150 OKlitgenerator_nbl(s,k,n,d,p,c) := 0\$
00151
00152 OKgenerator_nbfcl(s,k,n,d,P,C) := []\$
00153
00154 /* Testing the inputs: */
00155 OKgenerator_nbfcl_p(s,k,n,d,P,C) := false\$
00156
00157
00158 /* *************************
00159    * Translated random DNF *
00160    *************************
00161 */
00162
00163
00164
00165
```