I'm a professor of computer science at the University
of Picardie Jules Verne. My research is concerned with the practical resolution
of NP-hard problems, including SAT, CSP, MaxSAT, MinSAT, MaxClique, GCP. I am
particularly interested in the intrinsical
relationships between these problems. One of my research directions is to find
and exploit these relationships to solve them. A recent example is the
exploitation of the relationships between MaxSAT and MaxClique to solve MaxClique, see
below.

**Algorithms: **

**The source codes of
different solvers are available below. Thanks for letting me
know all your remarks or suggestions.**

**WLMC: An Exact
Algorithm for the Maximum Weight Clique Problem in large graphs**

This exact algorithm is
even faster than the best heuristic algorithms for Maximum Weight Clique
Problem in large graphs, even when including the time needed for proving the
optimality of its solutions. The source code is
available here.

Reference:

Hua Jiang, Chu-Min Li, Felip Manya, An Exact Algorithm
for the Maximum Weight Clique Problem in large graphs. In Proceedings of
31nd AAAI Conference on Artificial Intelligence (AAAI-17), AAAI Press, Vol 2,
pages 830-838, San Francisco, USA, 2017.

**MaxCLQ**** for MaxClique**

**- Combining Incremental
Upper Bound and MaxSAT reasoning for MaxClique**

MaxSAT reasoning is powerful in
computing upper bounds for the cardinality of a maximum clique of a graph.
However, existing upper bounds based on MaxSAT
reasoning have two drawbacks: (1) at every node of the search tree, MaxSAT reasoning has to be performed from scratch to
compute an upper bound and is time-consuming; (2) due to the NP-hardness of the
MaxSAT problem, MaxSAT
reasoning generally cannot be complete at a node of a search tree, and may not
give an upper bound tight enough for pruning search space. We thus propose an
incremental upper bound and combine it with MaxSAT
reasoning to remedy the two drawbacks. The new approach is used to develop an
efficient branch-and-bound algorithm for MaxClique,
called **IncMaxCLQ**,
which is very efficient and *closes an
additional DIMACS instance **(**hamming10-4.clq) in less than 7 days *on an INTEL XEON E5-2680
(2.7Ghz, 20M Cache and
16GB memory) under Linux*.*

An executable of the incremental MaxCLQ for Linux is available here.

The source code of the incremental MaxCLQ is available here.

__Reference :__

Chu Min LI, Zhiwen
Fang, Ke XU, Combining MaxSAT Reasoning
and Incremental Upper Bound for the Maximum Clique Problem, in proceedings of the 2013 IEEE 25th International
Conference on Tools with Artificial Intelligence (ICTAI2013), Pages 939-946.

**- Upper Bound Based on MaxSAT
Reasoning for MaxClique**

Branch-and-bound algorithms for the Maximum Clique
problem (MaxClique) usually partition a graph into
independent sets to compute an upper bound for the size of a maximum clique of
the graph, since every independent set can have at most one vertex in a clique.
However, this upper bound cannot be very tight for two reasons :
(1) partitioning a graph into independent sets is equivalent to coloring the
graph, which is even harder than MaxClique in
practice, so the partition cannot be optimal in every node of the search
tree ; (2) even if the partition is optimal, the number of independent
sets is strictly larger than the size of
a maximum clique for imperfect graphs (by definition of imperfect
graphs). Note that MaxClique and the graph coloring
problem are polynomial for perfect graphs.

The upper bound based on independent sets can be
significantly improved using MaxSAT reasoning. In
every node of the search tree, we dynamically encode a MaxClique
instance into a partial MaxSAT problem and use MaxSAT reasoning to underestimate the number of independent
sets that cannot have a vertex in the maximum clique, obtaining MaxCLQ, a highly efficient branch-and-bound solver for MaxClique.

An executable MaxCLQ
for Linux is available here. This version is described in the ICATI2010
paper and improved from the version presented in the AAAI2010 paper.

The source
code of MaxCLQ is here.

__References____ :__

Chu Min LI, Zhe Quan. 2010. Combining Graph Structure
Exploitation and Propositional Reasoning for the Maximum Clique Problem, in proceedings of the 22th IEEE International Conference
on Tools with Artificial Intelligence (ICTAI2010), Arras, France, October 2010,
Pages 344-351.

