3.1.8. cnfformula.families.randomformulas module

Random CNF Formulas

class RandCmdHelper

Bases: object

Command line helper for random formulas

Methods

build_cnf(args)	Build a conjunction
setup_command_line(parser)	Setup the command line options for an and of literals

static build_cnf(args)

Build a conjunction

Arguments: - args: command line options

description = 'random k-CNF'

name = 'randkcnf'

static setup_command_line(parser)

Setup the command line options for an and of literals

Arguments: - parser: parser to load with options.

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

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(dict), optional

a set of total/partial assigments such that all clauses in the formula will be satisfied by all of them.

Returns:

a CNF object

Raises:

ValueError

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

all_clauses(k, indices, 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, indices, m, planted_assignments)

sample_clauses_dense(k, indices, m, planted_assignments)