Plans for generators for (various types of) random clausesets.
More...
Go to the source code of this file.
Detailed Description
Plans for generators for (various types of) random clausesets.
 Todo:
 Random subsets, sublists etc.
 Todo:
 Specifying the AES random generator

The specification was given in [Oliver Kullmann, CSR192002].

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

s in W(64) (the seed)

k in W(64) (the formula number)

n in W^*(31) (the number of variables)

p a list of length m, where m in W^*(31) (number of clausesizes), with entries natural numbers, strictly increasing, and with p[i] in W^*(31) (the clauselengths).

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 AESfunction 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:

First let alpha_n be the bijection from {0, ..., 2n1} > {n, ..., n}  {0}, given by 0 > 1, 1 > 2, ..., n1 > n, and then n > 1, n+1 > 2, ..., 2n1 > n.

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)).

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:

C_i := [l_{i,1}, ..., l_{i,p}], where the l_{i,j} are defined as follows.

For 1 <= j <= p let x_{i,j} be defined by x_{i,j} := OKlitgenerator(s, k, nj+1, p, (i1)*p+j1).

The sign of l_{i,j} is now the sign of x_{i,j}.

The variable of l_{i,1} is the variable of x_{i,1}.

Regarding the other variables, we can not use the x_{i,j} for j > 1, since we must avoid repetitions.

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 nonboolean clausesets 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.
 Todo:
 Implementing the AES random generator
 Todo:
 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.
 Todo:
 DONE (moved to ComputerAlgebra/Satisfiability/Lisp/FiniteFunctions/Basics.mac) Move random_full_fcs
Definition in file RandomClauseSets.hpp.