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)