Zhengling Yangli's Homepage

School of Mathematics and Statistics

Yunnan University

Kunming, Yunnan, China

Zhengling Yangli (杨李正凌) is an undergraduate student of Statistics at Yunnan University (2024–).

Her current research interests are in combinatorial optimization and Boolean satisfiability solving, specifically: diverse-model enumeration for SAT/MaxSAT, MaxSAT encodings of non-linear integer programs, lower-bound search for the minimum weight dominating set, and extensions of fair multi-resource allocation under partial accessibility. Methodologically she prefers to start from a concrete empirical anomaly, work out a first-principles mechanism, and design the next experimental intervention from there, rather than rely on broad hyperparameter sweeps.

Research Map

SAT / MaxSAT

Diverse solutions and integer encodings

Question. How can we move from finding one feasible assignment to finding a set of structurally different assignments?

Result. DiverseSAT uses DW / IW threshold encodings and is evaluated on 289 instances across 7 benchmark families; the NLIP project further encodes QPLIB and SMT-LIB QF\_NIA instances into weighted MaxSAT.

DiverseSAT · NLIP via MaxSAT

MWDS

Lower-bound search in Dual-Bound Search

Question. After the LB side becomes numerically tighter, how can the improvement actually propagate to the UB side through hard proof rules?

Result. Ant-Q plug-ins reduce the row-averaged gap of `Deep-v6` by 23.7%–31.2% and reveal a structural decoupling between LB tightening and `#opt`.

AntQO for MWDS · note

Fair Allocation

Fairness under partial accessibility

Question. Under meta-type resource accessibility, can we improve social welfare while preserving the core fairness constraints?

Result. UNB-MT differentiates dominant shares on top of DRF-MT and identifies why a linear EF sufficient condition becomes over-tight under partial access.

UNB-MT · note

Applied Projects

Reproducible modeling on real data

Question. When data comes from real systems rather than clean benchmarks, how can the modeling pipeline remain interpretable and reproducible?

Result. Applied projects cover retrieval-augmented mathematical reasoning, platform-market analysis, wearable EEG signals, and minimum-cost flow modeling.

applied projects · MathRAG

Research notes and post-mortems on misjudgments are collected at /notes/.

Email is the most reliable way to reach me.

selected publications

Under Review

DiverseSAT: Finding k Diverse Satisfying Assignments via Threshold Encodings and Incremental Solving

Zhengling Yangli, Saïd Cherif, and others

Under Review, 2026

Submitted to JAIR

Abs PDF

We study the problem of computing k maximally diverse satisfying assignments of a propositional formula, a setting with applications to bounded model checking (e.g., all-zero / all-one witnesses) and robust network path design. We propose two encodings — Direct Weight (DW) and Incremental Weight with incremental totalizer (IW) — and three search strategies (binary-lifting, binary-search, SAT-UNSAT), together with a model-aware refinement that exploits partial solutions. Experiments on 289 instances across 7 benchmark families show that our approach consistently outperforms MaxSAT, Pseudo-Boolean and CPLEX baselines.
Under Review

Encoding Non-linear Integer Programs into Weighted MaxSAT: A Systematic Study

Zhengling Yangli, Saïd Cherif, and others

Under Review, 2026

Submitted to SAT 2026 (CCF-B)

Abs

We investigate the encoding of non-linear integer programs (NLIP) — polynomial objectives and constraints over bounded integer variables — into weighted MaxSAT. Four encoding families are studied (one-hot, unary, binary, and binary with order decomposition) and evaluated on QPLIB (137), SMT-LIB QF_NIA (2591) and Diverse-SAT (287) benchmarks against Z3, CPLEX and CaDiCaL baselines. We identify when MaxSAT-based encoding dominates and diagnose a fundamental limitation of unary encoding at large domain sizes.
Working Paper

Ant-Q: A Lightweight Ant-Colony + Q-Learning Plug-in that Tightens Lower Bounds for Minimum Weight Dominating Set

Zhengling Yangli and others

Working Paper, 2026

Built on ECAI-2025 baselines

Abs

Building on the Dual-Bound Search (DBS) framework of the ECAI 2025 baselines Dual-Deep and Dual-Fast, we plug a K-ant Ant-Q module into the LB-side pair construction of ibmwds_init_bounds, without touching the UB search. The resulting variants Deep-v6 and Fast-v19 reduce the row-averaged gap by 23.68%/31.23% (T1/T2) on Deep and by 6.92%/9.89% (T1/T2) on Fast, with instance-level win rates up to 99.37%. A central finding is the asymmetry between gap and #opt: tightening LB alone does not shrink UB unless it triggers hard reduction rules.