Boolean Circuit Minimal Synthesis

synthesis.py

# /// script
# requires-python = ">=3.13"
# dependencies = [
#     "z3-solver",
# ]
# ///

"""
This script finds minimal boolean circuits for a provided boolean function. It supports:
- Multiple output variables (multiple boolean functions computed by the same circuit)
- Any basis for gates

Used by me to generate examples to my blog post about circuit complexity:
https://alon.kr/posts/circuit-complexity

Written with help from claude.ai.
"""

from dataclasses import dataclass
from typing import List, Tuple

from z3 import *


@dataclass
class Gate:
    """Represents a gate type with its truth table."""
    name: str
    num_inputs: int
    truth_table: List[int]  # Truth table as list of outputs, indexed by input combinations
    
    def __post_init__(self):
        expected_size = 2 ** self.num_inputs
        if len(self.truth_table) != expected_size:
            raise ValueError(f"Truth table size {len(self.truth_table)} doesn't match 2^{self.num_inputs} = {expected_size}")
        if not all(x in [0, 1] for x in self.truth_table):
            raise ValueError("Truth table must contain only 0 and 1")


class GeneralBooleanCircuitSynthesizer:
    """
    General boolean circuit synthesizer using Z3.
    Finds minimal circuits using custom gates defined by truth tables.
    """
    
    def __init__(self, num_inputs: int, num_outputs: int, gates: List[Gate], max_gates: int = 20):
        self.num_inputs = num_inputs
        self.num_outputs = num_outputs
        self.gates = gates
        self.max_gates = max_gates
        self.solver = Solver()
        
        # Validate gates
        for gate in gates:
            if gate.num_inputs <= 0:
                raise ValueError(f"Gate {gate.name} must have at least 1 input")
    
    def synthesize(self, truth_table: List[List[int]]) -> bool:
        """
        Synthesize a circuit for the given truth table.
        
        Args:
            truth_table: List of output vectors, where truth_table[i] is the output
                        for input combination i (in binary order).
                        Each output vector has length num_outputs.
        
        Returns:
            True if synthesis succeeded, False otherwise
        """
        self._validate_truth_table(truth_table)
        
        # Try to find solution with minimal gates
        for target_gates in range(1, self.max_gates + 1):
            print(f"Trying with {target_gates} gates...")
            
            if self._try_synthesis(truth_table, target_gates):
                return True
                
        print("No solution found within the gate limit!")
        return False
    
    def _validate_truth_table(self, truth_table: List[List[int]]):
        """Validate that the truth table has correct dimensions and values."""
        expected_rows = 2 ** self.num_inputs
        if len(truth_table) != expected_rows:
            raise ValueError(f"Truth table must have {expected_rows} rows for {self.num_inputs} inputs")
        
        for i, outputs in enumerate(truth_table):
            if len(outputs) != self.num_outputs:
                raise ValueError(f"Row {i} has {len(outputs)} outputs, expected {self.num_outputs}")
            if not all(x in [0, 1] for x in outputs):
                raise ValueError(f"Row {i} contains non-binary values: {outputs}")
    
    def _try_synthesis(self, truth_table: List[List[int]], target_gates: int) -> bool:
        """Try to synthesize circuit with exactly target_gates gates."""
        self.solver.push()
        
        # Decision variables
        gate_vars = self._create_gate_variables(target_gates)
        output_vars = self._create_output_variables()
        
        # Add constraints
        self._add_gate_constraints(gate_vars, target_gates)
        self._add_output_constraints(output_vars, target_gates)
        self._add_truth_table_constraints(gate_vars, output_vars, truth_table, target_gates)
        
        if self.solver.check() == sat:
            print(f"Found solution with {target_gates} gates!")
            self._print_solution(self.solver.model(), gate_vars, output_vars, target_gates)
            self._verify_solution(self.solver.model(), gate_vars, output_vars, truth_table, target_gates)
            self.solver.pop()
            return True
        
        self.solver.pop()
        return False
    
    def _create_gate_variables(self, num_gates: int):
        """Create Z3 variables for gate configuration."""
        gate_vars = {
            'types': [Int(f'gate_type_{i}') for i in range(num_gates)],
            'inputs': []
        }
        
        # Create input variables for each gate
        for i in range(num_gates):
            gate_inputs = []
            max_gate_inputs = max(gate.num_inputs for gate in self.gates)
            for j in range(max_gate_inputs):
                gate_inputs.append(Int(f'gate_{i}_input_{j}'))
            gate_vars['inputs'].append(gate_inputs)
        
        return gate_vars
    
    def _create_output_variables(self):
        """Create Z3 variables for output connections."""
        return [Int(f'output_{i}') for i in range(self.num_outputs)]
    
    def _add_gate_constraints(self, gate_vars, num_gates: int):
        """Add constraints on gate types and connections."""
        for i in range(num_gates):
            # Gate type must be valid
            self.solver.add(gate_vars['types'][i] >= 0)
            self.solver.add(gate_vars['types'][i] < len(self.gates))
            
            # Gate inputs can connect to primary inputs (0 to num_inputs-1) 
            # or previous gate outputs (num_inputs to num_inputs+i-1)
            max_input_id = self.num_inputs + i - 1
            
            for j in range(len(gate_vars['inputs'][i])):
                self.solver.add(gate_vars['inputs'][i][j] >= 0)
                self.solver.add(gate_vars['inputs'][i][j] <= max_input_id)
    
    def _add_output_constraints(self, output_vars, num_gates: int):
        """Add constraints on output connections."""
        for i in range(self.num_outputs):
            self.solver.add(output_vars[i] >= 0)
            self.solver.add(output_vars[i] < self.num_inputs + num_gates)
    
    def _add_truth_table_constraints(self, gate_vars, output_vars, truth_table, num_gates: int):
        """Add constraints ensuring circuit matches truth table."""
        for input_idx in range(len(truth_table)):
            # Convert input index to binary tuple
            input_vals = self._int_to_binary_tuple(input_idx, self.num_inputs)
            expected_outputs = truth_table[input_idx]
            
            # Create boolean variables for gate outputs for this input combination
            gate_outputs = [Bool(f'gate_out_{i}_{input_idx}') for i in range(num_gates)]
            
            # Define gate behavior
            for i in range(num_gates):
                gate_output = self._define_gate_output(
                    gate_vars, i, input_vals, gate_outputs[:i]
                )
                self.solver.add(gate_outputs[i] == gate_output)
            
            # Define circuit outputs
            for out_idx in range(self.num_outputs):
                circuit_output = self._define_circuit_output(
                    output_vars[out_idx], input_vals, gate_outputs
                )
                expected = expected_outputs[out_idx] == 1
                self.solver.add(circuit_output == expected)
    
    def _define_gate_output(self, gate_vars, gate_idx: int, input_vals: Tuple[int, ...], 
                           prev_gate_outputs: List):
        """Define the output of a specific gate given inputs."""
        # Create conditions for each possible gate type
        conditions = []
        
        for gate_type_idx, gate in enumerate(self.gates):
            # Get input values for this gate type
            gate_input_vals = []
            for input_idx in range(gate.num_inputs):
                signal_val = self._get_signal_value(
                    gate_vars['inputs'][gate_idx][input_idx], input_vals, prev_gate_outputs
                )
                gate_input_vals.append(signal_val)
            
            # Create condition for this gate type
            gate_condition = gate_vars['types'][gate_idx] == gate_type_idx
            
            # Create output based on gate's truth table
            gate_output = self._apply_gate_truth_table(gate, gate_input_vals)
            
            conditions.append(And(gate_condition, gate_output))
        
        # At least one condition must be true (exactly one will be due to type constraints)
        return Or(conditions)
    
    def _apply_gate_truth_table(self, gate: Gate, input_vals: List):
        """Apply gate's truth table to input values."""
        # Create conditions for each possible input combination
        conditions = []
        
        for input_combo in range(2 ** gate.num_inputs):
            # Convert input combination to binary
            binary_combo = self._int_to_binary_tuple(input_combo, gate.num_inputs)
            
            # Check if current input values match this combination
            input_match_conditions = []
            for i, bit in enumerate(binary_combo):
                if bit == 1:
                    input_match_conditions.append(input_vals[i])
                else:
                    input_match_conditions.append(Not(input_vals[i]))
            
            input_matches = And(input_match_conditions)
            
            # Get expected output from truth table
            expected_output = gate.truth_table[input_combo] == 1
            
            conditions.append(And(input_matches, expected_output))
        
        return Or(conditions)
    
    def _define_circuit_output(self, output_var, input_vals: Tuple[int, ...], gate_outputs: List):
        """Define a circuit output given the output variable assignment."""
        # Check if output connects to primary input
        conditions = []
        for i in range(self.num_inputs):
            conditions.append(And(output_var == i, input_vals[i] == 1))
        
        # Check if output connects to gate output
        for i in range(len(gate_outputs)):
            conditions.append(And(output_var == self.num_inputs + i, gate_outputs[i]))
        
        return Or(conditions)
    
    def _get_signal_value(self, signal_var, input_vals: Tuple[int, ...], gate_outputs: List):
        """Get the boolean value of a signal (primary input or gate output)."""
        conditions = []
        
        # Primary inputs
        for i in range(self.num_inputs):
            conditions.append(And(signal_var == i, input_vals[i] == 1))
        
        # Gate outputs
        for i in range(len(gate_outputs)):
            conditions.append(And(signal_var == self.num_inputs + i, gate_outputs[i]))
        
        return Or(conditions)
    
    def _int_to_binary_tuple(self, n: int, width: int) -> Tuple[int, ...]:
        """Convert integer to binary tuple (little-endian)."""
        return tuple((n >> i) & 1 for i in range(width))
    
    def _print_solution(self, model, gate_vars, output_vars, num_gates: int):
        """Print the synthesized circuit in readable format."""
        print(f"\nCircuit with {num_gates} gates:")
        print("=" * 50)
        
        # Print gate definitions
        for i in range(num_gates):
            gate_type_idx = model[gate_vars['types'][i]].as_long()
            gate = self.gates[gate_type_idx]
            
            inputs = []
            for j in range(gate.num_inputs):
                input_id = model[gate_vars['inputs'][i][j]].as_long()
                inputs.append(self._signal_name(input_id))
            
            input_str = ", ".join(inputs)
            print(f"g{i} = {gate.name}({input_str})")
        
        # Print outputs
        print(f"\nOutputs:")
        for i in range(self.num_outputs):
            out_connection = model[output_vars[i]].as_long()
            print(f"y{i} = {self._signal_name(out_connection)}")
    
    def _signal_name(self, signal_id: int) -> str:
        """Convert signal ID to readable name."""
        if signal_id < self.num_inputs:
            return f'x{signal_id}'
        else:
            return f'g{signal_id - self.num_inputs}'
    
    def _verify_solution(self, model, gate_vars, output_vars, truth_table, num_gates: int):
        """Verify that the synthesized circuit produces correct outputs."""
        print(f"\nVerification:")
        print(f"{'Input':<15} | {'Expected':<15} | {'Actual':<15} | Match")
        print("-" * 65)
        
        all_correct = True
        for input_idx, expected_outputs in enumerate(truth_table):
            input_vals = self._int_to_binary_tuple(input_idx, self.num_inputs)
            
            # Simulate circuit
            actual_outputs = self._simulate_circuit(model, gate_vars, output_vars, 
                                                  input_vals, num_gates)
            
            match = actual_outputs == expected_outputs
            all_correct = all_correct and match
            
            input_str = "".join(map(str, reversed(input_vals)))
            expected_str = "".join(map(str, expected_outputs))
            actual_str = "".join(map(str, actual_outputs))
            
            print(f"{input_str:<15} | {expected_str:<15} | {actual_str:<15} | {'✓' if match else '✗'}")
        
        print(f"\nOverall: {'✓ CORRECT' if all_correct else '✗ INCORRECT'}")
    
    def _simulate_circuit(self, model, gate_vars, output_vars, input_vals: Tuple[int, ...], 
                         num_gates: int) -> List[int]:
        """Simulate the circuit for given input values."""
        # Compute gate outputs
        gate_vals = [None] * num_gates
        for g in range(num_gates):
            gate_type_idx = model[gate_vars['types'][g]].as_long()
            gate = self.gates[gate_type_idx]
            
            def get_val(signal_id):
                if signal_id < self.num_inputs:
                    return input_vals[signal_id]
                else:
                    return gate_vals[signal_id - self.num_inputs]
            
            # Get input values for this gate
            gate_input_vals = []
            for i in range(gate.num_inputs):
                input_id = model[gate_vars['inputs'][g][i]].as_long()
                gate_input_vals.append(get_val(input_id))
            
            # Compute gate output using truth table
            input_combo = sum(val * (2 ** i) for i, val in enumerate(gate_input_vals))
            gate_vals[g] = gate.truth_table[input_combo]
        
        # Compute outputs
        outputs = []
        for i in range(self.num_outputs):
            out_connection = model[output_vars[i]].as_long()
            if out_connection < self.num_inputs:
                outputs.append(input_vals[out_connection])
            else:
                outputs.append(gate_vals[out_connection - self.num_inputs])
        
        return outputs


