This repository contains the practical assignments completed for the course TOIA (Techniques d'Optimisation et IA). Developed by team F6score, it includes Jupyter notebooks and comprehensive reports detailing our approaches to solving the MAX-SAT problem.
The unweighted MAX-SAT problem consists of finding a boolean variable assignment that maximizes the number of satisfied clauses in a given Conjunctive Normal Form (CNF) formula. This work explores the problem from multiple angles: exact methods, constructive heuristics, local search, and population-based metaheuristics. It features implementations of established state-of-the-art algorithms from the literature, as well as several original contributions designed to improve robustness and convergence.
- MESSAOUD Amal - ma_messaoud@esi.dz
- KELLOU Lylia Ines - ml_kellou@esi.dz
- DJAFOUR Touria - mt_djafour@esi.dz
- DJOUAHER Yasmine - my_djouaher@esi.dz
- BOUSSEKINE Wissal - mw_boussekine@esi.dz
- OUAKKI Mohamed Shamseddine - mm_ouakki@esi.dz
The work is organized into four main parts, representing the progressive exploration of optimization techniques. All algorithms were evaluated using standard SATLIB benchmark instances (e.g., uf20-01, uf75-01, uuf100-01) at the phase transition.
Report: B&B report.pdf
Explores complete search methods guaranteeing optimal solutions.
- Implemented Algorithms:
V0: Baseline Branch & Bound (Zhang et al., 2003)V1: Heuristic initialization using GSAT (Borchers & Furman, 1999)V2: Addition of inference rules for early conflict detection (Li et al., 2007)
- 🌟 Original Contribution (
V3): A hybrid approach introducing advanced bound evaluation using Unit Propagation (UP) and a conflict-based branching heuristic. This drastically reduced the search tree size compared to standard baselines.
Report: Heuristics report.pdf
Studies incomplete methods that trade optimality for speed, divided into three families.
- Construction Methods: Greedy, Jeroslow-Wang (JW)
- Neighborhood Methods: GSAT, GWSAT, HSAT, GSAT/TABU
- Clause Weighting: PAWS, SAPS
- 🌟 Original Contribution (
SAPS-Smart): An enhancement of the SAPS algorithm introducing Best of Multiple Samples (BMS) to reduce the complexity per flip from$O(n)$ to$O(k)$ , combined with an intelligent perturbation/restart mechanism based on the best-known solution.
Report: TP3_recherche_locale_F6_score.pdf
Focuses on single-solution based metaheuristics and advanced hybridizations.
- Classic Local Search: Random Walk (RW), Hill Climbing (HC), Simulated Annealing (SA), Tabu Search (TS)
- Hybrid Algorithms:
VNS-WalkSAT: Combines WalkSAT's make/break heuristic with Variable Neighborhood Search (VNS), optimized with incremental scoring via watch lists.IRoTS: Iterated Robust Tabu Search combining long intensification phases with guided perturbation phases.
Report: rapport_AG___Swarm_intelligence.pdf
Compares evolutionary and swarm intelligence approaches.
- Genetic Algorithms: GA-1 (Standard), GA-3 (Memetic with local search), GASAT (Tabu-augmented GA)
- Swarm Intelligence: Ant Colony Optimization (ACO), Bee Colony Optimization (BCO), Binary Particle Swarm Optimization (PSO)
- 🌟 Original Contribution (
GASAT-RESTART): Addresses the premature convergence issue of standard GASAT. It introduces a stagnation detection mechanism paired with adaptive population restarts, injecting the best-known solution (elitism) to maintain robustness—achieving 0 standard deviation on hard unsatisfiable instances.
- Language: Python 3.12
- Key Libraries: NumPy 2.0, Optuna 4.8
- Hyperparameter Optimization (HPO): Extensive use of the Optuna framework (TPE Sampler) was made across TPs 3 and 4 to independently calibrate algorithm parameters and ensure fair comparisons.
All implemented algorithms are rigorously based on published academic papers. Full citations and bibliographies are available at the end of each respective PDF report in the repository.