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 procedures are available
below. Thanks for letting me
know all your remarks or suggestions.**

**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.

__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.

__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.

**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.