I’m sharing my new paper, CoverTrace-SAT as Disjoint-Subcube Knowledge Compilation.” It reframes CNF-SAT/#SAT geometrically: clauses forbid axis-aligned subcubes of the Boolean hypercube, and we maintain an exact disjoint cover (DSOP-style) so model counting becomes additive and witness extraction is constructive. The paper formalizes correctness, analyzes fragmentation as the central complexity driver, proves explicit exponential worst-case lower bounds for disjoint subcube covers, and discusses the conditional consequence that uniform polynomial-size disjoint-cover compilation would imply #SAT ∈ P and collapse PH. Code is included for reproducibility and benchmarking.
CoverTrace-SAT as Disjoint Subcube Knowledge Compilation
- 2-watched literals propagation
- 1-UIP conflict analysis and backjumping
- VSIDS variable activity + decay
- Phase saving
- Luby restarts
- LBD scoring (Glucose-style) + learned DB reduction
- Final model verification (never prints SAT with invalid assignment)
- While CDCL runs, we continuously feed a filtered stream of *entailed clauses* (learned clauses with low LBD / small size, plus optionally original clauses) into CoverTrace.
- If CoverTrace proves coverage of {0,1}^n, we can conclude UNSAT early.
- Optional: CoverTrace witness (when y>0) is used to set CDCL phase preferences.
g++ -O3 -std=c++17 -march=native -DNDEBUG covertrace_sat.cpp -o covertrace_sat -static
./covertrace_sat instancia.cnf
./covertrace_sat --count --ct-maxu 200000 instancia.cnf
./covertrace_sat --count-only --ct-maxu 200000 instancia.cnf
./covertrace_sat --covertrace --count --ct-maxu 200000 instancia.cnf