Zhengling Yangli's Homepage

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.

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.

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.