Li, C. M., and Quan, Z., 2010, An efﬁcient branch-and-bound algorithm based on
maxsat for the maximum clique problem. In *Proceedins** of AAAI-10*, Pages 128-133.

**MinSatz****: A branch and bound algorithm for
the minimum satisfiability problem.**

MinSAT is an optimization extension
of SAT and it is the dual problem of MaxSAT, aiming
at finding a truth assignment to minimize the number of satisfied clauses. It
is complementary with MaxSAT when solving combinatorial
optimization problems. Its code source is
available here.

References:

Chu Min Li, Zhu Zhu, Felip
Manya, Laurent Simon, Minimum satisfiability and its
applications, In : Proceedings of the 22nd
International Joint Conference on Artificial Intelligence (IJCAI-2011), pp
605-610, 2011.

Chu-Min Li, Zhu Zhu, Felip
Manya, Laurent Simon. Optimizing
with Minimum Satisfiability, In Artificial Intelligence 190 (2012) 32-44.

**Sattime****: An efficient local search solver
for SAT**

Sattime is a Stochastic Local Search
(SLS) solver for SAT, that exploits the satisfying history of clauses, instead
of falsifying history of clauses as in most other SLS solvers, in selecting the
next variable to flip. Sattime participated in the 2011 SAT competition and
won a silver medal in the ran- dom
category. Especially, Sattime beat easily all the
Conflict Driven Clause Learning (CDCL) solvers in the crafted sat category (Sattime solved 109 instances while the best CDCL only
solved 93 instances), although SLS has been considered less effective than CDCL
for structured SAT problems for a long time. This is the first time that a SLS
solver enters the final phase of the SAT competition in the crafted category
and beats there all the CDCL algorithms on structured SAT problems.

Sattime confirmed its performance in the SAT challenge
2012, as the best SLS solver in the crafted (Hard Combinatorial
SAT+UNSAT) category and the second best single engine solver in the random SAT
category.

The source codes of Sattime
are available here.

* Reference :*

Chu Min Li and Yu Li, Satisfying versus Falsifying in
Local Search for Satisfiability, in proceedings of SAT2012, Springer LNCS 7317, pp. 477–478, 2012.

**Maxsatz****: A branch and bound solver for Max-SAT**

A branch and bound solver for Max-SAT that
incorporates into a Max-SAT solver some of the technology developed for **Satz** (see below). At each node of the proof tree it transforms the
formula into an equivalent formula that preserves the number of unsatisfied
clauses by applying some efficient refinements of unit resolution that the
authors have defined for Max-SAT (e.g., it replaces $x, y, \neg x \vee \neg y$ with $\Box, x \vee y$, it replaces $x, \neg x \vee y, \neg x \vee z, \neg y \vee \neg
z$ with $\Box, \neg x \vee
y \vee z, x \vee \neg y \vee \neg
z$). MaxSatz implements a lower bound
computation method that consists of incrementing the lower bound by one for
every disjoint inconsistent subset that can be detected by unit propagation.
Moreover, the lower
bound computation method is enhanced with failed literal
detection. The variable selection heuristics takes into account the number of
positive and negative occurrences in binary and ternary clauses Maxsatz and its variants are the best performing solvers in
the unweighted maxsat category in the 2006 maxsat
solvers evaluation and the 2007 maxsat solvers evaluation.

The source codes of maxsatz
are available here.

The weighted version of maxsatz (wmaxsatz2009)
is available here.

An executable, called maxsatz2013f, that participated in the MaxSAT evaluation 2013 is available here. Maxsatz2013f is significantly faster than the previous versions of maxsatz and is one of the best solvers in the MaxSAT evaluation 2013.

**
References: **

Chu Min LI, Felip Manya, Nouredine
Mohamedou, Jordi Planes, "Exploiting Cycle Structures in
Max-SAT". In proceedings of 12th
international conference on the Theory and Applications of Satisfiability
Testing (SAT2009), Springer, LNCS 5584,
pages 467-480, June-July 2009, Swansea, United Kindom.

Chu Min LI, Felip Manya,
Jordi Planes, "New Inference Rules for Max-SAT", in
Journal of Artificial Intelligence Research, October 2007, Volume 30, pages
321-359

