⏺ Input Analysis: Circuit vs CNF Representation
This is critical for OB-SAT! Your tensor network framework needs structured constraints (circuits/CSP), not just flat CNF.
Problem Categories by Input Type
✅ Category A: Natural Circuits (OB-SAT applicable)
┌────────────────┬───────────────┬──────────────┬────────────────────────────┐
│ Problem │ Input Type │ Circuit │ Notes │
│ │ │ Structure │ │
├────────────────┼───────────────┼──────────────┼────────────────────────────┤
│ Factoring │ $(n, m, N)$ │ Multiplier │ ✓ Already doing this │
│ │ │ circuit │ │
├────────────────┼───────────────┼──────────────┼────────────────────────────┤
│ Multiplier │ Two circuits │ Arithmetic │ Input: .aig or .v │
│ Verification │ $C_1, C_2$ │ circuits │ (Verilog)Perfect fit! │
├────────────────┼───────────────┼──────────────┼────────────────────────────┤
│ │ Message/key │ Boolean │ Input: Can generate from │
│ SHA/MD5/AES │ bits │ circuit │ crypto libNatural gates: │
│ │ │ │ XOR, AND, NOT │
├────────────────┼───────────────┼──────────────┼────────────────────────────┤
│ Circuit-SAT │ Circuit $C$ │ Any boolean │ Input: .aig, .bench, │
│ │ │ circuit │ .blifAlready supported │
├────────────────┼───────────────┼──────────────┼────────────────────────────┤
│ Hardware │ RTL design │ Gate-level │ Input: .aig, .aiger (HWMCC │
│ Verification │ │ circuit │ format)Direct application │
├────────────────┼───────────────┼──────────────┼────────────────────────────┤
│ XOR-SAT │ Mixed │ XOR + AND │ Can represent as │
│ (hybrid) │ constraints │ gates │ circuitBut often given as │
│ │ │ │ CNF │
└────────────────┴───────────────┴──────────────┴────────────────────────────┘
Key insight: These problems have native circuit representation where tensor network makes sense.
---
⚠️ Category B: Constraint Networks (Need CSP encoding)
┌─────────────┬───────────┬──────────────┬───────────────────────────────────┐
│ Problem │ Input │ Structure │ OB-SAT Applicability │
│ │ Type │ │ │
├─────────────┼───────────┼──────────────┼───────────────────────────────────┤
│ │ │ │ Input: Grid positions + │
│ Latin │ Partial │ Constraint │ constraintsCan encode as CSP │
│ Square │ grid │ network │ (all-different │
│ │ │ │ constraints)Awkward as circuit │
├─────────────┼───────────┼──────────────┼───────────────────────────────────┤
│ Graph │ Graph │ Graph │ Input: Edge listCan encode as CSP │
│ Coloring │ $G(V,E)$ │ constraints │ (inequality constraints)Not │
│ │ │ │ natural circuit │
├─────────────┼───────────┼──────────────┼───────────────────────────────────┤
│ │ Partial │ Constraint │ Similar to Latin │
│ Sudoku │ grid │ network │ SquareAll-different constraints │
│ │ │ │ per row/col/box │
├─────────────┼───────────┼──────────────┼───────────────────────────────────┤
│ Job-Shop │ Jobs + │ Temporal │ Input: Task durations, │
│ Scheduling │ machines │ constraints │ precedenceCSP encoding │
│ │ │ │ possibleVery unnatural as circuit │
└─────────────┴───────────┴──────────────┴───────────────────────────────────┘
Key insight: These need constraint network representation, not circuits. OB-SAT's tensor framework could handle CSP, but:
- Current implementation uses circuits
- Would need generalization to arbitrary constraints
---
❌ Category C: Pure CNF (OB-SAT at disadvantage)
┌──────────────┬─────────────┬───────────────┬───────────────────────────────┐
│ Problem │ Input Type │ Structure │ Problem for OB-SAT │
├──────────────┼─────────────┼───────────────┼───────────────────────────────┤
│ Pigeonhole │ $(n, m)$ │ │ Input: Usually direct CNFNo │
│ Principle │ parameters │ Generated CNF │ circuit availableCan encode │
│ │ │ │ as circuit but loses meaning │
├──────────────┼─────────────┼───────────────┼───────────────────────────────┤
│ Planning │ │ State │ Input: PDDL → SAT encodingCNF │
│ (PDDL) │ PDDL file │ transition │ is the outputOriginal │
│ │ │ CNF │ structure (STRIPS) lost │
├──────────────┼─────────────┼───────────────┼───────────────────────────────┤
│ Random 3-SAT │ Generator │ Unstructured │ Input: Pure CNF clausesNo │
│ │ seed │ CNF │ structure to exploit! │
├──────────────┼─────────────┼───────────────┼───────────────────────────────┤
│ Crafted │ Generator │ Hand-crafted │ Input: CNF clausesStructure │
│ (Urquhart, │ params │ CNF │ designed to fool solvers │
│ etc) │ │ │ │
├──────────────┼─────────────┼───────────────┼───────────────────────────────┤
│ 2+p SAT │ Random │ Nearly 2-SAT │ Input: CNFNo circuit │
│ │ generator │ CNF │ structure │
└──────────────┴─────────────┴───────────────┴───────────────────────────────┘
Key insight: Only CNF available → OB-SAT loses its advantage (no tensor structure to exploit).
---
Detailed Analysis by Problem
🟢 Multiplier Verification (BEST FIT)
Input Format:
# Option 1: AIGER format (.aig)
aag M I L O A
i1
i2
...
o1
...
a1 lhs rhs
Circuit Structure:
Inputs: x[0..n-1], y[0..n-1]
Gates: Half-adders, full-adders arranged in array
Output: z[0..2n-1]
Why perfect for OB-SAT:
- ✓ Natural gate-level structure (AND, XOR)
- ✓ Hierarchical (carry chains)
- ✓ Tensor network can exploit regularity
- ✓ Available in .aig format → can use your existing circuit parser
Example: https://github.com/meelgroup/AIG-benchmarks/blob/master/multiplier/mult_8.aig
---
🟢 SHA-256 / AES (GOOD FIT)
Input Format:
# Typically generated programmatically
def sha256_circuit(message_bits):
# Message schedule
w[0..63] = expand(message_bits)
# Compression rounds
for i in range(64):
t1 = Σ1(e) ⊕ Ch(e,f,g) ⊕ h ⊕ K[i] ⊕ w[i]
...
return circuit
Circuit Structure:
- XOR, AND, NOT gates
- Modular addition (ripple-carry adders)
- Bit rotations (just rewiring)
Why good for OB-SAT:
- ✓ Natural boolean circuit
- ✓ Can generate from specification
- ⚠️ Very large (SHA-256 ≈ 100K gates for one round)
- ⚠️ XOR-heavy → might need special handling
Resources:
- SAT encoding: https://github.com/vegard/sha1-sat
- Circuit generator: https://github.com/cjliu20152/CNFgen
---
🟡 Latin Square / Sudoku (POSSIBLE BUT AWKWARD)
Input Format:
# Given: partial grid
3 0 0 0 5 0 0 0 8
0 0 0 2 0 0 1 0 0
...
# Or as constraints:
cell(0,0) = 3
cell(0,4) = 5
...
Not naturally a circuit! But can encode:
Option 1: One-hot encoding
For each cell (i,j), variables: x[i][j][1..n]
Constraint: exactly one of x[i][j][*] is true
All-different per row: atmost-one circuit
Option 2: Direct encoding
Variables: cell[i][j] ∈ {1..n}
Constraint network (not circuit!)
Why awkward:
- ✗ All-different constraint not natural as boolean circuit
- ✗ One-hot encoding blows up size
- ✗ Loses elegant structure of the problem
Verdict: Can do it, but not OB-SAT's strength. Better suited for CSP solvers.
---
🟡 Graph Coloring (SIMILAR ISSUE)
Input Format:
# DIMACS graph format
p edge 125 736
e 1 2
e 1 3
...
Encoding to circuit:
Variables: color[v] for each vertex v
For each edge (u,v): color[u] ≠ color[v]
One-hot encoding:
For vertex v: c[v][1..k] (k colors)
Constraint: exactly-one(c[v][1..k])
For edge (u,v): AND_i NOT(c[u][i] AND c[v][i])
Why awkward:
- ✗ One-hot encoding artificial
- ✗ Constraint is "not-equal", not naturally boolean operations
- ✗ Tensor network doesn't exploit graph structure
Verdict: Can encode, but loses structure. Graph-based SAT encodings are better.
---
🟢 Hardware Verification (HWMCC) (EXCELLENT FIT)
Input Format:
# AIGER format (.aig)
aag 7 2 1 2 4
2 # input
4 # input
6 13 # latch (next state = 13)
6 # output (current state)
8 # output (safety property)
10 3 2 # AND gate
12 6 10
14 2 13
Circuit Structure:
- Sequential circuit: latches + combinational logic
- Bounded model checking: unroll circuit
- Safety property: assert output
Why excellent:
- ✓ Already in .aig format
- ✓ Your circuit parser works directly
- ✓ Standard benchmark format
- ✓ Industry-relevant
Resource: http://fmv.jku.at/hwmcc20/
---
❌ Planning (PDDL → SAT) (POOR FIT)
Input Format:
; PDDL domain
(define (domain blocksworld)
(:action pickup
:parameters (?x)
:precondition (and (clear ?x) (on-table ?x) (empty-hand))
:effect (and (holding ?x) (not (on-table ?x)) (not (empty-hand)))))
SAT Encoding Process:
PDDL → Ground actions → State variables per timestep → CNF
Why poor fit:
- ✗ Original structure (state transitions) lost in CNF
- ✗ SAT encoding is the output, not input
- ✗ No natural circuit representation
- ✗ Temporal structure flattened
Verdict: Not suitable for OB-SAT. The structure you'd want to exploit is gone.
---
❌ Random 3-SAT (WORST FIT)
Input Format:
p cnf 100 430
1 -2 3 0
-1 4 -5 0
...
No circuit at all! Just random clauses.
Why worst fit:
- ✗ No structure to exploit
- ✗ Converting to circuit is pointless (artificial)
- ✗ This is march/CDCL territory
Verdict: Skip this entirely. Designed to test unstructured SAT solving.
---
Summary Table: OB-SAT Suitability
┌─────────────────────┬────────────────┬────────────┬─────────────┬──────────┐
│ Problem │ Input │ Circuit? │ OB-SAT Fit │ Priority │
│ │ Available │ │ │ │
├─────────────────────┼────────────────┼────────────┼─────────────┼──────────┤
│ Multiplier │ .aig │ ✓✓✓ │ 🟢 │ P0 │
│ Verification │ │ Natural │ Excellent │ │
├─────────────────────┼────────────────┼────────────┼─────────────┼──────────┤
│ SHA/AES │ Generated │ ✓✓ Natural │ 🟢 Good │ P0 │
│ │ circuit │ │ │ │
├─────────────────────┼────────────────┼────────────┼─────────────┼──────────┤
│ Hardware │ .aig │ ✓✓✓ Native │ 🟢 │ P0 │
│ Verification │ │ │ Excellent │ │
├─────────────────────┼────────────────┼────────────┼─────────────┼──────────┤
│ Circuit-SAT │ .aig, .bench │ ✓✓✓ Native │ 🟢 │ Current │
│ │ │ │ Excellent │ │
├─────────────────────┼────────────────┼────────────┼─────────────┼──────────┤
│ Factoring │ Generated │ ✓✓✓ │ 🟢 Good │ Current │
│ │ │ Natural │ │ │
├─────────────────────┼────────────────┼────────────┼─────────────┼──────────┤
│ XOR-SAT Hybrid │ Mixed │ ✓ Can │ 🟡 Possible │ P1 │
│ │ │ encode │ │ │
├─────────────────────┼────────────────┼────────────┼─────────────┼──────────┤
│ Latin Square │ Grid + rules │ ⚠️ Awkward │ 🟡 Awkward │ P2 │
├─────────────────────┼────────────────┼────────────┼─────────────┼──────────┤
│ Graph Coloring │ Graph │ ⚠️ Awkward │ 🟡 Awkward │ P2 │
├─────────────────────┼────────────────┼────────────┼─────────────┼──────────┤
│ Pigeonhole │ CNF │ ✗ No │ 🔴 Poor │ P3 │
├─────────────────────┼────────────────┼────────────┼─────────────┼──────────┤
│ Planning │ PDDL │ ✗ No │ 🔴 Poor │ Skip │
├─────────────────────┼────────────────┼────────────┼─────────────┼──────────┤
│ Random SAT │ CNF │ ✗ No │ 🔴 Terrible │ Skip │
└─────────────────────┴────────────────┴────────────┴─────────────┴──────────┘
---
Recommendation: Focus on "Natural Circuit" Problems
Ideal benchmarks for OB-SAT:
1. Multiplier verification (.aig available, arithmetic structure)
2. Crypto primitives (SHA, AES - can generate circuits)
3. Hardware verification (HWMCC .aig files)
Why these are perfect:
- Input is naturally a circuit
- Structure is meaningful (not artificially imposed)
- Tensor network should exploit structure better than flat CNF solvers
- Available in formats you can already parse
Avoid:
- Pure CNF problems (Random SAT, PHP, Planning)
- Problems where circuit encoding is artificial (Latin Square, Coloring)
Add more problems
Avalable solvers need to benchmark