dunkirk.sh
optimizing a gate level bcm to the end of the earth and back
feat: add circuit breaking to ignore consecutive gates
+42
bcd_optimization/solver.py
+42
bcd_optimization/solver.py
···
686
for sel2 in all_sels[idx1 + 1:]:
687
clauses.append([-sel1, -sel2])
688
689
+
# Constraint 2b: Symmetry breaking - gates of same type ordered by first input
690
+
# For consecutive gates of the same size, require first input index is non-decreasing
691
+
for gate_idx in range(n_gates - 1):
692
+
i = n_inputs + gate_idx
693
+
i_next = n_inputs + gate_idx + 1
694
+
size = gate_sizes[gate_idx]
695
+
size_next = gate_sizes[gate_idx + 1]
696
+
697
+
if size != size_next:
698
+
continue # Only break symmetry between same-type gates
699
+
700
+
if size == 2:
701
+
# For 2-input gates: if gate i has first input j and gate i+1 has first input j',
702
+
# require j <= j'
703
+
for j in range(i):
704
+
for k in range(j + 1, i):
705
+
for j_next in range(j): # j_next < j violates ordering
706
+
for k_next in range(j_next + 1, i_next):
707
+
if j_next in s2[i_next] and k_next in s2[i_next][j_next]:
708
+
clauses.append([-s2[i][j][k], -s2[i_next][j_next][k_next]])
709
+
elif size == 3:
710
+
for j in range(i):
711
+
for k in range(j + 1, i):
712
+
for l in range(k + 1, i):
713
+
for j_next in range(j):
714
+
for k_next in range(j_next + 1, i_next):
715
+
for l_next in range(k_next + 1, i_next):
716
+
if j_next in s3[i_next] and k_next in s3[i_next][j_next] and l_next in s3[i_next][j_next][k_next]:
717
+
clauses.append([-s3[i][j][k][l], -s3[i_next][j_next][k_next][l_next]])
718
+
else: # size == 4
719
+
for j in range(i):
720
+
for k in range(j + 1, i):
721
+
for l in range(k + 1, i):
722
+
for m in range(l + 1, i):
723
+
for j_next in range(j):
724
+
for k_next in range(j_next + 1, i_next):
725
+
for l_next in range(k_next + 1, i_next):
726
+
for m_next in range(l_next + 1, i_next):
727
+
if (j_next in s4[i_next] and k_next in s4[i_next][j_next] and
728
+
l_next in s4[i_next][j_next][k_next] and m_next in s4[i_next][j_next][k_next][l_next]):
729
+
clauses.append([-s4[i][j][k][l][m], -s4[i_next][j_next][k_next][l_next][m_next]])
730
+
731
# Constraint 3: Gate function consistency
732
for gate_idx in range(n_gates):
733
i = n_inputs + gate_idx
+19
-6
search_with_4input.py
+19
-6
search_with_4input.py
···
237
return f"{label}[{bar}] {current}/{total} ({pct:.0f}%)"
238
239
240
-
def try_config_with_stats(n2, n3, n4, use_complements, restrict_functions, stats_queue):
241
"""Try a single (n2, n3, n4) configuration with stats reporting."""
242
cost = n2 * 2 + n3 * 3 + n4 * 4
243
n_gates = n2 + n3 + n4
···
254
255
start = time.time()
256
try:
257
# Build the CNF without solving
258
cnf = solver._build_general_cnf(n2, n3, n4, use_complements, restrict_functions)
259
if cnf is None:
···
284
total_decisions = 0
285
286
while True:
287
sat_solver.conf_budget(conflict_budget)
288
status = sat_solver.solve_limited()
289
···
326
327
def try_config(args):
328
"""Try a single (n2, n3, n4) configuration. Run in separate process."""
329
-
n2, n3, n4, use_complements, restrict_functions, stats_queue = args
330
-
return try_config_with_stats(n2, n3, n4, use_complements, restrict_functions, stats_queue)
331
332
333
def worker_init():
···
478
configs_tested = 0
479
total_configs = len(configs)
480
481
-
# Create shared queue for stats
482
manager = Manager()
483
stats_queue = manager.Queue()
484
progress.stats_queue = stats_queue
485
486
with ProcessPoolExecutor(max_workers=mp.cpu_count(), initializer=worker_init) as executor:
···
506
# Start async progress display
507
progress.start(group_size, cost)
508
509
-
# Add stats_queue to each config
510
-
configs_with_queue = [(cfg[0], cfg[1], cfg[2], cfg[3], cfg[4], stats_queue) for cfg in group]
511
futures = {executor.submit(try_config, cfg): cfg for cfg in configs_with_queue}
512
found_solution = False
513
···
536
best_result = result
537
best_cost = result_cost
538
found_solution = True
539
for f in futures:
540
f.cancel()
541
break
···
237
return f"{label}[{bar}] {current}/{total} ({pct:.0f}%)"
238
239
240
+
def try_config_with_stats(n2, n3, n4, use_complements, restrict_functions, stats_queue, stop_event=None):
241
"""Try a single (n2, n3, n4) configuration with stats reporting."""
242
cost = n2 * 2 + n3 * 3 + n4 * 4
243
n_gates = n2 + n3 + n4
···
254
255
start = time.time()
256
try:
257
+
# Check early termination before building CNF
258
+
if stop_event and stop_event.is_set():
259
+
return None, cost, "Cancelled", (n2, n3, n4)
260
+
261
# Build the CNF without solving
262
cnf = solver._build_general_cnf(n2, n3, n4, use_complements, restrict_functions)
263
if cnf is None:
···
288
total_decisions = 0
289
290
while True:
291
+
# Check early termination
292
+
if stop_event and stop_event.is_set():
293
+
elapsed = time.time() - start
294
+
return None, cost, f"Cancelled ({elapsed:.1f}s, {total_conflicts} conflicts)", (n2, n3, n4)
295
+
296
sat_solver.conf_budget(conflict_budget)
297
status = sat_solver.solve_limited()
298
···
335
336
def try_config(args):
337
"""Try a single (n2, n3, n4) configuration. Run in separate process."""
338
+
n2, n3, n4, use_complements, restrict_functions, stats_queue, stop_event = args
339
+
return try_config_with_stats(n2, n3, n4, use_complements, restrict_functions, stats_queue, stop_event)
340
341
342
def worker_init():
···
487
configs_tested = 0
488
total_configs = len(configs)
489
490
+
# Create shared queue for stats and stop event for early termination
491
manager = Manager()
492
stats_queue = manager.Queue()
493
+
stop_event = manager.Event()
494
progress.stats_queue = stats_queue
495
496
with ProcessPoolExecutor(max_workers=mp.cpu_count(), initializer=worker_init) as executor:
···
516
# Start async progress display
517
progress.start(group_size, cost)
518
519
+
# Add stats_queue and stop_event to each config
520
+
stop_event.clear() # Reset for new cost group
521
+
configs_with_queue = [(cfg[0], cfg[1], cfg[2], cfg[3], cfg[4], stats_queue, stop_event) for cfg in group]
522
futures = {executor.submit(try_config, cfg): cfg for cfg in configs_with_queue}
523
found_solution = False
524
···
547
best_result = result
548
best_cost = result_cost
549
found_solution = True
550
+
# Signal other workers to stop
551
+
stop_event.set()
552
for f in futures:
553
f.cancel()
554
break