1M 变量,19.66s,95.36

Zenodo (CERN European Organization for Nuclear Research) 2026 Open access

Read full text
Authors: Dequan Yang
DOI: 10.5281/zenodo.18787730
Cited by: 0

Abstract

Million-Scale Max-3-SAT Solver | EEP-Powered Solve 1M-variable Max-3-SAT in 19.66s (single core) with 95.36% satisfaction—no OOM, no multi-hour runtime. Built on Lagrangian dual equilibration (EEP), it extracts a 4.6% Unsat Core for industrial constraint diagnosis, outperforming MaxHS/Kissat/WalkSAT on large-scale instances.

Fields of Study & Subjects

Constraint Satisfaction and Optimization Formal Methods in Verification Advanced Graph Theory Research

Publication details

Journal / source
Zenodo (CERN European Organization for Nuclear Research)
Publication date
26 February 2026
Language
EN