3.1.9. cnfgen.families.randomformulas module

Random CNF Formulas

RandomKCNF(k, n, m, seed=None, planted_assignments=None)

Build a random k-CNF

Sample \(m\) clauses over \(n\) variables, each of width \(k\), uniformly at random. The sampling is done without repetition, meaning that whenever a randomly picked clause is already in the CNF, it is sampled again.

Parameters:

k : int

width of each clause

n : int

number of variables to choose from. The resulting CNF object will contain n variables even if some are not mentioned in the clauses.

m : int

number of clauses to generate

seed : hashable object

seed of the random generator

planted_assignments : iterable(lists), optional

a set of total/partial assigments such that all clauses in the formula will be satisfied by all of them. Each partial assignment is a sequence of literals. Undefined behaviour if some assignment contains opposite literals.

Returns:

a CNF object

Raises:

ValueError

when some paramenter is negative, or when k>n.

all_clauses(k, n, planted_assignments)

clause_satisfied(cls, assignments)

Test whether a clause is satisfied by all assignments

Test if clauses cls is satisfied by all assigment in the list assignments.

sample_clauses(k, n, m, planted_assignments)

Sample m random k-clauses on a set of n variables

First it tries sparse sampling: - samples with repetition which is fast - filters bad samples

If after enough samples we haven’t got enough clauses we use dense sampling, namely we generare all possible clauses and pick at random m of them. This approach always succeeds, but is quite slower and wasteful for just few samples.

sample_clauses_dense(k, n, m, planted_assignments)