files / problems / unique-sum / compute / q5 / midpoint_cases.py
#!/usr/bin/env python3
"""Partition an AP-avoiding completion problem by a named midpoint witness.
Every selected center c needs distinct selected endpoints u,v with u+v=2c.
List ALL these pairs. Roots already containing a forbidden AP are impossible
in this conditional family. Affine-equivalent remaining roots share one run.
"""
import argparse
import hashlib
import json
from pathlib import Path
from audit_cover import has_ap, mask, root
from run_cover import run
def canonical(p, values):
return min(tuple(sorted((a*(x-b)) % p for x in values))
for a in range(1, p) for b in values)
def cases(p, initial_ap, forbid_ap, center):
selected = root(p, initial_ap)
assert selected >> center & 1, 'center must be selected in the root'
rows, classes = [], {}
for a in range(p):
b = (2*center-a) % p
if a >= b:
continue
combined = selected | (1 << a) | (1 << b)
values = {x for x in range(p) if combined >> x & 1}
row = dict(pair=[a, b], root=sorted(values), root_mask=hex(combined))
if has_ap(p, values, forbid_ap):
row['forbidden_progression'] = True
else:
key = canonical(p, values)
if key not in classes:
classes[key] = len(rows)
row['representative'] = classes[key]
rows.append(row)
assert len(rows) == (p-1)//2
return rows
def main():
ap = argparse.ArgumentParser(description=__doc__)
ap.add_argument('binary', type=Path)
ap.add_argument('p', type=int)
ap.add_argument('bound', type=int)
ap.add_argument('--initial-ap', type=int, default=3)
ap.add_argument('--forbid-ap', type=int, default=4)
ap.add_argument('--center', type=int, default=1)
ap.add_argument('--nodes', type=int, default=10000000)
ap.add_argument('--seconds-per-case', type=float, default=120)
ap.add_argument('--output', type=Path, required=True)
args = ap.parse_args()
if not 3 <= args.p < 64 or any(args.p % d == 0 for d in range(2, args.p)):
ap.error('odd prime below 64 required')
if not (2 <= args.bound <= args.p and 3 <= args.initial_ap <= args.p
and 3 <= args.forbid_ap <= args.p and 0 <= args.center < args.p
and args.nodes > 0 and args.seconds_per_case > 0):
ap.error('invalid bounds, progression, center or limits')
source = Path(__file__).with_name('cover_search.c')
payload = dict(p=args.p, bound=args.bound, initial_ap=args.initial_ap,
forbid_ap=args.forbid_ap, center=args.center,
source_sha256=hashlib.sha256(source.read_bytes()).hexdigest(),
binary_sha256=hashlib.sha256(args.binary.read_bytes()).hexdigest(),
partition_source_sha256=hashlib.sha256(Path(__file__).read_bytes()).hexdigest(),
status='UNKNOWN', conditional=True,
cases=cases(args.p, args.initial_ap, args.forbid_ap, args.center))
def save():
temporary = args.output.with_suffix('.tmp')
temporary.write_text(json.dumps(payload, indent=2)+'\n')
temporary.replace(args.output)
save()
order = [i for i, row in enumerate(payload['cases']) if row.get('representative') == i]
order.sort(key=lambda i: -len(payload['cases'][i]['root']))
for i in order:
row = payload['cases'][i]
row['result'] = run(args.binary, args.p, args.bound, args.nodes, args.initial_ap,
args.forbid_ap, int(row['root_mask'], 16), args.seconds_per_case)
save()
print(f"case={i} center={args.center} pair={row['pair']} "
f"root_size={len(row['root'])} status={row['result']['status']}", flush=True)
if row['result']['status'] == 'SAT':
break
results = [row.get('result', {}).get('status') for i, row in enumerate(payload['cases'])
if row.get('representative') == i]
payload['status'] = 'SAT' if 'SAT' in results else 'UNSAT' if all(s == 'UNSAT' for s in results) else 'UNKNOWN'
save()
print(f"conditional_status={payload['status']} representatives={len(results)}", flush=True)
return 3 if payload['status'] == 'UNKNOWN' else 0
if __name__ == '__main__':
raise SystemExit(main())