Keywords
Machine Learning, Meta-Classification

Technologies
Ensemble Learning, Recursive Feature Elimination

This project develops a lightweight, two-stage machine learning portfolio for optimal #SAT solver selection. While model counting is #P-complete, no single solver dominates all structures. This system utilizes Recursive Feature Elimination (RFE) to identify a minimal 48-feature subset, significantly reducing pre-execution overhead compared to traditional 75-feature suites.

The architecture consists of an ExtraTrees "Hardness Predictor" to filter unsolvable instances and a RandomForest "Counter Selector" to route solvable formulas. In final 5-fold cross-validation, the optimized pipeline achieved 1,390 exact counts, strictly outperforming the Single Best Solver (GPMC).

By closing 50.21% of the performance gap to the theoretical Oracle, the portfolio achieved a PAR-2 score of 6,342,331 and saved 550,000 seconds (6.37 days) of wall-clock CPU time. These results demonstrate that a mathematically optimized, dual-model approach effectively mitigates catastrophic timeouts and improves resource utility in real-world model counting environments.