Chu Min LI, Felip Manya,
Jordi Planes, "Detecting disjoint inconsistent subformulas for computing lower bounds for
Max-SAT". In Proceedings of the 21st
National Conference on Artificial Intel ligence
(AAAI-06), Boston, USA, pp. 86–91. AAAI Press.

**TNM** (Wanxia
Wei, Chu Min Li):

A local search procedure based on **G2wsat** (see
below) and using two different adaptive noise mechanisms: Hoos
mechanism and a new adaptive noise mechanism based on the history of the most
recent consecutive falsiﬁcations of a clause. TNM automatically switches
between these two mechanisms during search according to the variable weight
distribution. No parameter is needed to adjust when using TNM. TNM won a *GOLD
Medal *in the SAT2009 competition in satisfiable
random formula category. The version used in the competition
(using input and output format of the competition) as well as a
short presentation of the procedure can be obtained here.

* **Reference:*

Chu
Min Li, Wanxia Wei, and Yu
Li, Exploiting
Historical Relationships of
Clauses and Variables in Local Search for Satisfiability, in proceedings
of SAT2012, Springer LNCS 7317, pp. 479–480, 2012.

**Adaptg2wsat2009++** (Chu Min Li, Wanxia Wei):

A local search procedure based on **G2wsat** (see
below) by integrating the adaptive noise mechanism of Hoos.
No parameter is needed to adjust when using adaptg2wsat2009++. Adaptg2wsat2009++
won a *Bronze Medal *in the SAT2009 competition in satisfiable
random formula category. The version used in the competition (using
input and output format of the competition) as well as a short presentation of
the procedure can be obtained here.

**Adaptg2wsat0**
(Chu Min Li, Wanxia Wei and Harry Zhang):

A local search procedure based on **G2wsat** (see
below) by integrating the adaptive noise mechanism of Hoos.
No parameter is needed to adjust when using adaptg2wsat0. Adaptg2wsat0 won a *Silver
Medal *in SAT2007 competition in satisfiable
random formula category. The version used in the competition (using input
and output format of the competition) as well as a short presentation of the
procedure can be obtained here. The normal version can be found here.

** Adaptg2wsat+** (Chu Min Li, Wanxia Wei and
Harry Zhang):

A
local search procedure based on G2wsat
by integrating the adaptive noise and random walk mechanisms
of Hoos. No
parameter is needed to adjust when using adaptg2wsat+. Adaptg2wsat+ won a *Bronze
Medal* in SAT2007 competition in satisfiable
random formula category. The version used in the competition (using input and output
formats of the competition) as well as a short presentation of the procedure
can be obtained here.

*
References for Adaptg2wsat0 and Adaptg2wsat+:*

**
**Chu Min Li, Wanxia Wei,
Harry Zhang, "Combining Adaptive Noise and Look-Ahead
in Local Search for SAT". In proceedings of 10th
international conference on the Theory and Applications of Satisfiability
Testing (SAT2007), Lisbon, Portugal, May 2007.

**G2wsat **(Chu Min LI & Wenqi HUANG):

A local search
procedure which won a *Silver Medal* in SAT2005 competition in satisfiable random
formula category. The version used in the competition as well as a short presentation of the
procedure can be obtained here. The current
version (2005) is optimized after the competition and is
generally more than 50% faster. To get
the source code of current g2wsat (version 2005), click here.

**
Reference:**

Chu
Min LI & Wenqi HUANG, "Diversification and Determinism in
Local search

for Satisfiability", in proceedings of 8th international conference, SAT2005, LNCS
3569 Springer, St Andrews, UK, June 2005, Pages 158-172

** Satz215.2**:

Satz215 is Satz214 + Detection of implied literals
suggested by Daniel Le Berre. Satz215 solves more
structured instances than Satz214. Particularly, Satz215 solves 3bitadd_31 and
3bitadd_32 in a few seconds. Satz215.1 is Satz215 modified in which the
preprocessing only adds up to 10*INIT_NB_CLAUSE ternary resolvents
into a formule with initially INIT_NB_CLAUSE clauses.

To get the source code of Satz215.2, click here.

** Satz214.2** (Li and Anbulagan) :

