260
Index
Boolean functions (cont.)
equivalence class sizes, 199, 200
execution times, 204, 208
function equivalence partitions, 195
linear equivalence classes, 204, 205
sizes distribution, 205, 208
NPN equivalence, 195
quantum computation, 196
Rademacher-Walsh spectral domain, 195
representative function, 196
reversible circuits, 196
spectra
equivalence class, 198
Hadamard transform matrix, 197
mapping, 196
Rademacher-Walsh spectrum,
197–198
spectral equivalence classes, 204, 207
size distribution, 208, 209
spectral translations, 198–199
transformation algorithm, 201–204
translation costs, 200
Boolean functions, classes C N
BDE, 52
classifications, 52
coefficients, 60
decimal equivalents, 55, 56
derivative operations, 51
BV, 66–68
IDM, 65–67
k-fold derivative operation, 76–81
single derivative operation, 72–76
vectorial derivative operation, 65–66
(see also Vectorial derivative
operation)
equivalence relation, 54
exploration, 53, 58
IDM, 61–62
independence function, 56, 64–65
rank, 62–64
refiexivity, 54
representative function, 55, 57
single derivatives, 59
symmetry, 54
transitivity, 54–55
vectorial derivative, 60
Boolean minimization, 251–252
Boolean satisfiability (SAT), 3
exact synthesis, 178, 179
algorithm, 183–184
Boolean variables, 180–181
combinational Boolean circuits, 182
conflict limit, 185
constraint satisfaction problem,
182–183
correctness, 188
counterexample-guided abstractionrefinement algorithm, 184–185
decision procedure, 182
decomposition-based ESOP synthesis,
181
downward vs. upward search, 185
LUT mapping, 188–191
NPN4 equivalence class, 188–189
random, 188, 191
reversible logic synthesis, 188, 192
XOR-constraints to CNF, 183
See also Monte Carlo Tree Search
(MCTS)-based SAT solving
algorithm
Boolean to Majority (B2M) algorithm, 136
BV, see Binary vector
C
Chinese reminder theorem, 238
Chosen-ciphertext attack (CCA), 24
Chosen-plaintext attack (CPA), 24
Classes of Boolean functions, see Boolean
functions, classes C N
Combinational Boolean circuits, 182
Commutativity axiom, 139
Component functions (CFs), 217, 220
elements, 230
linear variables, 227–228
NPNP-classes, 228
P-equivalence classes, 231–234
projection functions, 229–231
variable assignments, 229, 230, 232
Computation Tree Logic (CTL), 4, 15
Conflict-Driven Clause Learning (CDCL),
107
analysis, 115–117
backpropagation phase, 114, 115
heuristics
probability heuristics, 119–120
scoring heuristics, 117–122
implication graph, 113
search trees visualization, 112
selection phase, 113
unit propagation, 114
variable assignment, 113, 114
Conjunctive normal form (CNF), 108, 110
Cryptographic key-exchange mechanisms
(KEMs), 21, 22
Cryptography, 196
Index
Boolean functions (cont.)
equivalence class sizes, 199, 200
execution times, 204, 208
function equivalence partitions, 195
linear equivalence classes, 204, 205
sizes distribution, 205, 208
NPN equivalence, 195
quantum computation, 196
Rademacher-Walsh spectral domain, 195
representative function, 196
reversible circuits, 196
spectra
equivalence class, 198
Hadamard transform matrix, 197
mapping, 196
Rademacher-Walsh spectrum,
197–198
spectral equivalence classes, 204, 207
size distribution, 208, 209
spectral translations, 198–199
transformation algorithm, 201–204
translation costs, 200
Boolean functions, classes C N
BDE, 52
classifications, 52
coefficients, 60
decimal equivalents, 55, 56
derivative operations, 51
BV, 66–68
IDM, 65–67
k-fold derivative operation, 76–81
single derivative operation, 72–76
vectorial derivative operation, 65–66
(see also Vectorial derivative
operation)
equivalence relation, 54
exploration, 53, 58
IDM, 61–62
independence function, 56, 64–65
rank, 62–64
refiexivity, 54
representative function, 55, 57
single derivatives, 59
symmetry, 54
transitivity, 54–55
vectorial derivative, 60
Boolean minimization, 251–252
Boolean satisfiability (SAT), 3
exact synthesis, 178, 179
algorithm, 183–184
Boolean variables, 180–181
combinational Boolean circuits, 182
conflict limit, 185
constraint satisfaction problem,
182–183
correctness, 188
counterexample-guided abstractionrefinement algorithm, 184–185
decision procedure, 182
decomposition-based ESOP synthesis,
181
downward vs. upward search, 185
LUT mapping, 188–191
NPN4 equivalence class, 188–189
random, 188, 191
reversible logic synthesis, 188, 192
XOR-constraints to CNF, 183
See also Monte Carlo Tree Search
(MCTS)-based SAT solving
algorithm
Boolean to Majority (B2M) algorithm, 136
BV, see Binary vector
C
Chinese reminder theorem, 238
Chosen-ciphertext attack (CCA), 24
Chosen-plaintext attack (CPA), 24
Classes of Boolean functions, see Boolean
functions, classes C N
Combinational Boolean circuits, 182
Commutativity axiom, 139
Component functions (CFs), 217, 220
elements, 230
linear variables, 227–228
NPNP-classes, 228
P-equivalence classes, 231–234
projection functions, 229–231
variable assignments, 229, 230, 232
Computation Tree Logic (CTL), 4, 15
Conflict-Driven Clause Learning (CDCL),
107
analysis, 115–117
backpropagation phase, 114, 115
heuristics
probability heuristics, 119–120
scoring heuristics, 117–122
implication graph, 113
search trees visualization, 112
selection phase, 113
unit propagation, 114
variable assignment, 113, 114
Conjunctive normal form (CNF), 108, 110
Cryptographic key-exchange mechanisms
(KEMs), 21, 22
Cryptography, 196