RandomClauseSets.hpp File Reference

Plans for generators for (various types of) random clause-sets. More...

Go to the source code of this file.

Detailed Description

Plans for generators for (various types of) random clause-sets.

Random subsets, sublists etc.
Specifying the AES random generator
  • The specification was given in [Oliver Kullmann, CSR19-2002].
  • For k in NNZ let W(k) := {0, ..., 2^k - 1} and W^*(k) := W(k) - {0}.
  • Input specification: OKgenerator(s,k,n,p,c), where
    1. s in W(64) (the seed)
    2. k in W(64) (the formula number)
    3. n in W^*(31) (the number of variables)
    4. p a list of length m, where m in W^*(31) (number of clause-sizes), with entries natural numbers, strictly increasing, and with p[i] in W^*(31) (the clause-lengths).
    5. c a list of length m, with entries c[i] in W^*(32) (the number of clauses of length p[i]).
  • According to our general philosophy, the function OKgenerator does not check its input, but we have a special test function for this.
  • The AES-function is considered as aes: W(128) x W(128) -> W(128), given by "aes_int(p,k,10)" (see ComputerAlgebra/Cryptology/Lisp/CryptoSystems/Rijndael/AdvancedEncryptionStandard.mac).
  • The central helper function is the OKlitgenerator(s,k,n,p,c), where s,k,n as above, p in W(31), c in W(64), defined as follows:
    1. First let alpha_n be the bijection from {0, ..., 2n-1} -> {-n, ..., n} - {0}, given by 0 -> 1, 1 -> 2, ..., n-1 -> n, and then n -> -1, n+1 -> -2, ..., 2n-1 -> -n.
    2. Now OKlitgenerator(s,k,n,p,c) := alpha_n(aes_int(n * 2^96 + p * 2^64 + c, s * 2^64 + k,10) mod 2n)).
    3. Thus -2^31 < OKlitgenerator(s,k,n,p,c) < 2^31, where the value 0 is excluded.
  • Now the OKgenerator for m = 1 is defined as follows: OKgenerator(s,k,n,[p],[c]) := [C_1, ..., C_c], where for 1 <= i <= c we define:
    1. C_i := [l_{i,1}, ..., l_{i,p}], where the l_{i,j} are defined as follows.
    2. For 1 <= j <= p let x_{i,j} be defined by x_{i,j} := OKlitgenerator(s, k, n-j+1, p, (i-1)*p+j-1).
    3. The sign of l_{i,j} is now the sign of x_{i,j}.
    4. The variable of l_{i,1} is the variable of x_{i,1}.
    5. Regarding the other variables, we can not use the x_{i,j} for j > 1, since we must avoid repetitions.
    6. This is now achieved by using first x_{i,2}, then x_{i,3}, and so on, however not as absolute values, but only relative, that is, the variable l_{i,2} is value number |x_{i,2}| in the variables left from {1, ..., n} after having removed |x_{i,1}|, and so on.
  • The general OKgenerator(s,k,n,p,c) for m >= 1 is now defined as the concatenation of the values OKgenerator(s,k,n,[p[i]],[c[i]]) for i from 1 to m.
  • For generating non-boolean clause-sets there exists an additional parameter d in W^*(32), d >= 2, specifying the (uniform) domain size.
  • How to call the generalised OKgenerator (and the generalised OKlitgenerator)? Perhaps we use "OKgenerator_cs" and "OKgenerator_nbcs".
  • Finally, where to insert the additional parameter d in the parameter list? In the paper it is inserted after n, which seems reasonable.
Implementing the AES random generator
Filtering out
  • A natural extensions of random generators is by applying some filter, removing for example instances with repeated clauses.
  • We need a framework for this.
DONE (moved to ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/Basics.mac) Move random_full_fcs

Definition in file RandomClauseSets.hpp.