Index
263
Linear equivalence classes, 204, 205
sizes distribution, 205, 208
Linear temporal logic (LTL), 4, 16
Look-up tables (LUTs), 179, 188–191
M
MA, see Modular arithmetic
Majority expressions Look-Up Table (MLUT),
136
Majority Inverter Graph (MIG) algorithm,
136
Majority logic
axiomatization
Associativity axiom, 139, 140
axioms, types, 138
Commutativity axiom, 139
Distribution axiom, 139, 141
Inverter Propagation axiom, 139, 142
Majority, 139–140, 142
binary value, 137
B2M algorithm, 136
DSD, 137
equivalence, 138
majority algebra axiomatization, 135
MPC algorithm, 137
average memory usage, 156
cost, 153, 154
4-input functions, 146–149
5-input functions, 149–153
runtime, 155, 156
tables formulation, 144–146
operation, 137, 138
AND and OR functions, 137, 138
primitive functions, 136, 144
construction of, 140
input variables, 141–143
Shannon decomposition, 137
SISTOOL program, 136
SMT, 136, 137
XMG, 136
Majority Logic Synthesizer (MALS)
algorithm, 136
Microcontroller implementation, 27
Minimal degree assignment (MDA), 161
HMDA, 166
offline scheduling problem, 165
polynomial time algorithms, 166
selection strategy, heuristic, 166–167
Minimal partition assignment (MPA), 161
benchmarks, 167
BFS tree, 168
HMPA2, 169–170
literals, 168
MLUT, see Majority expressions Look-Up
Table (MLUT )
Modified Levenshtein Distance (MLD)
algorithm, 136
Modular arithmetic (MA), 237
Modular multiplication, 237, 238, 240,
250–251
Modulus function calculation, 245–248
automaton model, 240
bit-by-bit input reduction, 241
cryptography, 240
hardware realization, 240
limitation, 240
memory elements, 240
modular exponentiation, 243
periodic property, 242–243
powers of 2, 243–244
type 2 n ± k, 244–245
Monte Carlo Tree Search (MCTS)-based SAT
solving algorithm
backpropagation, 110, 112
backtracking-based solver, 108
benchmark problems, 123–124
CDCL, 107
analysis, 115–117
backpropagation phase, 114, 115
implication graph, 113
search trees visualization, 112
selection phase, 113
unit propagation, 114
variable assignment, 113, 114
CNF, 108, 110
expansion phase, 111–112
explicit assignment, 109
heuristics
probability heuristics, 119–120
scoring heuristics, 117–122, 124–130
implementations, 109
partial variable assignment, 109, 110
preprocessing, multiple solver instances,
122–123
as preprocessor, 130–131
selection phase, 110–111
simulation phase, 110, 112
UCT formula, 109–110
unit propagation, 108
MPA, see Minimal partition assignment
MPC algorithm, 137
average memory usage, 156
cost, 153, 154
4-input functions, 146–149
5-input functions, 149–153
runtime, 155, 156
tables formulation, 144–146
263
Linear equivalence classes, 204, 205
sizes distribution, 205, 208
Linear temporal logic (LTL), 4, 16
Look-up tables (LUTs), 179, 188–191
M
MA, see Modular arithmetic
Majority expressions Look-Up Table (MLUT),
136
Majority Inverter Graph (MIG) algorithm,
136
Majority logic
axiomatization
Associativity axiom, 139, 140
axioms, types, 138
Commutativity axiom, 139
Distribution axiom, 139, 141
Inverter Propagation axiom, 139, 142
Majority, 139–140, 142
binary value, 137
B2M algorithm, 136
DSD, 137
equivalence, 138
majority algebra axiomatization, 135
MPC algorithm, 137
average memory usage, 156
cost, 153, 154
4-input functions, 146–149
5-input functions, 149–153
runtime, 155, 156
tables formulation, 144–146
operation, 137, 138
AND and OR functions, 137, 138
primitive functions, 136, 144
construction of, 140
input variables, 141–143
Shannon decomposition, 137
SISTOOL program, 136
SMT, 136, 137
XMG, 136
Majority Logic Synthesizer (MALS)
algorithm, 136
Microcontroller implementation, 27
Minimal degree assignment (MDA), 161
HMDA, 166
offline scheduling problem, 165
polynomial time algorithms, 166
selection strategy, heuristic, 166–167
Minimal partition assignment (MPA), 161
benchmarks, 167
BFS tree, 168
HMPA2, 169–170
literals, 168
MLUT, see Majority expressions Look-Up
Table (MLUT )
Modified Levenshtein Distance (MLD)
algorithm, 136
Modular arithmetic (MA), 237
Modular multiplication, 237, 238, 240,
250–251
Modulus function calculation, 245–248
automaton model, 240
bit-by-bit input reduction, 241
cryptography, 240
hardware realization, 240
limitation, 240
memory elements, 240
modular exponentiation, 243
periodic property, 242–243
powers of 2, 243–244
type 2 n ± k, 244–245
Monte Carlo Tree Search (MCTS)-based SAT
solving algorithm
backpropagation, 110, 112
backtracking-based solver, 108
benchmark problems, 123–124
CDCL, 107
analysis, 115–117
backpropagation phase, 114, 115
implication graph, 113
search trees visualization, 112
selection phase, 113
unit propagation, 114
variable assignment, 113, 114
CNF, 108, 110
expansion phase, 111–112
explicit assignment, 109
heuristics
probability heuristics, 119–120
scoring heuristics, 117–122, 124–130
implementations, 109
partial variable assignment, 109, 110
preprocessing, multiple solver instances,
122–123
as preprocessor, 130–131
selection phase, 110–111
simulation phase, 110, 112
UCT formula, 109–110
unit propagation, 108
MPA, see Minimal partition assignment
MPC algorithm, 137
average memory usage, 156
cost, 153, 154
4-input functions, 146–149
5-input functions, 149–153
runtime, 155, 156
tables formulation, 144–146