3.1.14. cnfgen.families.cpls module

Implementation of Thapen’s size-width tradeoff formula

CPLSFormula(a, b, c)

Thapen’s size-width tradeoff formula

The formula is a propositional version of the coloured polynomial local search principle (CPLS). A description can be found in [1]. The difference with the formula in the paper is that here, unary indices start from 1 instead of 0. Binary strings stil counts from 0, therefore the mappings \(f[i](x)=x'\) is actually represented in binary with the binary representation of \(x'-1\).

Parameters:

a: integer

number of levels

b: integer

nodes per level (must be a power of 2)

c: integer

number of colours (must be a power of 2)

References

[1]	N. Thapen (2016) Trade-offs between length and width in resolution. Theory of Computing, 12(1), 1–14.

intlog2(x)

Compute the ceiling of the log2(x)