Emit minimal penalty gadgets for Boolean logic constraint patterns (NOT/AND/OR/XOR)

[bernalde]

Motivation

MQT QAO (arXiv:2406.12840) ships dedicated quadratic penalty gadgets for ~a=b, a&b=c, a|b=c, a^b=c (src/mqt/qao/constraints.py:187-671). Their version is limited to raw single binary variables and its AND/OR solution checkers contain operator-precedence bugs (bool(e1) and bool(e2) == bool(e3) at constraints.py:402,458,557,613), so this is not a battle-tested advantage — but the minimal-gadget forms do save ancillas and penalty magnitude versus a generic squared residual.

Current state

src/compiler/constraints.jl has constraint() dispatch only for SAF/SQF in EQ/LT/GT/Interval (:198-760), VectorOfVariables-in-SOS1 (:770), and Indicator (:914-978) — no logic-set or gadget-pattern handling. Every gate is expressible today: e.g. c == a*b compiles via the SQF-in-EQ path (:484-541, squared residual + Quadratize at :535), at the cost of ancilla overhead.

Proposed change

Add pattern recognition inside constraint(model, ci, f::SQF, s::EQ) (constraints.jl:494-541) for residuals of shape:

• c - a*b → textbook AND penalty,
• a + b - a*b - c → OR penalty,
• a + b - 2ab - c → XOR (cubic residual; reuses the existing Quadratize path),

emitting the penalty PBF directly and skipping the square. Alternatively (or additionally) document MOI.Indicator-based formulations, which are already supported. All variables involved must be verified binary before matching; fall back to the generic path otherwise.

Acceptance criteria

• AND/OR/XOR equality constraints over binary variables compile to the minimal textbook penalties (assert term counts/coefficients in tests).
• Non-matching SQF-EQ constraints still take the generic squared-residual path (regression tests pass unchanged).
• Ground states of each gadget penalty are exactly the gate's truth table (exhaustive check via ExactSampler).

Part of the MQT QAO parity epic: JuliaQUBO/QUBO.jl#69