Advancing the theory and engineering of SAT/MaxSAT/Pseudo-Boolean encodings, exact decision solvers, and verified algorithms for industrial scheduling, 2D packing, graph labeling, and software verification.
We build specialized SAT encodings and exact solver pipelines that outperform standard commercial MIP/CPLEX/Gurobi solvers on hard combinatorial optimization problems.
New Sequential Counter (NSC), Cardinality constraints (AMO/AMK/ALK), Pseudo-Boolean (PB) encodings, and the SCLib solver ecosystem.
Power Peak Minimization in Assembly Line Balancing (SALB, UALBP), Job-Shop Scheduling (JSSP/FJSSP), and Train Rescheduling via MaxSAT-DDD.
Exact SAT/MaxSAT models for 2D Strip Packing, 2D Bin Packing, and Cutting Stock Problems with non-overlapping constraints.
SAT-based exact algorithms for Antibandwidth, Cyclic Antibandwidth, Bandwidth Multicoloring, Radio-k Labeling, and k-Safe Labeling.
An academic monograph synthesizing theoretical foundations and software engineering practices for optimal SAT encodings.
We welcome motivated undergraduate, master, and PhD students with strong backgrounds in algorithms, discrete mathematics, and software development.
View Openings & Student Opportunities ↗