Tuyen Van Kieu

Tuyen Van Kieu, Chi Linh Hoang, Khanh Van To

Cutting rectangular items from stock sheets to satisfy demands while minimizing waste is a central manufacturing task. The Two-Dimensional Single Stock Size Cutting Stock Problem (2D-CSSP) generalizes bin packing by requiring multiple copies of each item type, which causes a strong combinatorial blow-up. We present a SAT-based framework where item types are expanded by demand, each copy has a sheet-assignment variable and non-overlap constraints are activated only for copies assigned to the same sheet. We also introduce an infeasible-orientation elimination rule that fixes rotation variables when only one orientation can fit the sheet. For minimizing the number of sheets, we compare three approaches: non-incremental SAT with binary search, incremental SAT with clause reuse across iterations and weighted partial MaxSAT. On the Cui--Zhao benchmark suite, our best SAT configurations certify two to three times more instances as provably optimal and achieve lower optimality gaps than OR-Tools, CPLEX and Gurobi. The relative ranking among SAT approaches depends on rotation: incremental SAT is strongest without rotation, while non-incremental SAT is more effective when rotation increases formula size.

Tuyen Van Kieu, Tan Huu Nguyen, Khanh Van To

Train rescheduling repairs disturbed timetables while enforcing train-path precedence, resource capacity, and delay objectives. Dynamic Discretization Discovery (DDD) avoids full time discretization by refining only time points needed to certify feasibility and optimality. We strengthen a recent MaxSAT-DDD model through two encoding changes. First, resource conflicts are encoded as time-dependent at-most-one cliques, using pairwise clauses for small cliques and a sequential counter for large cliques. Second, earliest feasible times are propagated along train paths before the first DDD iteration. We evaluate four MaxSAT variants, two SAT optimization backends, Gurobi/CPLEX MILP models, and CPLEX CP on 72 instances and three delay objectives. MaxSAT-DDD solves all stepwise instances in about 23 ms on average. MaxSAT-Default reduces rounded-cost runtime from 794 to 479 ms, and the ablation study reports up to 79.6\% runtime reduction on the common-solved subset of hard continuous track instances.