Satz214 is a very fast and a very simple Davis-Putnam
procedure to solve satisfiablility problems in DIMACS
format. Satz214 adds binary and ternary resolvents
into a formule when preprocessing it. Satz214.1 is
the last version in which only up to 10*INIT_NB_CLAUSE ternary resolvents
can be added into a formule with initially
INIT_NB_CLAUSE clauses To get the source
code of Satz214.2, click here. To compile it under Unix or
Linux system, the commande line looks like: gcc satz214.1.c -O3
-o satz

** References: **

Chu Min LI, "A constrained-based approach to
narrow search trees for satisfiability",
Information processing letters 71(1999) page 75-80.

Chu Min LI & Anbulagan, "Look-ahead versus look-back for satisfiability
problems", in preceedings of third international conference on Principles
and Practice of Constraint Programming--CP97, Springer-Verlag, LNCS 1330, Page 342-356, Autriche,
1997.

Chu Min LI & Anbulagan, "Heuristics based on unit propagation for
satisfiability problems", in
proceedings of 15th International Joint Conference on Artificial Interlligence (IJCAI'97), Morgan Kaufmann Publishers, ISBN
1-55860-480-4, Page 366-371, Japon, 1997.

** ****EqSatz** (Chu Min
LI) :

EqSatz is equivalency
reasoning enhanced satz to solve satisfiability problems
involving equivalency clauses (Xor or modulo 2 arithmetics) such as 1<->2<->3 (equivalent
to four CNF clauses: -1 or -2 or 3, -1 or 2 or -3, 1 or -2 or -3, 1 or 2
or 3). EqSatz
is the first method to solve *all *the
ten DIMACS 32 bit parity par32-* instances (second
IJCAI-97 challenge on propositional reasoning and search) in reasonable
time. To get its source code click here. To compile it under Unix or Linux system, the
commande line looks like: gcc
eqsatz20.c -O3 -o eqsatz

** References:
**

Chu Min LI, "Integrating Equivalency reasoning
into Davis-Putnam procedure", in the
proceedings of AAAI-2000. Austin Texas, USA, July 2000, Page 291-296.

Chu Min LI, ``Equivalent literal propagation in
Davis-Putnam procedure'', in *Discrete Applied
Mathematics*, Vol 130/2 pp 251-276, 2003.

** Compactor **(Chu Min LI) **:**

The compactor is used to simplify an input formula in
DIMACS format. It is Satz without branching. To
get its source code, click here. Four operations are performed given an input formula:

(i)
the input formula is performed by adding resolvent of length < 4; e.g. if 1 2 3 and -1 2 4 are clauses,
add a clause 2 3 4 into the formula.

(ii)
elimination of pure literals;

(iii)
detection of failure literals ;

(iv)
rename remaining variables to be continuous;

The simplified formula is
written into the file named "out" in the
directory where the compactor is run. The old and new variables are
written into the file named "var_table" in
the directory where the compactor runs. This is a two-column file. The first
column is the old
variables in the original input formula which are replaced in the
simplified formula by the variables in
the second column.

Please don't hesitate to
contact the author for any question and any suggestion.

** ****ParaSatz**** **(Bernard Jurkowiak, Chu Min LI, Gil Utard) : ** **

ParaSatz is the
distributed/parallel version of Satz which can run on
any machines in a local network. For example, it can run on any Linux or Unix
machines in a local network. Based on sequential Satz,
ParaSatz is developed by Bernard Jurkowiak,
Chu Min Li and Gil Utard. Particular thanks to
Dominique Lazure for material help.

ParaSatz uses the simple master/slave model for communication and dynamically
balances workload among slaves, i.e. a slave cannot be idle whenever the
resolution is not finished, since the most loaded working slave is capable of
giving a part of its work to the slave which has finished its own work.

Moreover,
ParaSatz supports
fault-tolerant computing, i.e. the work of any died slave will be continued by other slaves. ParaSatz also supports partial computing, i.e. the entire
resolution can be stopped at any moment and continued later, which is
important for the so-called "global computing" using idle machines in
the world.

To get the source code of ParaSatz, click here.

**
Reference: **

Bernard Jurkowiak,
Chu Min LI, and Gil Utard, A parallelization scheme based on
work stealing for a class of SAT solvers, in
Journal of Automated Reasoning (2005) 34:73-101.