# Predefined common gates
def create_standard_gates() -> List[Gate]:
    """Create standard logic gates."""
    return [
        Gate("AND", 2, [0, 0, 0, 1]),      # AND(a,b) = a∧b
        Gate("OR", 2, [0, 1, 1, 1]),       # OR(a,b) = a∨b
        Gate("NOT", 1, [1, 0]),            # NOT(a) = ¬a
        Gate("NAND", 2, [1, 1, 1, 0]),     # NAND(a,b) = ¬(a∧b)
        Gate("NOR", 2, [1, 0, 0, 0]),      # NOR(a,b) = ¬(a∨b)
        Gate("XOR", 2, [0, 1, 1, 0]),      # XOR(a,b) = a⊕b
        Gate("XNOR", 2, [1, 0, 0, 1]),     # XNOR(a,b) = ¬(a⊕b)
    ]


def create_xor_example() -> List[List[int]]:
    """Create truth table for 2-input XOR function."""
    return [
        [0],  # 00 -> 0
        [1],  # 01 -> 1
        [1],  # 10 -> 1
        [0],  # 11 -> 0
    ]


def create_full_adder_example() -> List[List[int]]:
    """Create truth table for full adder (3 inputs: a, b, cin; 2 outputs: sum, cout)."""
    return [
        [0, 0],  # 000 -> sum=0, cout=0
        [1, 0],  # 001 -> sum=1, cout=0
        [1, 0],  # 010 -> sum=1, cout=0
        [0, 1],  # 011 -> sum=0, cout=1
        [1, 0],  # 100 -> sum=1, cout=0
        [0, 1],  # 101 -> sum=0, cout=1
        [0, 1],  # 110 -> sum=0, cout=1
        [1, 1],  # 111 -> sum=1, cout=1
    ]


