NAE-SAT (Not-All-Equal Satisfiability)

The Not-All-Equal Satisfiability (NAE-SAT) problem is a variant of the Boolean satisfiability problem (SAT). Given a set of Boolean variables $x_0, x_1, \ldots, x_{n-1}$ and a collection of clauses, each clause is satisfied if and only if at least one variable in the clause is True and at least one is False. In other words, a clause is violated when all its variables have the same value (all True or all False).

For example, for Boolean variables $x_0, x_1, x_2, x_3$, consider the following clauses:

\[\begin{aligned} C_0 &= \lbrace x_0,x_1,x_2 \rbrace,\\ C_1 &= \lbrace x_1,x_2,x_3 \rbrace,\\ C_2 &= \lbrace x_1,x_3 \rbrace \end{aligned}\]

The assignment $(x_0, x_1, x_2, x_3) = (\text{True}, \text{True}, \text{False}, \text{False})$ is a solution: each clause contains at least one True and at least one False variable.

NAE-SAT is NP-complete and arises in applications such as hypergraph coloring and constraint satisfaction.

HUBO formulation

For $n$ binary variables $x_0, x_1, \ldots, x_{n-1}$ and $m$ clauses $C_0, C_1, \ldots, C_{m-1}$, the NAE-SAT constraint can be formulated as a HUBO (Higher-order Unconstrained Binary Optimization) expression.

NAE constraint

For each clause $C_k = \lbrace x_{i_1}, x_{i_2}, \ldots, x_{i_s} \rbrace$, we define:

• All-True penalty: the product \(x_{i_1} \cdot x_{i_2} \cdots x_{i_s}\) equals 1 only when all variables in the clause are True.
• All-False penalty: the product \(\overline{x}_{i_1} \cdot \overline{x}_{i_2} \cdots \overline{x}_{i_s}\) equals 1 only when all variables are False, where \(\overline{x}_i\) denotes the negated literal (\(\overline{x}_i = 1 - x_i\)).

The constraint for the entire instance is:

\[\text{constraint} = \sum_{k=0}^{m-1} \Bigl( \prod_{j \in C_k} x_j + \prod_{j \in C_k} \overline{x}_j \Bigr)\]

This expression equals 0 if and only if every clause is NAE-satisfied.

Objective (optional)

As a secondary objective, we can balance the number of True and False variables:

\[\text{objective} = \Bigl(2\sum_{i=0}^{n-1} x_i - n\Bigr)^2\]

This is minimized (reaching 0 when $n$ is even, or 1 when $n$ is odd) when the True/False count is as balanced as possible.

HUBO expression

The final HUBO expression combines the constraint and objective with a penalty weight $P$:

\[f = \text{objective} + P \times \text{constraint}\]

where $P$ must be large enough (e.g., $P = n^2 + 1$) to ensure that constraint satisfaction is prioritized over objective minimization.

PyQBPP formulation

PyQBPP handles negated literals \(\overline{x}_i\) (written as ~x[i]) natively, which makes the NAE-SAT formulation natural and efficient. The following program defines a simple NAE-SAT instance with 5 variables and 4 clauses of size 3, solves it using EasySolver, and verifies the result.

import pyqbpp as qbpp

n = 5

# Clauses: each clause is a set of variable indices
clauses = [
    [0, 1, 2],
    [1, 2, 3],
    [2, 3, 4],
    [0, 3, 4],
]

# Create binary variables
x = qbpp.var("x", n)

# NAE constraint: penalty if all-true or all-false
constraint = 0
for clause in clauses:
    all_true = 1
    all_false = 1
    for idx in clause:
        all_true *= x[idx]
        all_false *= ~x[idx]
    constraint += all_true + all_false

# Objective: balance True/False count
s = qbpp.sum(x)
objective = (2 * s - n) * (2 * s - n)

# HUBO expression with penalty weight
penalty_weight = n * n + 1
f = (objective + penalty_weight * constraint).simplify_as_binary()

# Solve
solver = qbpp.EasySolver(f)
sol = solver.search({"target_energy": 1})  # n=5 is odd, so best balance gives (2*s-n)^2 = 1

# Print results
print(f"Energy = {sol.energy}")
print("Assignment:", " ".join(f"x[{i}]={sol(x[i])}" for i in range(n)))

print(f"constraint = {sol(constraint)}")
print(f"objective  = {sol(objective)}")

# Verify: check each clause
all_satisfied = True
for k, clause in enumerate(clauses):
    sum_val = 0
    for idx in clause:
        sum_val += sol(x[idx])
    satisfied = 0 < sum_val < len(clause)
    print(f"Clause {k}: {'satisfied' if satisfied else 'VIOLATED'}")
    if not satisfied:
        all_satisfied = False
print(f"All clauses NAE-satisfied: {'Yes' if all_satisfied else 'No'}")

Example output

Energy = 1
Assignment: x[0]=1 x[1]=0 x[2]=1 x[3]=0 x[4]=1
constraint = 0
objective  = 1
Clause 0: satisfied
Clause 1: satisfied
Clause 2: satisfied
Clause 3: satisfied
All clauses NAE-satisfied: Yes

The solver finds an assignment where constraint = 0, meaning all four clauses are NAE-satisfied. The objective value is 1 because $n = 5$ is odd, so a perfect True/False balance (e.g., 3 True and 2 False) gives $(2 \times 3 - 5)^2 = 1$.

Key points

• Negated literals: ~x[i] is used directly in PyQBPP to express \(\overline{x}_i\) without expanding to \(1 - x_i\). This keeps the HUBO expression compact.
• Higher-order terms: Each clause of size $s$ produces degree-$s$ terms (e.g., $x_0 x_1 x_2$ for a 3-literal clause). PyQBPP handles HUBO expressions natively without requiring quadratization.
• Penalty weight: $P = n^2 + 1$ ensures that any constraint violation outweighs the maximum possible objective value.