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.

**We
developed solvers for SAT, MaxSAT, MinSAT, MaxClique and Graph Coloring. Their
source codes are available below under the MIT Licence. Thanks for letting me
know all your remarks or suggestions.**

**New: MaxCDCL1.2,**** a MaxSAT solver
combining branch-and-bound and clause learning, implemented by Chu-Min Li based
on Maple_LCM with the help of Jordi Coll. Its source code is available here.**

**Reference:
**Chu-Min Li, Zhenxing Xu, Jordi Coll, Felip Manyà,
Djamal Habet, Kun He,** **Combining Clause Learning and Branch and
Bound for MaxSAT. CP-2021: 38:1-38:18, *prix du meilleur papier*.

**Solvers
for SAT:**

Ø **Maple_CM : it won the bronze medal of the
main track ****of the SAT competition
2017. ****Its
source code, as well as the detailed results, is available in the sat competition web page, or here.**

**Reference: **

Chu-Min Li, Fan
Xiao, Mao Luo, Felip Manyà, Zhipeng Lü, Yu Li, Clause vivification by unit
propagation in CDCL SAT solvers, Artificial
Intelligence, volume 279, February 2020, 103197, 23 pages,
https://doi.org/10.1016/j.artint.2019.103197

Ø **Maple_LCM_Dist and Maple_LCM (Maple+ in the
set): they won the main track of the SAT competition 2017 (see ****the sat competition web page**)**. **The source codes of
these solvers (for Mac OS and Linux, respectively) are available here.

**Reference: **

Mao Luo, Chu-Min Li, Fan Xiao,
Felip Many, Zhipeng Lu, An
Effective Learnt Clause Minimization Approach for CDCL SAT Solvers, In
Proceedings of the Twenty-Sixth International Joint Conference on Artificial
Intelligence (IJCAI-17), 2017, Melbourne, Pages 703-711.

**Solvers for ****the
Maximum Weight Clique Problem (weighted MaxClique):**

Ø **TSM-MWC: **it is an exact
(BnB) solver highly effective for small, medium and massive graphs, with or
without very different vertex weight. It is the first exact algorithm that
reaches the best performance in both small/medium and massive real-world
graphs. Its source code is available here.

**Reference:**

Hua
Jiang, Chu-Min
Li, Yanli
Liu, Felip Manya, A
Two-Stage MaxSAT Reasoning Approach for the Maximum Weight Clique Problem,
in proceedings of The
Thirty-Second AAAI Conference on Artificial Intelligence (AAAI-18), pages 1338-1346.

Ø
**WLMC: **it is
the first exact solver that finds better solutions than heuristic solvers in
shorter time in large graphs, even when including the time needed for proving
the optimality of its solutions, *refuting
**the prevailing
hypothesis that exact MaxClique algorithms, despite proving optimality, are
less adequate for large graphs than heuristic algorithms. *A new release (Release 2017) of the solver (wlmc2)
able to handle very large vertex weights 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.

**Solvers for ****the
Maximum Clique Problem (non-Weighted MaxClique):**

Ø **LMC****: **A very efficient exact (BnB) solver for the maximum clique problem in
large graphs. It combines efficient preprocessing to eliminate vertices that cannot
belong to a maximum clique and incremental MaxSAT reasoning to prune branches
that cannot lead to a maximum clique. The source code of
the algorithm is available here.

**Reference:**

Hua Jiang, Chu-Min Li, Felip Manya, Combining
efficient preprocessing and incremental MaxSAT reasoning for MaxClique in large
graphs. In Proceedings of 22nd European Conference On Artifical
Intelligence (ECAI-2016), pages 939-947, 2016.

Ø **MoMC, SoMC, DoMC: **three efficient exact (BnB)
solvers for the maximum clique problem SoMC (Static ordering MaxClique Solver)
and DoMC (Dynamic ordering MaxClique Solver) correspond to SoMC2 and DoMC2
described in the paper below. The paper presents also MoMC (Mixed ordering
MaxClique Solver), which switches cleverly between the static and the dynamic
vertex orderings and achieves better performance than SoMC and DoMC in general
for solving MaxClique. The
source code of the algorithms is available here.

**Reference:**

Chu-Min Li, Hua Jiang, Felip Manya, On
Minimization of the Number of Branches in Branch-and-Bound Algorithms for the
Maximum Clique Problem, Computers & Operations Research 84 (2017): 1-15

Compile for obtaining SoMC, DoMC and MoMC,
respectively, from the same source:

gcc
MoMC2016.c -O3 -DSOMC –o SoMC

gcc
MoMC2016.c -O3 -DDOMC –o DoMC

gcc
MoMC2016.c -O3 -DMOMC -o MoMC

for
finding a maximum clique, run ./MoMC inputGraphInDimacsFormat

for
listing all maximum cliques

./MoMC
instance -a n (where n is the max number of cliques to be printed)

Ø **IncMC2:**** **it uses similar technology to SoMC and is better than SoMC. When solving
MaxClique using a BnB procedure, a prevailing hypothesis is that the larger the
initial (incumbent) clique, the easier the search, because it is believed that
larger incumbent would allow to prune more search space. *However,
the performance of IncMC2 refutes this hypothesis*, as showed in the paper
below. Indeed, IncMC2 solves (i.e., finds and proves an optimal solution of)
certain instances more quickly from scratch than from an optimal initial clique
size, thanks to incremental upper bound.

The source of
IncMC2 is available here.

Use

./IncMC2 graphFile

to solve the graph from scratch.

Use

./IncMC2 graphFile –i lb

to find a clique larger than lb, where lb is a positive integer. When lb
is the optimal solution size, this command proves the optimality of lb.

**Reference:**

Chu-Min Li, Zhiwen Fang, Hua Jiang, Ke Xu, Incremental
Upper Bound for the Maximum Clique Problem, INFORMS Journal on
Computing, 2018, vol. 30, no. 1, pp. 137–153

**Other solvers:**

**Color6:
A Complete (Exact) Algorithm for Graph k-Coloring**

This algorithm solves efficiently the k-coloring problem by telling how
to color the vertices of a graph with k- colors if this is possible or proving
the graph cannot be colored with k colors. The source code of color6 is available here.

Compiling: gcc color6.c –O3 –o color6

Running: ./color6 inputGraphInDIMACSformat –nbColors k

**Reference:**

Zhaoyang Zhou, Chu-Min Li, Chong
Huang, Ruchu Xu. An
exact algorithm with learning for the graph coloring problem. Computers
& Operations Research, 51(2014) pp 282-301.

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