def main():
    """Example usage: synthesize circuits for different functions."""
    print("General Boolean Circuit Synthesis")
    print("=" * 50)
    
    # Create standard gates
    gates = create_standard_gates()
    
    # Example 1: XOR function
    print("\n1. Synthesizing XOR function:")
    print("Truth table for XOR:")
    xor_table = create_xor_example()
    for i, outputs in enumerate(xor_table):
        input_str = f"{i:02b}"
        output_str = "".join(map(str, outputs))
        print(f"  {input_str} -> {output_str}")
    
    synthesizer = GeneralBooleanCircuitSynthesizer(
        num_inputs=2, num_outputs=1, gates=[Gate("NAND", 2, [1, 1, 1, 0])], max_gates=10
    )
    
    success = synthesizer.synthesize(xor_table)
    if not success:
        print("Failed to synthesize XOR circuit!")
    
    # Example 2: Full Adder
    print("\n\n2. Synthesizing Full Adder:")
    print("Truth table for Full Adder (inputs: a, b, cin; outputs: sum, cout):")
    adder_table = create_full_adder_example()
    for i, outputs in enumerate(adder_table):
        input_str = f"{i:03b}"
        output_str = "".join(map(str, outputs))
        print(f"  {input_str} -> {output_str}")
    
    synthesizer2 = GeneralBooleanCircuitSynthesizer(
        num_inputs=3, num_outputs=2, gates=gates, max_gates=15
    )
    
    success2 = synthesizer2.synthesize(adder_table)
    if not success2:
        print("Failed to synthesize Full Adder circuit!")


if __name__ == "__main__":
    main()