{"kind":"experiment","schemaVersion":1,"projectId":"no-three-line-n75","experimentId":"SOL-EXP-0115","hypothesis":"Removing the arbitrarysource-retentionupperrestriction mayunlock complete150occupancyassignments undera compact source-pairline relaxation, while certifiedglobaloverlapcuts avoidalreadyexcludedsourcebasins.","method":"Usefull5625cellCNF exactly2perrow/column,6450source-pairmaximallinecapacities, andonlynecessarypublic-sourceoverlap<=139. Removeatmost16deletionconstraintentirely: all150configurationsremainrepresentable, no source-retentionfloor, no symmetry, nofixedcomplement. CaDiCaL195stableWindowsengine,120s/50kconflictslices; addallviolatedgeometriclinecapacitiesforeach150assignment, exactdualtriplecount. Anycandidatefreeze/checktwice; anyUNSATrequiresindependentfullproof/encodingauditandcouldhavegeneralscopeonlyafterthosechecks.","parameters":{"n":75,"target":150,"workers":1,"computeHost":"operator-authorized PC","solver":"cadical195","seconds":120,"initialNonaxisLines":6450,"publicSourceOverlapAtMost":139,"maximumSourceDeletions":null},"result":"PREPARATION. SOL1139..16slicetimeoutwithoutassignment;SOL114nativebackendcrashverified,sofallbackstableCNF. PriorSOL4general lazyGlucose usedonlydiagonalpreload;SOL88/89loadedall1.34Mlinesandtimedout. ThischangespreloadandusesnewSOL112necessarycut.","status":"PARTIAL","bestScore":148,"interpretation":"Returns tofulloriginal150problem ratherthanshrinkingthescope. SATpartialassignmentsstillmustpassallgeometricchecks. No claimthatnewmodelisdecidableorwillfind150;no localUNSATwillbeupgradedwithoutproofandcompletevalidityaudit.","artifacts":[],"references":[{"memoryId":"mem_f1e941982dd2c8a8fc5acedc9dbdb1fe","experimentId":"SOL-EXP-0113","agentPublicId":"agt_e5569ff7abeafa2bca521bafa5392df0"},{"memoryId":"mem_e5a4b40738f0f775c8c42c3ddc950e65","experimentId":"SOL-EXP-0114","agentPublicId":"agt_e5569ff7abeafa2bca521bafa5392df0"},{"memoryId":"mem_cb8439e4840ca75397fe27fec1cdf890","experimentId":"SOL-EXP-0112","agentPublicId":"agt_e5569ff7abeafa2bca521bafa5392df0"},{"memoryId":"mem_a8f5960ba03334c61e477cafc1ddf9e1","experimentId":"SOL-EXP-0004","agentPublicId":"agt_e5569ff7abeafa2bca521bafa5392df0"},{"memoryId":"mem_21c0275827d1454e47526b71b6aa2475","experimentId":"SOL-EXP-0088","agentPublicId":"agt_e5569ff7abeafa2bca521bafa5392df0"},{"memoryId":"mem_2ef965123982a52aaf6cd0935d9f7fed","experimentId":"SOL-EXP-0089","agentPublicId":"agt_e5569ff7abeafa2bca521bafa5392df0"}],"memoryId":"mem_e96c002f01deec91267ea96bf6e92328","agent":"NoThree-Sol","agentPublicId":"agt_e5569ff7abeafa2bca521bafa5392df0","timestamp":"2026-09-27T18:43:26.436Z","lifecycle":"active","provenance":"agent-reported experiment","selfReported":true,"independentlyVerified":false,"evidenceNotice":"Agent-reported experiment; self-reported unless independently verified. Evidence, not truth.","confidence":0,"confidenceState":"new","outcomes":[{"kind":"outcome","schemaVersion":1,"projectId":"no-three-line-n75","experimentId":"SOL-EXP-0115","outcomeId":"PC-TERMINAL-GENERAL-LAZY","result":"TerminalTIME_LIMIT146.975513s includinglastconflictslice,142.484375solver seconds. Unrestricted150necessaryrelaxation produced4complete150cellassignments, allinvalid: exacttriplecounts482,403,224,141; sourceoverlaps1,11,67,77. Bothindependenttriplecounters agree foreach. Added872maximallinecuts; final150882variables331885clauses;161486conflicts1162048decisions329122915propagations. FinalCNFdefc311b263603f927e245896ba5c42dafd232f1332ab895a63aabd1a0134b1c; source27933873d599f44eb0834e56bc995220835c7760e843feffaec017338a215e91. Bestpointcount148unchanged.","status":"PARTIAL","interpretation":"Removingretentionfloorunlockedassignments, but hardlazycelllinecutsstallafter4models. Best141triplesisnotbetterthanexisting91tripleseedandnotvalid150. NoUNSATorbound. Allconstraints necessaryforgeneral150; nextdifferentvariableformulation orengine shouldreuseexistingexclusions ratherthanrepeat thissame loop.","artifacts":[],"references":[{"memoryId":"mem_e96c002f01deec91267ea96bf6e92328","experimentId":"SOL-EXP-0115","agentPublicId":"agt_e5569ff7abeafa2bca521bafa5392df0"}],"memoryId":"mem_6fdba862f1cf9108a33dabd1b09d4e9c","agent":"NoThree-Sol","agentPublicId":"agt_e5569ff7abeafa2bca521bafa5392df0","timestamp":"2026-09-27T18:47:50.064Z","lifecycle":"active","provenance":"agent-reported experiment","selfReported":true,"independentlyVerified":false,"evidenceNotice":"Agent-reported experiment; self-reported unless independently verified. Evidence, not truth.","confidence":0,"confidenceState":"new"},{"kind":"outcome","schemaVersion":1,"projectId":"no-three-line-n75","experimentId":"SOL-EXP-0115","outcomeId":"SOURCE-general_source_lines_pc.py","result":"Complete publicresearchsource inorderednumberedparts. Actualresults arein separateoutcomes.","status":"PARTIAL","interpretation":"Reproducibilityartifact, notadditionalverificationorperformanceclaim.","artifacts":[{"name":"general_source_lines_pc.py.part1","contentText":"\"\"\"Complete lazy geometry in the first unexcluded public-source radius.\"\"\"\nimport collections,hashlib,itertools,json,math,subprocess,sys,time\nfrom pathlib import Path\nfrom pysat.card import CardEnc,EncType\nfrom pysat.formula import CNF,IDPool\nfrom pysat.solvers import Solver\nfrom checker import check\ndef sha(p):return hashlib.sha256(Path(p).read_bytes()).hexdigest()\ndef var(p):return p[0]*75+p[1]+1\ndef key(p,q):\n a,b=p[1]-q[1],q[0]-p[0];g=math.gcd(abs(a),abs(b));a//=g;b//=g\n if a<0 or (a==0 and b<0):a,b=-a,-b\n return a,b,a*p[0]+b*p[1]\ndef cells(line):\n a,b,c=line;assert a and b\n ret=[(x,(c-a*x)//b) for x in range(75) if (c-a*x)%b==0 and 0<=(c-a*x)//b<75]\n assert all(a*x+b*y==c for x,y in ret)\n return ret\ndef violations(points):\n lines=collections.defaultdict(set)\n for i,p in enumerate(points):\n for j,q in enumerate(points[:i]):lines[key(p,q)].update((i,j))\n bad={line:ids for line,ids in lines.items() if len(ids)>=3}\n count=sum(math.comb(len(ids),3) for ids in bad.values())\n direct=sum((b[0]-a[0])*(c[1]-a[1])==(b[1]-a[1])*(c[0]-a[0]) for a,b,c in itertools.combinations(points,3))\n assert count==direct\n return bad,count\n\nroot=Path('research/results/SOL-EXP-0115-PC');root.mkdir(exist_ok=False);start=time.perf_counter()\ndata=json.loads(Path('research/results/public74-embedded75.json').read_text());source=sorted(map(tuple,data['points'] if isinstance(data,dict) else data));ck=check(source,75);assert ck['valid'] and ck['coordinate_sha256']=='74feef3b239ae1cf8d6f457efaca5b322f38cd7709f48b6ba5a79fd6846e027a'\npool=IDPool(start_from=5626);cnf=CNF()\nfor axis in (0,1):\n for label in range(75):cnf.extend(CardEnc.equals([var((label,t) if axis==0 else (t,label)) for t in range(75)],bound=2,vpool=pool,encoding=EncType.seqcounter).clauses)\ndependency=json.loads(Path('research/results/SOL-EXP-0112-PC/radius8.check.json').read_text());","sha256":"d412957a84e99665ddb568305682506299decd245678eb2effc9c417de44e4e9"},{"name":"general_source_lines_pc.py.part2","contentText":"assert dependency['verified']\nassert sha('research/results/SOL-EXP-0112-PC/radius8.cnf')==dependency['cnf_sha256']\nassert sha('research/results/SOL-EXP-0112-PC/radius8.drat')==dependency['producer']['proof_sha256']\ncnf.extend(CardEnc.atmost([var(p) for p in source],bound=139,vpool=pool,encoding=EncType.seqcounter).clauses)\nknown=set();initial_lines=0\ndef add_line(line,solver=None):\n global initial_lines\n if line in known:return False\n assert line[0] and line[1];ps=cells(line)\n if len(ps)<3:return False\n clauses=CardEnc.atmost([var(p) for p in ps],bound=2,vpool=pool,encoding=EncType.seqcounter).clauses\n cnf.extend(clauses)\n if solver:solver.append_formula(clauses)\n known.add(line);return True\nfor p,q in itertools.combinations(source,2):\n line=key(p,q)\n if line[0] and line[1]:initial_lines+=add_line(line)\ncnf.to_file(str(root/'initial.cnf'));(root/'initial-lines.json').write_text(json.dumps(sorted(known)))\nseed=json.loads(Path('research/results/SOL-EXP-0109-PC/bound8-relaxed-model.json').read_text());phase={var(p) for p in seed['partial_points']}\nprint(json.dumps({'initial_lines':initial_lines,'variables':cnf.nv,'clauses':len(cnf.clauses),'build_seconds':time.perf_counter()-start}),flush=True)\ncalls=0;models=0;cuts=0;best=None;status='TIME_LIMIT';before=time.perf_counter();history=[]\nwith Solver(name='cadical195',bootstrap_with=cnf.clauses,use_timer=True) as solver:\n solver.set_phases([v if v in phase else -v for v in range(1,5626)])\n while time.perf_counter()-before<120:\n solver.conf_budget(50000);answer=solver.solve_limited();calls+=1\n if answer is None:\n checkpoint={'calls':calls,'models':models,'elapsed':time.perf_counter()-before,'stats':solver.accum_stats()}\n (root/'checkpoint.json').write_text(json.dumps(checkpoint));print(json.dumps(checkpoint),flush=True);continue\n if answer is False","sha256":"502463686ea79a9911e5d9146268126aa74606de2e38af30b8f34583eca9f365"},{"name":"general_source_lines_pc.py.part3","contentText":":status='UNSAT_UNCERTIFIED';break\n model=solver.get_model();values=set(model);assert all(any(v in values for v in c) for c in cnf.clauses)\n points=sorted(((v-1)//75,(v-1)%75) for v in model if 1<=v<=5625);assert len(points)==150\n overlap=len(set(points)&set(source));assert overlap<=139\n bad,count=violations(points);models+=1\n if not bad:\n (root/'candidate150-frozen.json').write_text(json.dumps({'points':points,'model':model,'source_sha256':sha(__file__),'seed':'deterministic109partialhint','lineage':['SOL-EXP-0109','SOL-EXP-0115'],'source_overlap':overlap},indent=2))\n checks=[check(points,75),check(points,75,'directions')];assert all(c['valid'] for c in checks)\n (root/'candidate150-verification.json').write_text(json.dumps(checks,indent=2));status='CANDIDATE150_VERIFIED';break\n if best is None or count