dunkirk.sh
optimizing a gate level bcm to the end of the earth and back
1#!/usr/bin/env python3
2"""
3Search for optimal BCD to 7-segment decoder circuit.
4Uses parallel SAT solving to search multiple configurations simultaneously.
5"""
6
7import multiprocessing as mp
8from concurrent.futures import ProcessPoolExecutor, as_completed
9import sys
10import time
11
12from bcd_optimization.solver import BCDTo7SegmentSolver
13from bcd_optimization.truth_tables import SEGMENT_MINTERMS, SEGMENT_NAMES
14
15
16def try_config(args):
17 """Try a single (n2, n3) configuration. Run in separate process."""
18 n2, n3, use_complements, restrict_functions = args
19 cost = n2 * 2 + n3 * 3
20 n_gates = n2 + n3
21
22 if n_gates < 7:
23 return None, cost, f"Skipped (only {n_gates} gates)"
24
25 solver = BCDTo7SegmentSolver()
26 solver.generate_prime_implicants()
27
28 try:
29 result = solver._try_mixed_synthesis(n2, n3, use_complements, restrict_functions)
30 if result:
31 return result, cost, "SUCCESS"
32 else:
33 return None, cost, "UNSAT"
34 except Exception as e:
35 return None, cost, f"Error: {e}"
36
37
38def verify_result(result):
39 """Verify a synthesis result is correct."""
40 def eval_func2(func, a, b):
41 return (func >> (a * 2 + b)) & 1
42
43 def eval_func3(func, a, b, c):
44 return (func >> (a * 4 + b * 2 + c)) & 1
45
46 for digit in range(10):
47 A = (digit >> 3) & 1
48 B = (digit >> 2) & 1
49 C = (digit >> 1) & 1
50 D = digit & 1
51
52 nodes = [A, B, C, D, 1-A, 1-B, 1-C, 1-D]
53
54 for g in result.gates:
55 if isinstance(g.input2, tuple):
56 k, l = g.input2
57 val = eval_func3(g.func, nodes[g.input1], nodes[k], nodes[l])
58 else:
59 val = eval_func2(g.func, nodes[g.input1], nodes[g.input2])
60 nodes.append(val)
61
62 for seg in SEGMENT_NAMES:
63 expected = 1 if digit in SEGMENT_MINTERMS[seg] else 0
64 actual = nodes[result.output_map[seg]]
65 if actual != expected:
66 return False, f"Digit {digit}, {seg}: expected {expected}, got {actual}"
67
68 return True, "All correct"
69
70
71def main():
72 print("=" * 60)
73 print("BCD to 7-Segment Optimal Circuit Search")
74 print("=" * 60)
75 print()
76 print("Gates: AND, OR, XOR, NAND, NOR (2 and 3 input variants)")
77 print("Primary input complements (A', B', C', D') are free")
78 print()
79
80 # Configurations to try, sorted by cost
81 configs = []
82 for n2 in range(0, 15):
83 for n3 in range(0, 8):
84 cost = n2 * 2 + n3 * 3
85 n_gates = n2 + n3
86 if 7 <= n_gates <= 12 and 18 <= cost <= 22:
87 configs.append((n2, n3, True, True))
88
89 # Sort by cost, then by number of gates
90 configs.sort(key=lambda x: (x[0]*2 + x[1]*3, x[0]+x[1]))
91
92 print(f"Searching {len(configs)} configurations from {min(c[0]*2+c[1]*3 for c in configs)} to {max(c[0]*2+c[1]*3 for c in configs)} inputs")
93 print(f"Using {mp.cpu_count()} CPU cores")
94 print()
95
96 best_result = None
97 best_cost = float('inf')
98
99 start_time = time.time()
100
101 # Group configs by cost for better progress reporting
102 cost_groups = {}
103 for cfg in configs:
104 cost = cfg[0] * 2 + cfg[1] * 3
105 if cost not in cost_groups:
106 cost_groups[cost] = []
107 cost_groups[cost].append(cfg)
108
109 with ProcessPoolExecutor(max_workers=mp.cpu_count()) as executor:
110 for cost in sorted(cost_groups.keys()):
111 if cost >= best_cost:
112 continue
113
114 group = cost_groups[cost]
115 print(f"Trying {cost} inputs ({len(group)} configurations)...", flush=True)
116
117 futures = {executor.submit(try_config, cfg): cfg for cfg in group}
118
119 for future in as_completed(futures):
120 cfg = futures[future]
121 n2, n3 = cfg[0], cfg[1]
122
123 try:
124 result, result_cost, status = future.result(timeout=300)
125
126 if result is not None:
127 valid, msg = verify_result(result)
128 if valid:
129 print(f" {n2}x2 + {n3}x3 = {result_cost}: {status} (verified)")
130 if result_cost < best_cost:
131 best_result = result
132 best_cost = result_cost
133 # Cancel remaining futures at this cost level
134 for f in futures:
135 f.cancel()
136 break
137 else:
138 print(f" {n2}x2 + {n3}x3 = {result_cost}: INVALID - {msg}")
139 else:
140 print(f" {n2}x2 + {n3}x3 = {result_cost}: {status}")
141
142 except Exception as e:
143 print(f" {n2}x2 + {n3}x3: Error - {e}")
144
145 if best_result is not None and best_cost <= cost:
146 print(f"\nFound solution at {best_cost} inputs, stopping search.")
147 break
148
149 elapsed = time.time() - start_time
150
151 print()
152 print("=" * 60)
153 print("RESULTS")
154 print("=" * 60)
155 print(f"Search time: {elapsed:.1f} seconds")
156
157 if best_result:
158 print(f"Best solution: {best_cost} gate inputs")
159 print()
160 print("Gates:")
161
162 node_names = ['A', 'B', 'C', 'D', "A'", "B'", "C'", "D'"]
163 for g in best_result.gates:
164 i1 = node_names[g.input1]
165 if isinstance(g.input2, tuple):
166 k, l = g.input2
167 i2, i3 = node_names[k], node_names[l]
168 print(f" g{g.index}: {g.func_name}({i1}, {i2}, {i3})")
169 else:
170 i2 = node_names[g.input2]
171 print(f" g{g.index}: {g.func_name}({i1}, {i2})")
172 node_names.append(f"g{g.index}")
173
174 print()
175 print("Outputs:")
176 for seg in SEGMENT_NAMES:
177 print(f" {seg} = {node_names[best_result.output_map[seg]]}")
178 else:
179 print("No solution found in the search range.")
180
181
182if __name__ == "__main__":
183 main()