On the Sufficiency of SAT Features for Genetic Algorithm Parameter Selection

SAT Feature-Based IGA Parameter Prediction This project investigates whether structural properties of SAT problem instances can inform the selection of optimal Island Genetic Algorithm (IGA) parameters. By training machine learning models to predict IGA configurations from SAT features, we aim to understand which problem characteristics most influence algorithm performance. Research Questions RQ1 (Sufficiency): Can learned configurations outperform a single best manually selected parameter set on unseen instances? RQ2 (Ablation): Can accurate predictions be achieved with reduced feature sets? RQ3 (Explainability): Which SAT features are most critical when tuning GA parameters? RQ4 (Correlation): Are the selected feature subsets correlated across different IGA parameters? Project Structure . ├── SAT instances/ # SAT problem instances from SATLIB │ ├── GA implementation and parameters/ # CUDA C++ IGA implementation │ ├── Obtaining GA parameter configuration/ # iRace tuning with active learning │ └── Final analysis of gathered data/ # ML-based analysis and results ├── best_configurations.xlsx ├── satzilla_features.csv ├── process_data_to_sets.py ├── Classification/ ├── Regression/ ├── Preliminary analysis/ ├── Feature ablation study/ ├── SAT feature sufficiency/ ├── IGA parameter impact/ └── Subsets correlations/ 1. SAT Instances Source dataset from the SATLIB benchmark library containing 44,675 instances. A representative subset of 2,000 instances was selected for tuning using active learning (see Section 3). SAT Features: State-of-the-art human-crafted features from the SATzilla feature set are used to characterize problem instances. 2. GA Implementation and Parameters Architecture The study uses an Island-Model Genetic Algorithm (IGA) implemented in CUDA C++ for GPU execution. The algorithm was run on eight NVIDIA V100 GPUs with a termination condition of either finding a solution or reaching 2,500,000 function evaluations. Algorithm Components Component Options Selection Tournament, Roulette wheel, Linear/Nonlinear rank-based Crossover Uniform, Single-point, Two-point Mutation Bit-flip, Single-point, Two-point Succession Elitism, No elitism, Steady-state Migration Ring, Star, Random topology Population Structure The population is partitioned into semi-isolated subpopulations (islands) that evolve independently with periodic migration to maintain genetic diversity while enabling parallel exploration. Migration Topologies Ring: Unidirectional circular migration (island i → island i+1 mod n) Star: Two-phase protocol through central hub (island 0) Random: Stochastic derangement permutation at each migration event Numerical Parameter Bounds Parameter Type Min Max Population size integer 256 2048 Migration frequency integer 10 500 Islands integer 2 8 Crossover rate real 0.0001 1.0 Mutation rate real 0.0001 1.0 Migration batch real 0.02 0.4 Fitness Function Solutions are evaluated by counting unsatisfied clauses, with the objective of minimizing this count to zero (satisfying assignment). 3. Obtaining GA Parameter Configuration Tuning Framework IGA parameters were tuned using iRace on 2,000 SAT instances. Preliminary experiments showed that tuning each instance individually requires approximately 2 hours (5,000 algorithm runs), making full dataset tuning impractical (~89,350 hours total). Configuration Scoring Configurations are evaluated using a score prioritizing solution quality over computational effort: $$f = C_S - \frac{n_{\text{eval}}}{N_{\max}}$$ where C_S is the number of satisfied clauses, n_{\text{eval}} is the number of evaluations, and N_{\max} = 2{,}500{,}000 is the maximum budget. Active Learning Pipeline To construct an informative and structurally diverse dataset, we employed active learning rather than random sampling: 1. Seed Selection (200 instances) DBSCAN clustering on precomputed SAT features 75% budget allocated to outliers (underexplored regions) Remaining budget distributed proportionally across clusters KMeans used to select representatives nearest to cluster centroids 2. Iterative Batch Selection (50 instances/round) Multi-output AutoGluon model trained to predict all configuration parameters Inverse Propensity (InvProp) weighting to address class imbalance Classes with cumulative frequency < 10% merged into "rare" category Uncertainty computed as entropy (classification) or ensemble variance (regression) Acquisition score combines InvProp weights with uncertainty Diversity enforced via weighted KMeans clustering 3. Iteration Model retrained after each batch Process repeated until 2,000 instances labeled 4. Final Analysis of Gathered Data 4.1 Preliminary Analysis Eigenvalue Decomposition: Features are standardized and the Pearson correlation matrix eigenvalues are computed to quantify feature redundancy. Large eigenvalues indicate directions where multiple features co-vary. Target Distribution Analysis: Skewness coefficient quantifies asymmetry in continuous parameter distributions: $$\text{Skew}(y) = \frac{1}{n} \sum_{i=1}^{n} \left( \frac{y_i - \mu}{\sigma} \right)^3$$ 4.2 Evaluation Metrics Task Metric Formula Classification Balanced Accuracy \text{BA} = \frac{1}{C}\sum_{c=1}^{C} \frac{TP_c}{TP_c + FN_c} Regression R² R^2 = 1 - \frac{\sum (y_i - \hat{y}_i)^2}{\sum (y_i - \bar{y})^2} 4.3 Feature Ablation Study Sequential Forward Selection (SFS) identifies minimal informative feature subsets. Models (Random Forest, XGBoost) are trained with subsets of size: 50, 25, 10, 5, 4, 3, 2, 1 features. Optimal Subset Selection: Identify subset achieving highest BA or R² Among subsets within 95% of best performance, select the smallest Data Augmentation: SVMSMOTE — Synthetic minority oversampling for classification SMOGN — Synthetic minority oversampling for regression 4.4 SAT Feature Sufficiency Model performance is compared against naive baselines (most frequent class for classification, mean value for regression) to verify that SAT features provide meaningful predictive signal. 4.5 IGA Parameter Impact Analysis of which SAT features most influence specific IGA parameters, providing explainability for configuration decisions. 4.6 Feature Subset Correlation Subsets are compared using Pearson correlation (features match if |r| ≥ 0.9): $$\text{Similarity}(A \rightarrow B) = \frac{|{f \in F_A : \exists \ g \in F_B, \ |r(f,g)| \geq 0.9}|}{|F_A|}$$ This asymmetric similarity matrix reveals shared feature structures across prediction tasks. Directory Structure (Final Analysis) Final analysis of gathered data/ ├── best_configurations.xlsx # Optimal IGA configurations per instance ├── satzilla_features.csv # SAT instance features ├── process_data_to_sets.py # Dataset preparation script │ ├── Classification/ # Categorical IGA parameters │ ├── crossover.csv │ ├── migration.csv │ ├── mutation.csv │ ├── selection.csv │ └── succession.csv │ ├── Regression/ # Continuous IGA parameters │ ├── crossover_rate.csv │ ├── islands.csv │ ├── migration_batch.csv │ ├── migration_freq.csv │ ├── mutation_rate.csv │ └── pop_size.csv │ ├── Preliminary analysis/ │ ├── eigenvalue_analysis.py │ ├── eigenvalue_analysis.png/pdf │ ├── imbalance_tables.py │ ├── plot_configurations_frequencies.py │ └── best_configurations_frequencies.png │ ├── Feature ablation study/ │ ├── sequential_features_selection.py │ ├── get_predictions.py │ ├── recalculate_log_metrics.py │ ├── overlapping_classification_chart.py │ ├── overlapping_regression_chart.py │ ├── sequential_classification.png │ └── sequential_regression.png │ ├── SAT feature sufficiency/ │ ├── run_sat_solver.py │ ├── run_single_config.py │ ├── summary_table.py │ ├── convert_csv_results_to_xlsx.py │ ├── all_results.csv │ ├── optimal_results.csv │ ├── tuned_results.csv │ ├── predicted_configs_*.csv/xlsx │ └── best_configurations.xlsx │ ├── IGA parameter impact/ │ └── generate_tables_for_features_explainability.py │ └── Subsets correlations/ ├── calculate_correlation_similarity_matrix.py ├── correlation_similarity_matrix.csv └── correlation_similarity_matrix.png Prediction Targets Classification (Categorical Parameters) Parameter Description crossover Crossover operator type (uniform, single-point, two-point) mutation Mutation operator type (bit-flip, single-point, two-point) selection Selection mechanism (tournament, roulette, rank-based) succession Replacement strategy (elitism, no elitism, steady-state) migration Migration topology (ring, star, random) Regression (Continuous Parameters) Parameter Description Range pop_size Population size 256–2048 crossover_rate Crossover probability 0.0001–1.0 mutation_rate Mutation probability 0.0001–1.0 islands Number of islands 2–8 migration_freq Migration frequency (generations) 10–500 migration_batch Migration batch size (fraction) 0.02–0.4 Dependencies Python 3.8+ AutoGluon scikit-learn XGBoost pandas, numpy matplotlib, seaborn imbalanced-learn (SVMSMOTE) smogn CUDA toolkit (for GA implementation) Workflow # 1. Prepare datasets from tuning results python "Final analysis of gathered data/process_data_to_sets.py" # 2. Run preliminary analysis python "Final analysis of gathered data/Preliminary analysis/eigenvalue_analysis.py" python "Final analysis of gathered data/Preliminary analysis/imbalance_tables.py" # 3. Perform feature selection python "Final analysis of gathered data/Feature ablation study/sequential_features_selection.py" # 4. Evaluate SAT feature sufficiency python "Final analysis of gathered data/SAT feature sufficiency/run_sat_solver.py" python "Final analysis of gathered data/SAT feature sufficien