bcd-optimization / spec.md

# Beating 23 gate inputs: Multi-output logic synthesis for BCD to 7-segment decoders

A custom multi-output logic synthesis solver can achieve **18-21 total gate inputs** for the BCD to 7-segment decoder, substantially beating the 23-input baseline. The key insight is that SAT-based exact synthesis combined with aggressive shared term extraction is tractable for this 4-input, 7-output problem size, enabling provably optimal or near-optimal solutions. This report provides concrete algorithms, encodings, and implementation strategies to build such a solver.

## The BCD to 7-segment optimization landscape

The decoder maps 4-bit BCD inputs (0-9 valid, 10-15 don't-care) to 7 segment outputs. Standard K-map minimization yields **27-35 gate inputs** without sharing; the theoretical minimum with full multi-output sharing is approximately **18-20 gate inputs**. The 6 don't-care conditions per output and significant overlap between segment functions create substantial optimization opportunities.

The truth table reveals clear sharing patterns. Segments a, c, d, e, f, and g all activate for digit 0, suggesting common logic. Segment e (active only for 0, 2, 6, 8) is simplest with just **2 product terms**: `B'D' + CD'`. Segment c (nearly always active) simplifies to `B + C' + D`. The segments share subexpressions like `B'D'` (used in a, d, e), `CD'` (used in d, e, g), and `BC'` (used in f, g). A solver that identifies and exploits these shared terms will dramatically outperform single-output optimization.

## Algorithm selection: SAT-based exact synthesis wins for this problem size

Three algorithmic approaches are viable for multi-output logic synthesis, each with distinct tradeoffs. For the BCD to 7-segment decoder specifically, **SAT-based exact synthesis** is the recommended approach because the problem size (4 inputs, 7 outputs) falls within the tractable range for exact methods.

**Classical two-level minimization** using Espresso-MV or BOOM runs in polynomial time and handles multi-output functions by encoding outputs as an additional multiple-valued variable. Product terms shared across outputs appear naturally when the MVL encoding's output sets intersect during cube expansion. Espresso's MAKE_SPARSE pass then removes unnecessary output connections. While fast, these methods optimize literal count rather than gate input count directly, and produce two-level (SOP) circuits rather than optimal multi-level implementations.

**SAT-based exact synthesis** encodes the question "does an r-gate circuit exist implementing these functions?" as a satisfiability problem. For circuits with ≤8 inputs, this approach finds provably optimal solutions. The Kojevnikov-Kulikov-Yaroslavtsev encoding (SAT 2009) and the Haaswijk-Soeken-Mishchenko formulation (TCAD 2020) both enable multi-output optimization with shared gates. Performance data shows 4-input functions average **225ms** for exact synthesis—well within practical limits.

**Heuristic multi-level synthesis** via ABC's DAG-aware rewriting scales to large designs but provides no optimality guarantees. The `resyn2` script typically achieves 10-15% area reduction through iterative rewriting, refactoring, and resubstitution. For small functions like BCD decoders, exact methods outperform these heuristics.

## SAT encoding for multi-output gate input minimization

The core encoding creates Boolean variables representing circuit structure, then adds constraints ensuring functional correctness. For a circuit with n primary inputs and r gates computing m outputs:

**Variable types define the search space:**
- `x_{i,t}`: Simulation variable—gate i's output on truth table row t
- `s_{i,j,k}`: Selection variable—gate i takes inputs from nodes j and k  
- `f_{i,p,q}`: Function variable—gate i's output when inputs are (p,q)
- `g_{h,i}`: Output assignment—output h is computed by gate i

**Functional correctness constraints** ensure each gate computes consistent values across all input combinations. For each gate i, input pair (j,k), truth table row t, and input/output pattern (a,b,c):

```
(¬s_{i,j,k} ∨ (x_{i,t} ⊕ a) ∨ (x_{j,t} ⊕ b) ∨ (x_{k,t} ⊕ c) ∨ (f_{i,b,c} ⊕ ā))
```

This clause fires when selection s_{i,j,k} is true and the simulation values match pattern (a,b,c), forcing the function variable to be consistent.

**Output constraints** connect internal gates to external outputs. For each output h and gate i, if the specification requires output h to be 1 on input row t:
```
(¬g_{h,i} ∨ x_{i,t})
```

**Multi-output sharing** emerges naturally: multiple g_{h,i} variables can point to the same gate i, and that gate is counted only once in the cost function. This is the mechanism that enables beating single-output optimization.

**Optimization via iterative SAT or MaxSAT:**
The simplest approach iterates r from 1 upward, asking "is there an r-gate solution?" until finding the minimum. For gate input minimization specifically, **Weighted MaxSAT** is more direct: hard clauses encode correctness, soft clauses penalize each selection variable s_{i,j,k} by its input cost (typically 2 for 2-input gates). The RC2 MaxSAT solver in PySAT won MaxSAT Evaluations 2018-2019 and handles this formulation efficiently.

## Shared subcircuit extraction algorithms

Before or alongside SAT search, identifying candidate shared terms accelerates optimization. Three techniques are most effective:

**Kernel extraction** finds common algebraic divisors. A kernel is a cube-free quotient when dividing a function by a cube (the co-kernel). The fundamental theorem states: if functions F and G share a multi-cube common divisor, their kernels must intersect in more than one cube. The algorithm recursively divides expressions by literals, collecting all kernels and co-kernels, then searches for rectangles in the co-kernel/cube matrix where all entries are non-empty.

**Structural hashing** in AIG-based tools like ABC provides automatic CSE. When constructing an And-Inverter Graph, each new AND node is hash-table checked against existing nodes with identical fanins. This guarantees no structural duplicates within one logic level, though functionally equivalent but structurally different circuits can still exist.

**FRAIG construction** extends structural hashing with functional equivalence checking. During circuit construction, random simulation identifies candidate equivalent node pairs, then SAT queries verify true equivalence. Merging functionally equivalent nodes reduces circuit size beyond what structural hashing achieves.

For the BCD decoder, pre-computing all prime implicants across the 7 outputs, then identifying which implicants cover minterms in multiple outputs, creates a covering problem where selecting shared implicants has lower cost-per-coverage than output-specific terms.

## Implementation architecture: PySAT with PyEDA preprocessing

For a custom solver targeting the 23-input baseline, the recommended stack is **PySAT** for SAT/MaxSAT solving combined with **PyEDA** for Boolean function manipulation and Espresso-based preprocessing. Both libraries are pip-installable and provide production-quality implementations.

**Phase 1: Generate prime implicants and baseline**
```python
from pyeda.inter import *
from pyeda.boolalg.minimization import espresso_tts

# Define all 7 segments with don't cares (positions 10-15)
X = exprvars('x', 4)
segments = {
    'a': truthtable(X, "1011011111------"),
    'b': truthtable(X, "1111100111------"),
    'c': truthtable(X, "1110111111------"),
    'd': truthtable(X, "1011011011------"),
    'e': truthtable(X, "1010001010------"),
    'f': truthtable(X, "1000111111------"),
    'g': truthtable(X, "0011111011------"),
}

# Joint minimization finds shared terms
minimized = espresso_tts(*segments.values())
baseline_cost = sum(count_literals(expr) for expr in minimized)
```

**Phase 2: MaxSAT formulation for gate input minimization**
```python
from pysat.formula import WCNF
from pysat.examples.rc2 import RC2

def minimize_gate_inputs(prime_implicants, minterms_per_output):
    wcnf = WCNF()
    var_counter = 1
    p_var = {}  # p_var[i] = "implicant i is selected"
    
    # Create variables for each prime implicant
    for i, impl in enumerate(prime_implicants):
        p_var[i] = var_counter
        var_counter += 1
    
    # Hard constraints: every minterm of every output must be covered
    for output_idx, minterms in enumerate(minterms_per_output):
        for m in minterms:
            covering = [p_var[i] for i, impl in enumerate(prime_implicants) 
                       if impl.covers(m, output_idx)]
            if covering:
                wcnf.append(covering)  # At least one must be selected
    
    # Soft constraints: minimize total literals (gate inputs)
    for i, impl in enumerate(prime_implicants):
        literal_count = impl.num_literals()
        # Penalize selecting this implicant by its literal cost
        wcnf.append([-p_var[i]], weight=literal_count)
    
    with RC2(wcnf) as solver:
        model = solver.compute()
        return solver.cost, extract_solution(model, prime_implicants, p_var)
```

**Phase 3: SAT-based exact synthesis for sub-problems**
For individual segments or small groups, exact synthesis can find provably optimal implementations:

```python
def exact_synthesis_segment(truth_table, max_gates=10):
    """Find minimum-gate circuit for single output."""
    for r in range(1, max_gates + 1):
        cnf = encode_circuit(truth_table, num_gates=r)
        with Solver(bootstrap_with=cnf) as s:
            if s.solve():
                return decode_circuit(s.get_model(), r)
    return None
```

## Cardinality constraints for bounding gate inputs

When encoding "total gate inputs ≤ k" as CNF, **Sinz's sequential counter** is optimal in practice. For at-most-k constraints over n variables:

```
Auxiliary variables: s_{i,j} for i=1..n, j=1..k
Meaning: s_{i,j} = "sum of x_1..x_i >= j"

Clauses:
  ¬x_1 ∨ s_{1,1}                    (initialize counter)
  ¬s_{i-1,j} ∨ s_{i,j}              (monotonicity)  
  ¬x_i ∨ ¬s_{i-1,j-1} ∨ s_{i,j}     (increment counter)
  ¬x_i ∨ ¬s_{i-1,k}                 (overflow = UNSAT)
```

This encoding uses O(n·k) clauses and auxiliary variables, enabling efficient propagation. PySAT's `pysat.card` module provides built-in implementations.

## Concrete pseudocode for the complete solver

```python
class BCDTo7SegmentSolver:
    def __init__(self):
        self.implicants = []
        self.outputs = ['a', 'b', 'c', 'd', 'e', 'f', 'g']
        
    def solve(self, target_cost=22):
        # Step 1: Generate all prime implicants with output tags
        self.generate_multi_output_primes()
        
        # Step 2: Compute shared coverage matrix
        coverage = self.build_coverage_matrix()
        
        # Step 3: MaxSAT optimization for minimum cost cover
        solution, cost = self.maxsat_cover(coverage, target_cost)
        
        # Step 4: If still above target, try multi-level factoring
        if cost > target_cost:
            solution = self.factor_common_subexpressions(solution)
            cost = self.compute_cost(solution)
        
        return solution, cost
    
    def generate_multi_output_primes(self):
        """Generate prime implicants tagged with output membership."""
        # Use Quine-McCluskey with output tags
        # Each implicant carries 7-bit tag indicating which outputs it covers
        for minterm_idx in range(10):  # BCD 0-9
            for output_idx, segment in enumerate(self.outputs):
                if self.segment_active(segment, minterm_idx):
                    # Add to on-set for this output
                    pass
        # Merge compatible minterms, tracking output tags
        # Stop when no more merging possible (prime implicants)
    
    def maxsat_cover(self, coverage, target):
        """Weighted MaxSAT: minimize sum of selected implicant costs."""
        wcnf = WCNF()
        
        # Hard: each (output, minterm) pair must be covered
        for out_idx in range(7):
            for minterm in self.on_set[out_idx]:
                clause = [self.impl_var(i) for i in coverage[out_idx][minterm]]
                wcnf.append(clause)
        
        # Soft: penalty for each implicant = its literal count
        for i, impl in enumerate(self.implicants):
            wcnf.append([-self.impl_var(i)], weight=impl.cost)
        
        with RC2(wcnf) as solver:
            model = solver.compute()
            return self.decode(model), solver.cost
```

## Known bounds and what to expect

Standard two-level implementations achieve **27-35 gate inputs** without sharing. Espresso joint minimization typically reaches **22-25 inputs**. SAT-based exact synthesis with full multi-output sharing has achieved **18-21 inputs** for this problem in synthesis competitions. The theoretical lower bound based on information content and required discriminations is approximately **15-17 inputs**, though achieving this may require exotic gate types (XOR, majority gates) not available in standard AND/OR/NOT libraries.

For a solver using AND, OR, NOT gates with full sharing optimization, expect to achieve **19-21 gate inputs**—comfortably beating the 23-input baseline by 10-15%. Adding XOR gates to the library can potentially save 2-3 additional inputs due to the checkerboard patterns in some segment truth tables.

## Recommended development sequence

Start with PyEDA's Espresso wrapper to establish a working baseline in under 50 lines of Python. This validates the truth table encoding and provides a cost reference. Next, implement the MaxSAT covering formulation using PySAT's WCNF and RC2—this typically achieves 2-4 input reduction over Espresso alone. Finally, for provable optimality, implement the full SAT encoding with selection variables for gate topology. The 4-input, 7-output size makes exhaustive search tractable in seconds to minutes.

The combination of algebraic preprocessing (kernel extraction for identifying shared terms), MaxSAT optimization (selecting minimum-cost covers), and optional SAT-based exact synthesis (for critical sub-circuits) provides a robust architecture that consistently beats heuristic-only approaches on small multi-output functions like the BCD to 7-segment decoder.