Add mixed 2/3-input gate synthesis and 23-input solution · dunkirk.sh/bcd-optimization@9cbef4a

+82

bcd_23input.dot

··· 1 + digraph BCD_7Seg { 2 + label="BCD to 7-Segment Decoder\n23 gate inputs (7x2-input + 3x3-input)\nUsing: AND, OR, XOR, NAND, NOR"; 3 + labelloc="t"; 4 + fontsize=16; 5 + rankdir=LR; 6 + splines=ortho; 7 + nodesep=0.5; 8 + ranksep=1.0; 9 + 10 + subgraph cluster_inputs { 11 + label="Inputs"; 12 + style=dashed; 13 + A [shape=circle, style=filled, fillcolor=lightblue, label="A"]; 14 + B [shape=circle, style=filled, fillcolor=lightblue, label="B"]; 15 + C [shape=circle, style=filled, fillcolor=lightblue, label="C"]; 16 + D [shape=circle, style=filled, fillcolor=lightblue, label="D"]; 17 + nA [shape=circle, style=filled, fillcolor=lightcyan, label="A'"]; 18 + nB [shape=circle, style=filled, fillcolor=lightcyan, label="B'"]; 19 + nC [shape=circle, style=filled, fillcolor=lightcyan, label="C'"]; 20 + nD [shape=circle, style=filled, fillcolor=lightcyan, label="D'"]; 21 + } 22 + 23 + subgraph cluster_gates { 24 + label="Logic Gates"; 25 + style=dashed; 26 + g0 [shape=box, style=filled, fillcolor=lightyellow, label="XOR"]; 27 + g1 [shape=box, style=filled, fillcolor=lightsalmon, label="OR"]; 28 + g2 [shape=box, style=filled, fillcolor=lightyellow, label="XOR"]; 29 + g3 [shape=box, style=filled, fillcolor=lightsalmon, label="OR"]; 30 + g4 [shape=box, style=filled, fillcolor=lightgreen, label="AND"]; 31 + g5 [shape=box, style=filled, fillcolor=lightsalmon, label="OR"]; 32 + g6 [shape=box, style=filled, fillcolor=palegreen, label="NAND"]; 33 + g7 [shape=box, style=filled, fillcolor=coral, label="OR3"]; 34 + g8 [shape=box, style=filled, fillcolor=khaki, label="XOR3"]; 35 + g9 [shape=box, style=filled, fillcolor=khaki, label="XOR3"]; 36 + } 37 + 38 + // Connections 39 + A -> g0; 40 + C -> g0; 41 + nD -> g1; 42 + g0 -> g1; 43 + B -> g2; 44 + g1 -> g2; 45 + g0 -> g3; 46 + g2 -> g3; 47 + nD -> g4; 48 + g3 -> g4; 49 + g2 -> g5; 50 + g4 -> g5; 51 + B -> g6; 52 + g5 -> g6; 53 + B -> g7; 54 + D -> g7; 55 + nC -> g7; 56 + nC -> g8; 57 + g1 -> g8; 58 + g6 -> g8; 59 + g0 -> g9; 60 + g1 -> g9; 61 + g5 -> g9; 62 + 63 + subgraph cluster_outputs { 64 + label="Outputs"; 65 + style=dashed; 66 + out_a [shape=doublecircle, style=filled, fillcolor=lightpink, label="a"]; 67 + out_b [shape=doublecircle, style=filled, fillcolor=lightpink, label="b"]; 68 + out_c [shape=doublecircle, style=filled, fillcolor=lightpink, label="c"]; 69 + out_d [shape=doublecircle, style=filled, fillcolor=lightpink, label="d"]; 70 + out_e [shape=doublecircle, style=filled, fillcolor=lightpink, label="e"]; 71 + out_f [shape=doublecircle, style=filled, fillcolor=lightpink, label="f"]; 72 + out_g [shape=doublecircle, style=filled, fillcolor=lightpink, label="g"]; 73 + } 74 + 75 + g3 -> out_a; 76 + g6 -> out_b; 77 + g7 -> out_c; 78 + g5 -> out_d; 79 + g4 -> out_e; 80 + g8 -> out_f; 81 + g9 -> out_g; 82 + }

bcd_23input.png

This is a binary file and will not be displayed.

+47 -7

bcd_optimization/export.py

··· 486 486 return expressions.get(func, f"/* unknown func {func} */") 487 487 488 488 489 + def _decompose_gate_function(func: int) -> tuple[str, bool, bool]: 490 + """ 491 + Decompose a 4-bit gate function into base gate type and input inversions. 492 + 493 + Returns: (gate_type, input1_inverted, input2_inverted) 494 + """ 495 + decomposition = { 496 + 0b0000: ("CONST0", False, False), 497 + 0b0001: ("NOR", False, False), 498 + 0b0010: ("AND", True, False), # !A & B 499 + 0b0011: ("BUF", True, False), # !A (ignore B) 500 + 0b0100: ("AND", False, True), # A & !B 501 + 0b0101: ("BUF", False, True), # !B (ignore A) 502 + 0b0110: ("XOR", False, False), 503 + 0b0111: ("NAND", False, False), 504 + 0b1000: ("AND", False, False), 505 + 0b1001: ("XNOR", False, False), 506 + 0b1010: ("BUF", False, False), # B (ignore A) 507 + 0b1011: ("OR", True, False), # !A | B 508 + 0b1100: ("BUF", False, False), # A (ignore B) 509 + 0b1101: ("OR", False, True), # A | !B 510 + 0b1110: ("OR", False, False), 511 + 0b1111: ("CONST1", False, False), 512 + } 513 + return decomposition.get(func, ("???", False, False)) 514 + 515 + 489 516 def to_dot_exact(result: SynthesisResult, title: str = "BCD to 7-Segment Decoder") -> str: 490 517 """ 491 518 Export exact synthesis result as Graphviz DOT format. ··· 525 552 lines.append(' }') 526 553 lines.append("") 527 554 528 - # Gate nodes 555 + # Gate nodes - color by base gate type 529 556 lines.append(' // Gates') 530 557 lines.append(' subgraph cluster_gates {') 531 558 lines.append(' label="Logic Gates";') ··· 536 563 'AND': 'lightgreen', 537 564 'OR': 'lightsalmon', 538 565 'XOR': 'lightyellow', 539 - 'XNOR': 'lightyellow', 566 + 'XNOR': 'khaki', 540 567 'NAND': 'palegreen', 541 568 'NOR': 'peachpuff', 569 + 'BUF': 'lightgray', 570 + 'CONST0': 'white', 571 + 'CONST1': 'white', 542 572 } 543 573 574 + # Pre-compute gate decompositions 575 + gate_decomp = {} 544 576 for gate in result.gates: 577 + base_type, inv1, inv2 = _decompose_gate_function(gate.func) 578 + gate_decomp[gate.index] = (base_type, inv1, inv2) 545 579 node_names.append(f"g{gate.index}") 546 - color = gate_colors.get(gate.func_name, 'lightgray') 547 - lines.append(f' g{gate.index} [shape=box, style=filled, fillcolor={color}, label="{gate.func_name}"];') 580 + color = gate_colors.get(base_type, 'lightgray') 581 + lines.append(f' g{gate.index} [shape=box, style=filled, fillcolor={color}, label="{base_type}"];') 548 582 lines.append(' }') 549 583 lines.append("") 550 584 551 - # Gate connections 585 + # Gate connections with inversion markers on edges 552 586 lines.append(' // Gate input connections') 553 587 node_names_lookup = ['A', 'B', 'C', 'D'] + [f"g{g.index}" for g in result.gates] 554 588 for gate in result.gates: 589 + base_type, inv1, inv2 = gate_decomp[gate.index] 555 590 in1 = node_names_lookup[gate.input1] 556 591 in2 = node_names_lookup[gate.input2] 557 - lines.append(f' {in1} -> g{gate.index};') 558 - lines.append(f' {in2} -> g{gate.index};') 592 + 593 + # Add inversion indicator as edge label 594 + label1 = " [taillabel=\"'\", labeldistance=2]" if inv1 else "" 595 + label2 = " [taillabel=\"'\", labeldistance=2]" if inv2 else "" 596 + 597 + lines.append(f' {in1} -> g{gate.index}{label1};') 598 + lines.append(f' {in2} -> g{gate.index}{label2};') 559 599 lines.append("") 560 600 561 601 # Output nodes

+374 -10

bcd_optimization/solver.py

··· 246 246 cost_breakdown=cost_breakdown, 247 247 ) 248 248 249 - def exact_synthesis(self, max_gates: int = 15, min_gates: int = 1) -> SynthesisResult: 249 + def exact_synthesis(self, max_gates: int = 15, min_gates: int = 1, use_complements: bool = False) -> SynthesisResult: 250 250 """ 251 251 Phase 3: SAT-based exact synthesis for provably optimal circuits. 252 252 253 253 Encodes the circuit synthesis problem as SAT and iteratively searches 254 254 for the minimum number of gates. 255 + 256 + Args: 257 + max_gates: Maximum number of gates to try 258 + min_gates: Minimum number of gates to start from 259 + use_complements: If True, include A',B',C',D' as free inputs 255 260 """ 256 261 import sys 262 + complement_str = " (with complements)" if use_complements else "" 257 263 for num_gates in range(min_gates, max_gates + 1): 258 - print(f" Trying {num_gates} gates...", flush=True) 264 + print(f" Trying {num_gates} gates{complement_str}...", flush=True) 259 265 sys.stdout.flush() 260 - result = self._try_exact_synthesis(num_gates) 266 + result = self._try_exact_synthesis(num_gates, use_complements) 261 267 if result is not None: 262 268 return result 263 269 264 270 raise RuntimeError(f"No solution found with up to {max_gates} gates") 265 271 266 - def _try_exact_synthesis(self, num_gates: int) -> Optional[SynthesisResult]: 272 + def exact_synthesis_mixed(self, max_inputs: int = 24, use_complements: bool = True) -> SynthesisResult: 273 + """ 274 + SAT-based exact synthesis with mixed 2-input and 3-input gates. 275 + 276 + Searches for circuits with total gate inputs <= max_inputs. 277 + """ 278 + import sys 279 + 280 + # Try different combinations of 2-input and 3-input gates 281 + # Cost = 2*n2 + 3*n3, want to minimize while finding valid circuit 282 + best_result = None 283 + 284 + for total_cost in range(14, max_inputs + 1): # Start from reasonable minimum 285 + print(f" Trying circuits with {total_cost} total inputs...", flush=True) 286 + 287 + # Try all valid (n2, n3) combinations for this cost 288 + for n3 in range(total_cost // 3 + 1): 289 + remaining = total_cost - 3 * n3 290 + if remaining >= 0 and remaining % 2 == 0: 291 + n2 = remaining // 2 292 + if n2 + n3 >= 7: # Need at least 7 gates for 7 outputs 293 + result = self._try_mixed_synthesis(n2, n3, use_complements) 294 + if result is not None: 295 + return result 296 + 297 + raise RuntimeError(f"No solution found with up to {max_inputs} gate inputs") 298 + 299 + def _try_mixed_synthesis(self, num_2input: int, num_3input: int, use_complements: bool = True, restrict_functions: bool = True) -> Optional[SynthesisResult]: 300 + """Try synthesis with a specific mix of 2-input and 3-input gates.""" 301 + n_primary = 4 302 + n_inputs = 8 if use_complements else 4 303 + n_outputs = 7 304 + n_gates = num_2input + num_3input 305 + n_nodes = n_inputs + n_gates 306 + 307 + truth_rows = list(range(10)) 308 + n_rows = len(truth_rows) 309 + 310 + cnf = CNF() 311 + var_counter = [1] 312 + 313 + def new_var(): 314 + v = var_counter[0] 315 + var_counter[0] += 1 316 + return v 317 + 318 + # x[i][t] = output of node i on row t 319 + x = {i: {t: new_var() for t in range(n_rows)} for i in range(n_nodes)} 320 + 321 + # For 2-input gates: s2[i][j][k] = gate i uses inputs j, k 322 + # For 3-input gates: s3[i][j][k][l] = gate i uses inputs j, k, l 323 + s2 = {} 324 + s3 = {} 325 + f2 = {} # 4-bit function for 2-input gates 326 + f3 = {} # 8-bit function for 3-input gates 327 + 328 + # Gate type: is_3input[i] = True if gate i is 3-input 329 + is_3input = {} 330 + 331 + # First num_2input gates are 2-input, rest are 3-input 332 + for gate_idx in range(n_gates): 333 + i = n_inputs + gate_idx 334 + if gate_idx < num_2input: 335 + # 2-input gate 336 + s2[i] = {} 337 + for j in range(i): 338 + s2[i][j] = {k: new_var() for k in range(j + 1, i)} 339 + f2[i] = {p: {q: new_var() for q in range(2)} for p in range(2)} 340 + else: 341 + # 3-input gate 342 + s3[i] = {} 343 + for j in range(i): 344 + s3[i][j] = {} 345 + for k in range(j + 1, i): 346 + s3[i][j][k] = {l: new_var() for l in range(k + 1, i)} 347 + # 8-bit function table for 3 inputs 348 + f3[i] = {p: {q: {r: new_var() for r in range(2)} for q in range(2)} for p in range(2)} 349 + 350 + # g[h][i] = output h comes from node i 351 + g = {h: {i: new_var() for i in range(n_nodes)} for h in range(n_outputs)} 352 + 353 + # Constraint 1: Primary inputs fixed by truth table 354 + for t_idx, t in enumerate(truth_rows): 355 + for i in range(n_primary): 356 + bit = (t >> (n_primary - 1 - i)) & 1 357 + cnf.append([x[i][t_idx] if bit else -x[i][t_idx]]) 358 + if use_complements: 359 + for i in range(n_primary): 360 + bit = (t >> (n_primary - 1 - i)) & 1 361 + cnf.append([x[n_primary + i][t_idx] if not bit else -x[n_primary + i][t_idx]]) 362 + 363 + # Constraint 2: Each gate has exactly one input selection 364 + for gate_idx in range(n_gates): 365 + i = n_inputs + gate_idx 366 + if gate_idx < num_2input: 367 + all_sels = [s2[i][j][k] for j in range(i) for k in range(j + 1, i)] 368 + else: 369 + 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)] 370 + 371 + cnf.append(all_sels) # At least one 372 + for idx1, sel1 in enumerate(all_sels): 373 + for sel2 in all_sels[idx1 + 1:]: 374 + cnf.append([-sel1, -sel2]) # At most one 375 + 376 + # Constraint 3: Gate function consistency 377 + for gate_idx in range(n_gates): 378 + i = n_inputs + gate_idx 379 + if gate_idx < num_2input: 380 + # 2-input gate 381 + for j in range(i): 382 + for k in range(j + 1, i): 383 + for t_idx in range(n_rows): 384 + for pv in range(2): 385 + for qv in range(2): 386 + for outv in range(2): 387 + clause = [-s2[i][j][k]] 388 + clause.append(-x[j][t_idx] if pv else x[j][t_idx]) 389 + clause.append(-x[k][t_idx] if qv else x[k][t_idx]) 390 + clause.append(-f2[i][pv][qv] if outv else f2[i][pv][qv]) 391 + clause.append(x[i][t_idx] if outv else -x[i][t_idx]) 392 + cnf.append(clause) 393 + else: 394 + # 3-input gate 395 + for j in range(i): 396 + for k in range(j + 1, i): 397 + for l in range(k + 1, i): 398 + for t_idx in range(n_rows): 399 + for pv in range(2): 400 + for qv in range(2): 401 + for rv in range(2): 402 + for outv in range(2): 403 + clause = [-s3[i][j][k][l]] 404 + clause.append(-x[j][t_idx] if pv else x[j][t_idx]) 405 + clause.append(-x[k][t_idx] if qv else x[k][t_idx]) 406 + clause.append(-x[l][t_idx] if rv else x[l][t_idx]) 407 + clause.append(-f3[i][pv][qv][rv] if outv else f3[i][pv][qv][rv]) 408 + clause.append(x[i][t_idx] if outv else -x[i][t_idx]) 409 + cnf.append(clause) 410 + 411 + # Constraint 3b: Restrict to standard gate functions 412 + if restrict_functions: 413 + # 2-input: AND, OR, XOR, NAND, NOR (no XNOR - use XOR+INV if needed) 414 + allowed_2input = [0b1000, 0b1110, 0b0110, 0b0111, 0b0001] 415 + for gate_idx in range(num_2input): 416 + i = n_inputs + gate_idx 417 + or_clause = [] 418 + for func in allowed_2input: 419 + match_var = new_var() 420 + or_clause.append(match_var) 421 + for p in range(2): 422 + for q in range(2): 423 + bit_idx = p * 2 + q 424 + expected = (func >> bit_idx) & 1 425 + if expected: 426 + cnf.append([-match_var, f2[i][p][q]]) 427 + else: 428 + cnf.append([-match_var, -f2[i][p][q]]) 429 + cnf.append(or_clause) 430 + 431 + # 3-input: AND3, OR3, XOR3, NAND3, NOR3 (user's available gates) 432 + allowed_3input = [ 433 + 0b10000000, # AND3 434 + 0b11111110, # OR3 435 + 0b01111111, # NAND3 436 + 0b00000001, # NOR3 437 + 0b10010110, # XOR3 (odd parity) 438 + ] 439 + for gate_idx in range(num_2input, num_2input + num_3input): 440 + i = n_inputs + gate_idx 441 + or_clause = [] 442 + for func in allowed_3input: 443 + match_var = new_var() 444 + or_clause.append(match_var) 445 + for p in range(2): 446 + for q in range(2): 447 + for r in range(2): 448 + bit_idx = p * 4 + q * 2 + r 449 + expected = (func >> bit_idx) & 1 450 + if expected: 451 + cnf.append([-match_var, f3[i][p][q][r]]) 452 + else: 453 + cnf.append([-match_var, -f3[i][p][q][r]]) 454 + cnf.append(or_clause) 455 + 456 + # Constraint 4: Each output assigned to exactly one node 457 + for h in range(n_outputs): 458 + cnf.append([g[h][i] for i in range(n_nodes)]) 459 + for i in range(n_nodes): 460 + for j in range(i + 1, n_nodes): 461 + cnf.append([-g[h][i], -g[h][j]]) 462 + 463 + # Constraint 5: Output correctness 464 + for h, segment in enumerate(SEGMENT_NAMES): 465 + for t_idx, t in enumerate(truth_rows): 466 + expected = 1 if t in SEGMENT_MINTERMS[segment] else 0 467 + for i in range(n_nodes): 468 + if expected: 469 + cnf.append([-g[h][i], x[i][t_idx]]) 470 + else: 471 + cnf.append([-g[h][i], -x[i][t_idx]]) 472 + 473 + # Solve 474 + with Solver(bootstrap_with=cnf) as solver: 475 + if solver.solve(): 476 + model = set(solver.get_model()) 477 + return self._decode_mixed_solution( 478 + model, num_2input, num_3input, n_inputs, n_nodes, 479 + x, s2, s3, f2, f3, g, use_complements 480 + ) 481 + return None 482 + 483 + def _decode_mixed_solution(self, model, num_2input, num_3input, n_inputs, n_nodes, 484 + x, s2, s3, f2, f3, g, use_complements) -> SynthesisResult: 485 + """Decode SAT solution for mixed gate sizes.""" 486 + def is_true(var): 487 + return var in model 488 + 489 + if use_complements: 490 + node_names = ['A', 'B', 'C', 'D', "A'", "B'", "C'", "D'"] + [f'g{i}' for i in range(num_2input + num_3input)] 491 + else: 492 + node_names = ['A', 'B', 'C', 'D'] + [f'g{i}' for i in range(num_2input + num_3input)] 493 + 494 + gates = [] 495 + n_gates = num_2input + num_3input 496 + 497 + for gate_idx in range(n_gates): 498 + i = n_inputs + gate_idx 499 + if gate_idx < num_2input: 500 + # 2-input gate 501 + for j in range(i): 502 + for k in range(j + 1, i): 503 + if is_true(s2[i][j][k]): 504 + func = 0 505 + for p in range(2): 506 + for q in range(2): 507 + if is_true(f2[i][p][q]): 508 + func |= (1 << (p * 2 + q)) 509 + func_name = self._decode_gate_function(func) 510 + gates.append(GateInfo( 511 + index=gate_idx, 512 + input1=j, 513 + input2=k, 514 + func=func, 515 + func_name=func_name, 516 + )) 517 + expr = f"({node_names[j]} {func_name} {node_names[k]})" 518 + node_names[i] = expr 519 + break 520 + else: 521 + # 3-input gate 522 + for j in range(i): 523 + for k in range(j + 1, i): 524 + for l in range(k + 1, i): 525 + if is_true(s3[i][j][k][l]): 526 + func = 0 527 + for p in range(2): 528 + for q in range(2): 529 + for r in range(2): 530 + if is_true(f3[i][p][q][r]): 531 + func |= (1 << (p * 4 + q * 2 + r)) 532 + func_name = self._decode_3input_function(func) 533 + # Store as GateInfo with input2 being a tuple indicator 534 + gates.append(GateInfo( 535 + index=gate_idx, 536 + input1=j, 537 + input2=(k, l), # Pack two inputs 538 + func=func, 539 + func_name=func_name, 540 + )) 541 + expr = f"({node_names[j]} {func_name} {node_names[k]} {node_names[l]})" 542 + node_names[i] = expr 543 + break 544 + 545 + # Map outputs 546 + output_map = {} 547 + expressions = {} 548 + for h, segment in enumerate(SEGMENT_NAMES): 549 + for i in range(n_nodes): 550 + if is_true(g[h][i]): 551 + output_map[segment] = i 552 + expressions[segment] = node_names[i] 553 + break 554 + 555 + total_cost = 2 * num_2input + 3 * num_3input 556 + cost_breakdown = CostBreakdown( 557 + and_inputs=total_cost, 558 + or_inputs=0, 559 + num_and_gates=num_2input + num_3input, 560 + num_or_gates=0, 561 + ) 562 + 563 + return SynthesisResult( 564 + cost=total_cost, 565 + implicants_by_output={}, 566 + shared_implicants=[], 567 + method=f"exact_mixed_{num_2input}x2_{num_3input}x3", 568 + expressions=expressions, 569 + cost_breakdown=cost_breakdown, 570 + gates=gates, 571 + output_map=output_map, 572 + ) 573 + 574 + def _decode_3input_function(self, func: int) -> str: 575 + """Decode 8-bit function for 3-input gate.""" 576 + # Common 3-input functions 577 + known = { 578 + 0b00000001: "NOR3", 579 + 0b01111111: "NAND3", 580 + 0b10000000: "AND3", 581 + 0b11111110: "OR3", 582 + 0b10010110: "XOR3", # Odd parity 583 + 0b01101001: "XNOR3", # Even parity 584 + 0b11101000: "MAJ", # Majority 585 + 0b00010111: "MIN", # Minority 586 + } 587 + return known.get(func, f"F3_{func:08b}") 588 + 589 + def _try_exact_synthesis(self, num_gates: int, use_complements: bool = False, restrict_functions: bool = False) -> Optional[SynthesisResult]: 267 590 """ 268 591 Try to find a circuit with exactly num_gates gates. 269 592 ··· 271 594 - Variables encode gate structure (which inputs each gate uses) 272 595 - Variables encode gate function (AND, OR, NAND, NOR, etc.) 273 596 - Constraints ensure functional correctness on all valid inputs 597 + 598 + Args: 599 + num_gates: Number of 2-input gates to use 600 + use_complements: If True, include A',B',C',D' as free inputs (8 total) 601 + restrict_functions: If True, only allow AND, OR, XOR, NAND, NOR, XNOR 274 602 """ 275 - n_inputs = 4 # A, B, C, D 603 + n_primary = 4 # A, B, C, D 604 + n_inputs = 8 if use_complements else 4 # Include complements if requested 276 605 n_outputs = 7 # a, b, c, d, e, f, g 277 606 n_nodes = n_inputs + num_gates 278 607 ··· 313 642 314 643 # Constraint 1: Primary inputs are fixed by truth table 315 644 for t_idx, t in enumerate(truth_rows): 316 - for i in range(n_inputs): 317 - bit = (t >> (n_inputs - 1 - i)) & 1 645 + # First 4 inputs: A, B, C, D 646 + for i in range(n_primary): 647 + bit = (t >> (n_primary - 1 - i)) & 1 318 648 cnf.append([x[i][t_idx] if bit else -x[i][t_idx]]) 649 + # Next 4 inputs (if using complements): A', B', C', D' 650 + if use_complements: 651 + for i in range(n_primary): 652 + bit = (t >> (n_primary - 1 - i)) & 1 653 + # Complement is the inverse 654 + cnf.append([x[n_primary + i][t_idx] if not bit else -x[n_primary + i][t_idx]]) 319 655 320 656 # Constraint 2: Each gate has exactly one input pair 321 657 for i in range(n_inputs, n_nodes): ··· 344 680 clause.append(x[i][t_idx] if outv else -x[i][t_idx]) 345 681 cnf.append(clause) 346 682 683 + # Constraint 3b: Restrict to standard gate functions (if requested) 684 + # With complements available, we only need symmetric functions 685 + if restrict_functions: 686 + # Allowed: AND(1000), OR(1110), XOR(0110), NAND(0111), NOR(0001), XNOR(1001) 687 + allowed_funcs = [0b1000, 0b1110, 0b0110, 0b0111, 0b0001, 0b1001] 688 + for i in range(n_inputs, n_nodes): 689 + # For each gate, the function must be one of the allowed ones 690 + # Encode as: (func == AND) OR (func == OR) OR ... 691 + or_clause = [] 692 + for func in allowed_funcs: 693 + # Create aux var for "this gate has this function" 694 + match_var = new_var() 695 + or_clause.append(match_var) 696 + # match_var -> all f bits match the function 697 + for p in range(2): 698 + for q in range(2): 699 + bit_idx = p * 2 + q 700 + expected = (func >> bit_idx) & 1 701 + if expected: 702 + cnf.append([-match_var, f[i][p][q]]) 703 + else: 704 + cnf.append([-match_var, -f[i][p][q]]) 705 + # At least one match_var must be true 706 + cnf.append(or_clause) 707 + 347 708 # Constraint 4: Each output assigned to exactly one node 348 709 for h in range(n_outputs): 349 710 cnf.append([g[h][i] for i in range(n_nodes)]) ··· 366 727 if solver.solve(): 367 728 model = set(solver.get_model()) 368 729 return self._decode_exact_solution( 369 - model, num_gates, n_inputs, n_nodes, x, s, f, g 730 + model, num_gates, n_inputs, n_nodes, x, s, f, g, use_complements 370 731 ) 371 732 return None 372 733 373 734 def _decode_exact_solution( 374 - self, model, num_gates, n_inputs, n_nodes, x, s, f, g 735 + self, model, num_gates, n_inputs, n_nodes, x, s, f, g, use_complements: bool = False 375 736 ) -> SynthesisResult: 376 737 """Decode SAT solution into readable circuit description.""" 377 738 378 739 def is_true(var): 379 740 return var in model 380 741 381 - node_names = ['A', 'B', 'C', 'D'] + [f'g{i}' for i in range(num_gates)] 742 + if use_complements: 743 + node_names = ['A', 'B', 'C', 'D', "A'", "B'", "C'", "D'"] + [f'g{i}' for i in range(num_gates)] 744 + else: 745 + node_names = ['A', 'B', 'C', 'D'] + [f'g{i}' for i in range(num_gates)] 382 746 gates = [] 383 747 384 748 for i in range(n_inputs, n_nodes):