dunkirk.sh / bcd-optimization
optimizing a gate level bcm to the end of the earth and back
fork atom

feat: add fancy progress

dunkirk.sh e563d162 defd6bd1

verified
+644 -42
unified split
+295
bcd_optimization/solver.py
··· 599 599 } 600 600 return known.get(func, f"F4_{func:016b}") 601 601 602 + def _build_general_cnf(self, num_2input: int, num_3input: int, num_4input: int, 603 + use_complements: bool = True, restrict_functions: bool = True) -> Optional[dict]: 604 + """Build CNF for general synthesis without solving. Returns CNF + metadata for decoding.""" 605 + n_primary = 4 606 + n_inputs = 8 if use_complements else 4 607 + n_outputs = 7 608 + n_gates = num_2input + num_3input + num_4input 609 + n_nodes = n_inputs + n_gates 610 + 611 + truth_rows = list(range(10)) 612 + n_rows = len(truth_rows) 613 + 614 + clauses = [] 615 + var_counter = [1] 616 + 617 + def new_var(): 618 + v = var_counter[0] 619 + var_counter[0] += 1 620 + return v 621 + 622 + # x[i][t] = output of node i on row t 623 + x = {i: {t: new_var() for t in range(n_rows)} for i in range(n_nodes)} 624 + 625 + # Selection and function variables 626 + s2, s3, s4 = {}, {}, {} 627 + f2, f3, f4 = {}, {}, {} 628 + 629 + gate_sizes = [2] * num_2input + [3] * num_3input + [4] * num_4input 630 + 631 + for gate_idx in range(n_gates): 632 + i = n_inputs + gate_idx 633 + size = gate_sizes[gate_idx] 634 + 635 + if size == 2: 636 + s2[i] = {} 637 + for j in range(i): 638 + s2[i][j] = {k: new_var() for k in range(j + 1, i)} 639 + f2[i] = {p: {q: new_var() for q in range(2)} for p in range(2)} 640 + elif size == 3: 641 + s3[i] = {} 642 + for j in range(i): 643 + s3[i][j] = {} 644 + for k in range(j + 1, i): 645 + s3[i][j][k] = {l: new_var() for l in range(k + 1, i)} 646 + f3[i] = {p: {q: {r: new_var() for r in range(2)} for q in range(2)} for p in range(2)} 647 + else: 648 + s4[i] = {} 649 + for j in range(i): 650 + s4[i][j] = {} 651 + for k in range(j + 1, i): 652 + s4[i][j][k] = {} 653 + for l in range(k + 1, i): 654 + s4[i][j][k][l] = {m: new_var() for m in range(l + 1, i)} 655 + f4[i] = {p: {q: {r: {s: new_var() for s in range(2)} for r in range(2)} for q in range(2)} for p in range(2)} 656 + 657 + g = {h: {i: new_var() for i in range(n_nodes)} for h in range(n_outputs)} 658 + 659 + # Constraint 1: Primary inputs 660 + for t_idx, t in enumerate(truth_rows): 661 + for i in range(n_primary): 662 + bit = (t >> (n_primary - 1 - i)) & 1 663 + clauses.append([x[i][t_idx] if bit else -x[i][t_idx]]) 664 + if use_complements: 665 + for i in range(n_primary): 666 + bit = (t >> (n_primary - 1 - i)) & 1 667 + clauses.append([x[n_primary + i][t_idx] if not bit else -x[n_primary + i][t_idx]]) 668 + 669 + # Constraint 2: Each gate has exactly one input selection 670 + for gate_idx in range(n_gates): 671 + i = n_inputs + gate_idx 672 + size = gate_sizes[gate_idx] 673 + 674 + if size == 2: 675 + all_sels = [s2[i][j][k] for j in range(i) for k in range(j + 1, i)] 676 + elif size == 3: 677 + all_sels = [s3[i][j][k][l] for j in range(i) for k in range(j + 1, i) for l in range(k + 1, i)] 678 + else: 679 + all_sels = [s4[i][j][k][l][m] for j in range(i) for k in range(j + 1, i) for l in range(k + 1, i) for m in range(l + 1, i)] 680 + 681 + if not all_sels: 682 + return None 683 + 684 + clauses.append(all_sels) 685 + for idx1, sel1 in enumerate(all_sels): 686 + for sel2 in all_sels[idx1 + 1:]: 687 + clauses.append([-sel1, -sel2]) 688 + 689 + # Constraint 3: Gate function consistency 690 + for gate_idx in range(n_gates): 691 + i = n_inputs + gate_idx 692 + size = gate_sizes[gate_idx] 693 + 694 + if size == 2: 695 + for j in range(i): 696 + for k in range(j + 1, i): 697 + for t_idx in range(n_rows): 698 + for pv in range(2): 699 + for qv in range(2): 700 + for outv in range(2): 701 + clause = [-s2[i][j][k]] 702 + clause.append(-x[j][t_idx] if pv else x[j][t_idx]) 703 + clause.append(-x[k][t_idx] if qv else x[k][t_idx]) 704 + clause.append(-f2[i][pv][qv] if outv else f2[i][pv][qv]) 705 + clause.append(x[i][t_idx] if outv else -x[i][t_idx]) 706 + clauses.append(clause) 707 + elif size == 3: 708 + for j in range(i): 709 + for k in range(j + 1, i): 710 + for l in range(k + 1, i): 711 + for t_idx in range(n_rows): 712 + for pv in range(2): 713 + for qv in range(2): 714 + for rv in range(2): 715 + for outv in range(2): 716 + clause = [-s3[i][j][k][l]] 717 + clause.append(-x[j][t_idx] if pv else x[j][t_idx]) 718 + clause.append(-x[k][t_idx] if qv else x[k][t_idx]) 719 + clause.append(-x[l][t_idx] if rv else x[l][t_idx]) 720 + clause.append(-f3[i][pv][qv][rv] if outv else f3[i][pv][qv][rv]) 721 + clause.append(x[i][t_idx] if outv else -x[i][t_idx]) 722 + clauses.append(clause) 723 + else: 724 + for j in range(i): 725 + for k in range(j + 1, i): 726 + for l in range(k + 1, i): 727 + for m in range(l + 1, i): 728 + for t_idx in range(n_rows): 729 + for pv in range(2): 730 + for qv in range(2): 731 + for rv in range(2): 732 + for sv in range(2): 733 + for outv in range(2): 734 + clause = [-s4[i][j][k][l][m]] 735 + clause.append(-x[j][t_idx] if pv else x[j][t_idx]) 736 + clause.append(-x[k][t_idx] if qv else x[k][t_idx]) 737 + clause.append(-x[l][t_idx] if rv else x[l][t_idx]) 738 + clause.append(-x[m][t_idx] if sv else x[m][t_idx]) 739 + clause.append(-f4[i][pv][qv][rv][sv] if outv else f4[i][pv][qv][rv][sv]) 740 + clause.append(x[i][t_idx] if outv else -x[i][t_idx]) 741 + clauses.append(clause) 742 + 743 + # Constraint 3b: Restrict functions 744 + if restrict_functions: 745 + allowed_2input = [0b1000, 0b1110, 0b0110, 0b1001, 0b0111, 0b0001] 746 + allowed_3input = [0b10000000, 0b11111110, 0b01111111, 0b00000001, 0b10010110, 0b01101001] 747 + allowed_4input = [0x8000, 0xFFFE, 0x7FFF, 0x0001, 0x6996, 0x9669] 748 + 749 + for gate_idx in range(n_gates): 750 + i = n_inputs + gate_idx 751 + size = gate_sizes[gate_idx] 752 + 753 + if size == 2: 754 + or_clause = [] 755 + for func in allowed_2input: 756 + match_var = new_var() 757 + or_clause.append(match_var) 758 + for p in range(2): 759 + for q in range(2): 760 + bit_idx = p * 2 + q 761 + expected = (func >> bit_idx) & 1 762 + clauses.append([-match_var, f2[i][p][q] if expected else -f2[i][p][q]]) 763 + clauses.append(or_clause) 764 + elif size == 3: 765 + or_clause = [] 766 + for func in allowed_3input: 767 + match_var = new_var() 768 + or_clause.append(match_var) 769 + for p in range(2): 770 + for q in range(2): 771 + for r in range(2): 772 + bit_idx = p * 4 + q * 2 + r 773 + expected = (func >> bit_idx) & 1 774 + clauses.append([-match_var, f3[i][p][q][r] if expected else -f3[i][p][q][r]]) 775 + clauses.append(or_clause) 776 + else: 777 + or_clause = [] 778 + for func in allowed_4input: 779 + match_var = new_var() 780 + or_clause.append(match_var) 781 + for p in range(2): 782 + for q in range(2): 783 + for r in range(2): 784 + for s in range(2): 785 + bit_idx = p * 8 + q * 4 + r * 2 + s 786 + expected = (func >> bit_idx) & 1 787 + clauses.append([-match_var, f4[i][p][q][r][s] if expected else -f4[i][p][q][r][s]]) 788 + clauses.append(or_clause) 789 + 790 + # Constraint 4: Each output assigned to exactly one node 791 + for h in range(n_outputs): 792 + clauses.append([g[h][i] for i in range(n_nodes)]) 793 + for i in range(n_nodes): 794 + for j in range(i + 1, n_nodes): 795 + clauses.append([-g[h][i], -g[h][j]]) 796 + 797 + # Constraint 5: Output correctness 798 + for h, segment in enumerate(SEGMENT_NAMES): 799 + for t_idx, t in enumerate(truth_rows): 800 + expected = 1 if t in SEGMENT_MINTERMS[segment] else 0 801 + for i in range(n_nodes): 802 + clauses.append([-g[h][i], x[i][t_idx] if expected else -x[i][t_idx]]) 803 + 804 + return { 805 + 'clauses': clauses, 806 + 'n_vars': var_counter[0] - 1, 807 + 'gate_sizes': gate_sizes, 808 + 'n_inputs': n_inputs, 809 + 'n_nodes': n_nodes, 810 + 'use_complements': use_complements, 811 + 'x': x, 's2': s2, 's3': s3, 's4': s4, 812 + 'f2': f2, 'f3': f3, 'f4': f4, 'g': g, 813 + } 814 + 815 + def _decode_general_solution_from_cnf(self, model: set, cnf_data: dict) -> SynthesisResult: 816 + """Decode a SAT solution using stored CNF metadata.""" 817 + def is_true(var): 818 + return var in model 819 + 820 + gate_sizes = cnf_data['gate_sizes'] 821 + n_inputs = cnf_data['n_inputs'] 822 + n_nodes = cnf_data['n_nodes'] 823 + use_complements = cnf_data['use_complements'] 824 + s2, s3, s4 = cnf_data['s2'], cnf_data['s3'], cnf_data['s4'] 825 + f2, f3, f4 = cnf_data['f2'], cnf_data['f3'], cnf_data['f4'] 826 + g = cnf_data['g'] 827 + 828 + n_gates = len(gate_sizes) 829 + if use_complements: 830 + node_names = ['A', 'B', 'C', 'D', "A'", "B'", "C'", "D'"] + [f'g{i}' for i in range(n_gates)] 831 + else: 832 + node_names = ['A', 'B', 'C', 'D'] + [f'g{i}' for i in range(n_gates)] 833 + 834 + gates = [] 835 + total_cost = 0 836 + 837 + for gate_idx in range(n_gates): 838 + i = n_inputs + gate_idx 839 + size = gate_sizes[gate_idx] 840 + total_cost += size 841 + 842 + if size == 2: 843 + for j in range(i): 844 + for k in range(j + 1, i): 845 + if is_true(s2[i][j][k]): 846 + func = sum((1 << (p * 2 + q)) for p in range(2) for q in range(2) if is_true(f2[i][p][q])) 847 + func_name = self._decode_gate_function(func) 848 + gates.append(GateInfo(index=gate_idx, input1=j, input2=k, func=func, func_name=func_name)) 849 + node_names[i] = f"({node_names[j]} {func_name} {node_names[k]})" 850 + break 851 + elif size == 3: 852 + for j in range(i): 853 + for k in range(j + 1, i): 854 + for l in range(k + 1, i): 855 + if is_true(s3[i][j][k][l]): 856 + func = sum((1 << (p * 4 + q * 2 + r)) for p in range(2) for q in range(2) for r in range(2) if is_true(f3[i][p][q][r])) 857 + func_name = self._decode_3input_function(func) 858 + gates.append(GateInfo(index=gate_idx, input1=j, input2=(k, l), func=func, func_name=func_name)) 859 + node_names[i] = f"({node_names[j]} {func_name} {node_names[k]} {node_names[l]})" 860 + break 861 + else: 862 + for j in range(i): 863 + for k in range(j + 1, i): 864 + for l in range(k + 1, i): 865 + for m in range(l + 1, i): 866 + if is_true(s4[i][j][k][l][m]): 867 + func = sum((1 << (p * 8 + q * 4 + r * 2 + s)) for p in range(2) for q in range(2) for r in range(2) for s in range(2) if is_true(f4[i][p][q][r][s])) 868 + func_name = self._decode_4input_function(func) 869 + gates.append(GateInfo(index=gate_idx, input1=j, input2=(k, l, m), func=func, func_name=func_name)) 870 + node_names[i] = f"({node_names[j]} {func_name} {node_names[k]} {node_names[l]} {node_names[m]})" 871 + break 872 + 873 + output_map = {} 874 + expressions = {} 875 + for h, segment in enumerate(SEGMENT_NAMES): 876 + for i in range(n_nodes): 877 + if is_true(g[h][i]): 878 + output_map[segment] = i 879 + expressions[segment] = node_names[i] 880 + break 881 + 882 + num_2 = gate_sizes.count(2) 883 + num_3 = gate_sizes.count(3) 884 + num_4 = gate_sizes.count(4) 885 + 886 + return SynthesisResult( 887 + cost=total_cost, 888 + implicants_by_output={}, 889 + shared_implicants=[], 890 + method=f"exact_general_{num_2}x2_{num_3}x3_{num_4}x4", 891 + expressions=expressions, 892 + cost_breakdown=CostBreakdown(and_inputs=total_cost, or_inputs=0, num_and_gates=n_gates, num_or_gates=0), 893 + gates=gates, 894 + output_map=output_map, 895 + ) 896 + 602 897 def _try_general_synthesis(self, num_2input: int, num_3input: int, num_4input: int, 603 898 use_complements: bool = True, restrict_functions: bool = True) -> Optional[SynthesisResult]: 604 899 """Try synthesis with a mix of 2, 3, and 4-input gates."""
+349 -42
search_with_4input.py
··· 4 4 """ 5 5 6 6 import multiprocessing as mp 7 + from multiprocessing import Manager 7 8 from concurrent.futures import ProcessPoolExecutor, as_completed 8 9 import sys 9 10 import time 11 + import threading 12 + import queue 10 13 11 14 from bcd_optimization.solver import BCDTo7SegmentSolver 12 15 from bcd_optimization.truth_tables import SEGMENT_MINTERMS, SEGMENT_NAMES 16 + 17 + # ANSI escape codes for terminal control 18 + CLEAR_LINE = "\033[K" 19 + MOVE_UP = "\033[A" 20 + GREEN = "\033[92m" 21 + YELLOW = "\033[93m" 22 + CYAN = "\033[96m" 23 + DIM = "\033[2m" 24 + RESET = "\033[0m" 25 + BOLD = "\033[1m" 13 26 14 27 15 - def try_config(args): 16 - """Try a single (n2, n3, n4) configuration. Run in separate process.""" 17 - n2, n3, n4, use_complements, restrict_functions = args 28 + class ProgressDisplay: 29 + """Async progress display that updates in a separate thread.""" 30 + 31 + def __init__(self, stats_queue=None): 32 + self.lock = threading.Lock() 33 + self.running = False 34 + self.thread = None 35 + self.stats_queue = stats_queue 36 + 37 + # State 38 + self.completed = 0 39 + self.total = 0 40 + self.start_time = 0 41 + self.last_config = "" 42 + self.current_cost = 0 43 + self.message = "" 44 + 45 + # SAT solver stats (aggregated across all running configs) 46 + self.active_configs = {} # config_str -> stats dict 47 + self.total_conflicts = 0 48 + self.total_decisions = 0 49 + self.total_vars = 0 50 + self.total_clauses = 0 51 + 52 + def start(self, total, cost): 53 + """Start the progress display thread.""" 54 + with self.lock: 55 + self.completed = 0 56 + self.total = total 57 + self.start_time = time.time() 58 + self.last_config = "" 59 + self.current_cost = cost 60 + self.message = "" 61 + self.active_configs = {} 62 + self.total_conflicts = 0 63 + self.total_decisions = 0 64 + self.running = True 65 + 66 + self.thread = threading.Thread(target=self._update_loop, daemon=True) 67 + self.thread.start() 68 + 69 + def stop(self): 70 + """Stop the progress display thread.""" 71 + self.running = False 72 + if self.thread: 73 + self.thread.join(timeout=0.5) 74 + # Clear the line 75 + print(f"\r{CLEAR_LINE}", end="", flush=True) 76 + 77 + def update(self, completed, last_config=""): 78 + """Update progress state (called from main thread).""" 79 + with self.lock: 80 + self.completed = completed 81 + if last_config: 82 + self.last_config = last_config 83 + # Remove completed config from active 84 + if last_config in self.active_configs: 85 + del self.active_configs[last_config] 86 + 87 + def set_message(self, msg): 88 + """Set a temporary message to display.""" 89 + with self.lock: 90 + self.message = msg 91 + 92 + def _poll_stats(self): 93 + """Poll stats queue for updates from worker processes.""" 94 + if not self.stats_queue: 95 + return 96 + 97 + try: 98 + while True: 99 + stats = self.stats_queue.get_nowait() 100 + config = stats.get('config', '') 101 + with self.lock: 102 + self.active_configs[config] = stats 103 + # Aggregate stats 104 + self.total_conflicts = sum(s.get('conflicts', 0) for s in self.active_configs.values()) 105 + self.total_decisions = sum(s.get('decisions', 0) for s in self.active_configs.values()) 106 + self.total_vars = sum(s.get('vars', 0) for s in self.active_configs.values()) 107 + self.total_clauses = sum(s.get('clauses', 0) for s in self.active_configs.values()) 108 + except: 109 + pass # Queue empty 110 + 111 + def _update_loop(self): 112 + """Background thread that updates the display.""" 113 + import shutil 114 + 115 + spinner = "⠋⠙⠹⠸⠼⠴⠦⠧⠇⠏" 116 + spin_idx = 0 117 + last_conflicts = 0 118 + conflict_rate = 0 119 + 120 + def fmt_num(n): 121 + if n >= 1_000_000: 122 + return f"{n/1_000_000:.1f}M" 123 + elif n >= 1_000: 124 + return f"{n/1_000:.1f}K" 125 + return str(int(n)) 126 + 127 + while self.running: 128 + self._poll_stats() 129 + 130 + # Get terminal width each iteration (in case of resize) 131 + try: 132 + term_width = shutil.get_terminal_size().columns 133 + except: 134 + term_width = 80 135 + 136 + with self.lock: 137 + elapsed = time.time() - self.start_time 138 + speed = self.completed / elapsed if elapsed > 0 else 0 139 + remaining = self.total - self.completed 140 + eta = remaining / speed if speed > 0 else 0 141 + 142 + pct = 100 * self.completed / self.total if self.total > 0 else 0 143 + spin = spinner[spin_idx % len(spinner)] 144 + 145 + # Calculate conflict rate 146 + conflict_delta = self.total_conflicts - last_conflicts 147 + conflict_rate = conflict_rate * 0.7 + conflict_delta * 10 * 0.3 148 + last_conflicts = self.total_conflicts 149 + 150 + # Fixed parts (calculate their length) 151 + # Format: " ⠹ [BAR] 2/6 (33%) 0.8/s [ACT] 29K" 152 + prefix = f" {spin} [" 153 + count_str = f"] {self.completed}/{self.total} ({pct:.0f}%) {speed:.1f}/s" 154 + 155 + if self.total_conflicts > 0: 156 + activity_level = min(max(conflict_rate / 50000, 0), 1.0) 157 + conflict_str = f" {fmt_num(self.total_conflicts)}" 158 + else: 159 + activity_level = 0 160 + conflict_str = "" 161 + 162 + # Calculate available space for bars 163 + fixed_len = len(prefix) + len(count_str) + len(conflict_str) + 4 # +4 for " []" around activity 164 + available = term_width - fixed_len - 2 # -2 for safety margin 165 + 166 + if available < 10: 167 + # Too narrow, minimal display 168 + content = f" {spin} {self.completed}/{self.total} {fmt_num(self.total_conflicts)}" 169 + else: 170 + # Split available space: 70% progress bar, 30% activity bar 171 + if self.total_conflicts > 0: 172 + progress_width = int(available * 0.65) 173 + activity_width = available - progress_width 174 + else: 175 + progress_width = available 176 + activity_width = 0 177 + 178 + # Progress bar 179 + filled = int(progress_width * self.completed / self.total) if self.total > 0 else 0 180 + bar = "█" * filled + "░" * (progress_width - filled) 181 + 182 + # Activity bar 183 + if activity_width > 0: 184 + activity_filled = int(activity_width * activity_level) 185 + activity_bar = f" [{CYAN}{'▮' * activity_filled}{'▯' * (activity_width - activity_filled)}{RESET}]{conflict_str}" 186 + else: 187 + activity_bar = "" 188 + 189 + content = f"{prefix}{bar}{count_str}{activity_bar}" 190 + 191 + line = f"\r{content}{CLEAR_LINE}" 192 + sys.stdout.write(line) 193 + sys.stdout.flush() 194 + 195 + spin_idx += 1 196 + time.sleep(0.1) 197 + 198 + 199 + def progress_bar(current, total, width=30, label=""): 200 + """Generate a progress bar string.""" 201 + filled = int(width * current / total) if total > 0 else 0 202 + bar = "█" * filled + "░" * (width - filled) 203 + pct = 100 * current / total if total > 0 else 0 204 + return f"{label}[{bar}] {current}/{total} ({pct:.0f}%)" 205 + 206 + 207 + def try_config_with_stats(n2, n3, n4, use_complements, restrict_functions, stats_queue): 208 + """Try a single (n2, n3, n4) configuration with stats reporting.""" 18 209 cost = n2 * 2 + n3 * 3 + n4 * 4 19 210 n_gates = n2 + n3 + n4 211 + config_str = f"{n2}x2+{n3}x3+{n4}x4" 20 212 21 213 if n_gates < 7: 22 - return None, cost, f"Skipped (only {n_gates} gates)" 214 + return None, cost, f"Skipped (only {n_gates} gates)", (n2, n3, n4) 215 + 216 + from pysat.formula import CNF 217 + from pysat.solvers import Solver 23 218 24 219 solver = BCDTo7SegmentSolver() 25 220 solver.generate_prime_implicants() 26 221 222 + start = time.time() 27 223 try: 28 - result = solver._try_general_synthesis(n2, n3, n4, use_complements, restrict_functions) 29 - if result: 30 - return result, cost, "SUCCESS" 31 - else: 32 - return None, cost, "UNSAT" 224 + # Build the CNF without solving 225 + cnf = solver._build_general_cnf(n2, n3, n4, use_complements, restrict_functions) 226 + if cnf is None: 227 + return None, cost, f"UNSAT (no valid config)", (n2, n3, n4) 228 + 229 + n_vars = cnf['n_vars'] 230 + n_clauses = len(cnf['clauses']) 231 + 232 + # Report initial stats 233 + if stats_queue: 234 + try: 235 + stats_queue.put_nowait({ 236 + 'config': config_str, 237 + 'phase': 'solving', 238 + 'vars': n_vars, 239 + 'clauses': n_clauses, 240 + 'conflicts': 0, 241 + 'decisions': 0, 242 + }) 243 + except: 244 + pass 245 + 246 + # Solve with periodic stats updates 247 + with Solver(name='g3', bootstrap_with=CNF(from_clauses=cnf['clauses'])) as sat_solver: 248 + # Use solve_limited with conflict budget for progress updates 249 + conflict_budget = 10000 250 + total_conflicts = 0 251 + total_decisions = 0 252 + 253 + while True: 254 + sat_solver.conf_budget(conflict_budget) 255 + status = sat_solver.solve_limited() 256 + 257 + stats = sat_solver.accum_stats() 258 + total_conflicts = stats.get('conflicts', 0) 259 + total_decisions = stats.get('decisions', 0) 260 + 261 + if stats_queue: 262 + try: 263 + stats_queue.put_nowait({ 264 + 'config': config_str, 265 + 'phase': 'solving', 266 + 'vars': n_vars, 267 + 'clauses': n_clauses, 268 + 'conflicts': total_conflicts, 269 + 'decisions': total_decisions, 270 + }) 271 + except: 272 + pass 273 + 274 + if status is not None: 275 + # Solved (True = SAT, False = UNSAT) 276 + break 277 + # status is None means budget exhausted, continue 278 + 279 + elapsed = time.time() - start 280 + 281 + if status: 282 + model = set(sat_solver.get_model()) 283 + result = solver._decode_general_solution_from_cnf(model, cnf) 284 + return result, cost, f"SAT ({elapsed:.1f}s, {total_conflicts} conflicts)", (n2, n3, n4) 285 + else: 286 + return None, cost, f"UNSAT ({elapsed:.1f}s, {total_conflicts} conflicts)", (n2, n3, n4) 287 + 33 288 except Exception as e: 34 - return None, cost, f"Error: {e}" 289 + import traceback 290 + elapsed = time.time() - start 291 + return None, cost, f"Error ({elapsed:.1f}s): {e}", (n2, n3, n4) 292 + 293 + 294 + def try_config(args): 295 + """Try a single (n2, n3, n4) configuration. Run in separate process.""" 296 + n2, n3, n4, use_complements, restrict_functions, stats_queue = args 297 + return try_config_with_stats(n2, n3, n4, use_complements, restrict_functions, stats_queue) 35 298 36 299 37 300 def verify_result(result): ··· 75 338 76 339 77 340 def main(): 78 - print("=" * 60) 79 - print("BCD to 7-Segment Optimal Circuit Search (with 4-input gates)") 80 - print("=" * 60) 341 + print(f"{BOLD}{'=' * 60}{RESET}") 342 + print(f"{BOLD}BCD to 7-Segment Optimal Circuit Search (with 4-input gates){RESET}") 343 + print(f"{BOLD}{'=' * 60}{RESET}") 81 344 print() 82 - print("Gates: AND, OR, XOR, XNOR, NAND, NOR (2, 3, and 4 input variants)") 83 - print("Primary input complements (A', B', C', D') are free") 345 + print(f"Gates: AND, OR, XOR, XNOR, NAND, NOR (2, 3, and 4 input variants)") 346 + print(f"Primary input complements (A', B', C', D') are free") 84 347 print() 85 348 86 349 # Generate configurations sorted by cost ··· 91 354 cost = n2 * 2 + n3 * 3 + n4 * 4 92 355 n_gates = n2 + n3 + n4 93 356 # Need at least 7 gates for 7 outputs 94 - # Limit to reasonable ranges 95 357 if 7 <= n_gates <= 11 and 14 <= cost <= 22: 96 358 configs.append((n2, n3, n4, True, True)) 97 359 98 360 # Sort by cost, then by number of gates 99 361 configs.sort(key=lambda x: (x[0]*2 + x[1]*3 + x[2]*4, x[0]+x[1]+x[2])) 100 362 101 - print(f"Searching {len(configs)} configurations from {min(c[0]*2+c[1]*3+c[2]*4 for c in configs)} to {max(c[0]*2+c[1]*3+c[2]*4 for c in configs)} inputs") 363 + # Group configs by cost 364 + cost_groups = {} 365 + for cfg in configs: 366 + cost = cfg[0] * 2 + cfg[1] * 3 + cfg[2] * 4 367 + if cost not in cost_groups: 368 + cost_groups[cost] = [] 369 + cost_groups[cost].append(cfg) 370 + 371 + min_cost = min(cost_groups.keys()) 372 + max_cost = max(cost_groups.keys()) 373 + 374 + print(f"Searching {len(configs)} configurations from {min_cost} to {max_cost} inputs") 102 375 print(f"Using {mp.cpu_count()} CPU cores") 103 376 print() 104 377 105 378 best_result = None 106 379 best_cost = float('inf') 107 380 108 - start_time = time.time() 381 + total_start = time.time() 382 + configs_tested = 0 383 + total_configs = len(configs) 109 384 110 - # Group configs by cost 111 - cost_groups = {} 112 - for cfg in configs: 113 - cost = cfg[0] * 2 + cfg[1] * 3 + cfg[2] * 4 114 - if cost not in cost_groups: 115 - cost_groups[cost] = [] 116 - cost_groups[cost].append(cfg) 385 + # Create shared queue for stats 386 + manager = Manager() 387 + stats_queue = manager.Queue() 388 + 389 + progress = ProgressDisplay(stats_queue) 117 390 118 391 with ProcessPoolExecutor(max_workers=mp.cpu_count()) as executor: 119 392 for cost in sorted(cost_groups.keys()): ··· 121 394 continue 122 395 123 396 group = cost_groups[cost] 124 - print(f"Trying {cost} inputs ({len(group)} configurations)...", flush=True) 397 + group_size = len(group) 398 + group_start = time.time() 399 + completed_in_group = 0 125 400 126 - futures = {executor.submit(try_config, cfg): cfg for cfg in group} 401 + print(f"\n{CYAN}{BOLD}Testing {cost} inputs{RESET} ({group_size} configurations)") 402 + print("-" * 50) 403 + 404 + # Start async progress display 405 + progress.start(group_size, cost) 406 + 407 + # Add stats_queue to each config 408 + configs_with_queue = [(cfg[0], cfg[1], cfg[2], cfg[3], cfg[4], stats_queue) for cfg in group] 409 + futures = {executor.submit(try_config, cfg): cfg for cfg in configs_with_queue} 410 + found_solution = False 127 411 128 412 for future in as_completed(futures): 129 413 cfg = futures[future] 130 - n2, n3, n4 = cfg[0], cfg[1], cfg[2] 414 + n2, n3, n4 = cfg[0], cfg[1], cfg[2] # First 3 elements are gate counts 415 + completed_in_group += 1 416 + configs_tested += 1 417 + config_str = f"{n2}x2+{n3}x3+{n4}x4" 131 418 132 419 try: 133 - result, result_cost, status = future.result(timeout=300) 420 + result, result_cost, status, _ = future.result(timeout=300) 421 + 422 + # Update progress (always, even for UNSAT) 423 + progress.update(completed_in_group, config_str) 134 424 135 425 if result is not None: 426 + # Found a potential solution - stop progress to print 136 427 valid, msg = verify_result(result) 428 + progress.stop() 137 429 if valid: 138 - print(f" {n2}x2 + {n3}x3 + {n4}x4 = {result_cost}: {status} (verified)") 430 + print(f"\n {GREEN}✓ {n2}x2 + {n3}x3 + {n4}x4{RESET}: {status} {GREEN}(VERIFIED){RESET}") 139 431 if result_cost < best_cost: 140 432 best_result = result 141 433 best_cost = result_cost 434 + found_solution = True 142 435 for f in futures: 143 436 f.cancel() 144 437 break 145 438 else: 146 - print(f" {n2}x2 + {n3}x3 + {n4}x4 = {result_cost}: INVALID - {msg}") 147 - else: 148 - print(f" {n2}x2 + {n3}x3 + {n4}x4 = {result_cost}: {status}") 439 + print(f"\n {YELLOW}✗ {n2}x2 + {n3}x3 + {n4}x4{RESET}: INVALID - {msg}") 440 + # Restart progress 441 + progress.start(group_size, cost) 442 + progress.update(completed_in_group, config_str) 443 + # For UNSAT: just continue, progress bar updates automatically 149 444 150 445 except Exception as e: 151 - print(f" {n2}x2 + {n3}x3 + {n4}x4: Error - {e}") 446 + progress.stop() 447 + print(f"\n {n2}x2 + {n3}x3 + {n4}x4: Error - {e}") 448 + progress.start(group_size, cost) 449 + progress.update(completed_in_group) 450 + 451 + # Stop progress and print summary 452 + progress.stop() 453 + group_elapsed = time.time() - group_start 454 + 455 + if not found_solution: 456 + print(f" {YELLOW}✗ All {group_size} configurations UNSAT{RESET} ({group_elapsed:.1f}s, {progress.total_conflicts} conflicts)") 152 457 153 458 if best_result is not None and best_cost <= cost: 154 - print(f"\nFound solution at {best_cost} inputs, stopping search.") 459 + print(f"\n{GREEN}{BOLD}Found solution at {best_cost} inputs!{RESET}") 155 460 break 156 461 157 - elapsed = time.time() - start_time 462 + total_elapsed = time.time() - total_start 158 463 159 464 print() 160 - print("=" * 60) 161 - print("RESULTS") 162 - print("=" * 60) 163 - print(f"Search time: {elapsed:.1f} seconds") 465 + print(f"{BOLD}{'=' * 60}{RESET}") 466 + print(f"{BOLD}RESULTS{RESET}") 467 + print(f"{BOLD}{'=' * 60}{RESET}") 468 + print(f"Search time: {total_elapsed:.1f} seconds ({configs_tested} configurations tested)") 469 + print(f"Average speed: {configs_tested/total_elapsed:.2f} configurations/second") 164 470 165 471 if best_result: 166 - print(f"Best solution: {best_cost} gate inputs") 472 + print(f"\n{GREEN}{BOLD}Best solution: {best_cost} gate inputs{RESET}") 167 473 print() 168 474 print("Gates:") 169 475 ··· 189 495 for seg in SEGMENT_NAMES: 190 496 print(f" {seg} = {node_names[best_result.output_map[seg]]}") 191 497 else: 192 - print("No solution found in the search range.") 498 + print(f"\n{YELLOW}No solution found in the search range (14-22 inputs).{RESET}") 499 + print("The minimum is likely 23 inputs (7x2 + 3x3 configuration).") 193 500 194 501 195 502 if __name__ == "__main__":