Chu Min Li

AIJ Journal 2012 Journal Article

Optimizing with minimum satisfiability

• Chu Min Li
• Zhu Zhu
• Felip Manyà
• Laurent Simon

MinSAT is the problem of finding a truth assignment that minimizes the number of satisfied clauses in a CNF formula. When we distinguish between hard and soft clauses, and soft clauses have an associated weight, then the problem, called Weighted Partial MinSAT, consists in finding a truth assignment that satisfies all the hard clauses and minimizes the sum of weights of satisfied soft clauses. In this paper we describe a branch-and-bound solver for Weighted Partial MinSAT equipped with original upper bounds that exploit both clique partitioning algorithms and MaxSAT technology. Then, we report on an empirical investigation that shows that solving combinatorial optimization problems by reducing them to MinSAT is a competitive generic problem solving approach when solving MaxClique and combinatorial auction instances. Finally, we investigate an interesting correlation between the minimum number and the maximum number of satisfied clauses on random CNF formulae.

AAAI Conference 2000 Conference Paper

Integrating Equivalency Reasoning into Davis-Putnam Procedure

• Chu Min Li

Equivalency clauses (Xors or modulo 2 arithmetics) represent a common structure in the SAT-encoding of many hard real-world problems and constitute a major obstacle to Davis- Putnam (DP) procedure. We propose a special look-ahead technique called equivalency reasoning to overcome the obstacle and report on the performance of an equivalency reasoning enhanced DP procedure on SAT instances containing equivalency clauses derived from problems in parity learning, cryptographic key search and model checking. Our results show that integrating equivalency reasoning renders easy many problems which were beyond DP’s reach. We also compare equivalency reasoning with general CSP look-back techniques on equivalency clauses.

IJCAI Conference 1997 Conference Paper

Heuristics Based on Unit Propagation for Satisfiability Problems

• Chu Min Li
• Anbulagan