1212# --------
1313# For each edge (i, j, w):
1414# Introduce a selector variable s_ij (var index n + edge_idx + 1).
15- # Hard clauses force s_ij = 1 iff x_i != x_j (edge is cut):
16- # [ x_i v x_j v ~s_ij ]
17- # [~x_i v ~x_j v ~s_ij ]
15+ # Hard clauses encode s_ij <=> (x_i XOR x_j):
16+ # [ x_i v x_j v ~s_ij ] xi=0,xj=0 -> s=0 (always added)
17+ # [~x_i v ~x_j v ~s_ij ] xi=1,xj=1 -> s=0 (always added)
18+ # [~x_i v x_j v s_ij ] xi=1,xj=0 -> s=1 (only when min_w < 0)
19+ # [ x_i v ~x_j v s_ij ] xi=0,xj=1 -> s=1 (only when min_w < 0)
20+ # When all weights are non-negative RC2 already wants s=1 to claim the
21+ # reward, so the ->s clauses are redundant and omitted to halve the
22+ # clause count. When negative edges are present the ->s clauses are
23+ # critical: without them s can stay 0 while the edge is cut, letting
24+ # RC2 fraudulently claim the [-s] soft reward.
1825#
1926# Positive weight w > 0: we *want* the edge cut.
2027# Soft clause [s_ij] with weight round(w * SCALE).
7077# Encoding helpers
7178# ---------------------------------------------------------------------------
7279
73- def _build_wcnf (edges , n ):
80+ def _build_wcnf (edges , n , has_negative ):
7481 """
7582 Build a WCNF formula for MAXCUT on n nodes with the given edge list.
7683
@@ -84,16 +91,23 @@ def _build_wcnf(edges, n):
8491 """
8592 wcnf = WCNF ()
8693 total_pos_scaled = 0
94+ neg_scaled_total = 0
8795 baseline_neg = 0.0
8896
8997 for idx , (i , j , w ) in enumerate (edges ):
9098 xi = i + 1 # 1-indexed SAT variable for node i
9199 xj = j + 1 # 1-indexed SAT variable for node j
92100 s = n + idx + 1 # selector variable for this edge
93101
94- # Hard clauses: s <=> (x_i XOR x_j)
95- wcnf .append ([ xi , xj , - s ]) # ~s -> x_i v x_j
96- wcnf .append ([- xi , - xj , - s ]) # ~s -> ~x_i v ~x_j
102+ # s=1 when edge not cut is always suboptimal for positive edges,
103+ # so the two ->s direction clauses are only needed when negative
104+ # edges are present (otherwise they would double the clause count
105+ # for no benefit).
106+ wcnf .append ([ xi , xj , - s ]) # xi=0,xj=0 -> s=0
107+ wcnf .append ([- xi , - xj , - s ]) # xi=1,xj=1 -> s=0
108+ if has_negative :
109+ wcnf .append ([- xi , xj , s ]) # xi=1,xj=0 -> s=1
110+ wcnf .append ([ xi , - xj , s ]) # xi=0,xj=1 -> s=1
97111
98112 if w >= 0.0 :
99113 iw = max (1 , int (round (w * _SCALE )))
@@ -102,9 +116,10 @@ def _build_wcnf(edges, n):
102116 else :
103117 iw = max (1 , int (round (- w * _SCALE )))
104118 baseline_neg += w # this is already negative
119+ neg_scaled_total += iw
105120 wcnf .append ([- s ], weight = iw ) # soft: want edge NOT cut
106121
107- return wcnf , total_pos_scaled , baseline_neg
122+ return wcnf , total_pos_scaled , neg_scaled_total , baseline_neg
108123
109124
110125def _model_to_bits (model , n ):
@@ -236,7 +251,8 @@ def solve_maxcut_exact(
236251 bitstring , l , r = get_cut (warm_theta , nodes , n_qubits )
237252 return bitstring , 0.0 , (l , r ), 0.0 , True
238253
239- wcnf , total_pos_scaled , baseline_neg = _build_wcnf (edges , n_qubits )
254+ has_negative = any (w < 0.0 for _ , _ , w in edges )
255+ wcnf , total_pos_scaled , neg_scaled_total , baseline_neg = _build_wcnf (edges , n_qubits , has_negative )
240256
241257 if verbose :
242258 print ("Starting RC2 MaxSAT solver..." )
@@ -252,9 +268,9 @@ def solve_maxcut_exact(
252268 # RC2 uses Glucose3 internally; we set variable polarities to match the
253269 # warm start so the first SAT call explores the warm-start region first.
254270 try :
255- for i , bit in enumerate ( warm_theta ):
256- # oracle.set_phases expects a list of signed literals
257- rc2 .oracle .set_phases ([ i + 1 if bit else - ( i + 1 )] )
271+ phases = [ i + 1 if warm_theta [ i ] else - ( i + 1 )
272+ for i in range ( len ( warm_theta ))]
273+ rc2 .oracle .set_phases (phases )
258274 except AttributeError :
259275 pass # solver doesn't support phase setting; continue without
260276
@@ -274,7 +290,7 @@ def solve_maxcut_exact(
274290 best_theta = _model_to_bits (model , n_qubits )
275291
276292 if verbose and model is not None :
277- cut_opt = (total_pos_scaled - cost_scaled ) / _SCALE + baseline_neg
293+ cut_opt = baseline_neg + (total_pos_scaled + neg_scaled_total - cost_scaled ) / _SCALE
278294 print (f"RC2 optimum: { cut_opt :.6f} ({ elapsed :.3f} s)" )
279295
280296 # --- final scoring (matches spin_glass_solver return convention) ---
0 commit comments