[Synth] Add SAT-based exact synthesis pass

[uenoku]

Add synth-exact-synthesis, which rewrites small single-bit comb.truth_table ops into area-optimal synth dialect operations with BooleanLogicOpInterface.

The pass searches increasing node counts and, for each size, builds a SAT problem where each ordered step selects one allowed primitive fed by constants, inputs, or earlier steps.

Exact synthesis is really expensive that cannot be used in online. Instead this pass will be used in offline in order to popuatle database for good cut structures (which will be used by CutRewriter pass).

Depth-optimal exact synthesis and better symmetric breaking would be future enhancement.

Tests are currently weak since it's challenging to verify the area optimality. Running exact synthesis for onehot/dot on 222 NPN took 3 minutes locally (32 threads). We could create a CI(or circt-tests like post-merge tests in another repo).

I checked a few operations dot/onehot and verified the number matches with TABLE IV in https://si2.epfl.ch/~demichel/publications/archive/2021/3Input.pdf.

count  npn4-dot.mlir
-----  -------------
    0              2
    1              3
    2             32
    3            158
    4             27
total            222

count  npn4-onehot.mlir
-----  ----------------
    0                 2
    1                 3
    2                18
    3               151
    4                48
total               222

Assisted-by: codex: gpt-5.5

[circt-bot]

Results of circt-tests run for cf9f53a compared to results for c970c42: no change to test results.