I'm professor of
computer science at the University of Picardie Jules Verne. My research is
concerned with the practical resolution of NP-hard problems. I study structural
properties of
combinatorial problems and the encoding of these problems using propositional
logic (SAT), many-valued SAT or constraints (CSP).
Algorithms: The
source codes of different procedures are available below. Thanks for letting me
know all your remarks or suggestions.
Maxsatz (Chu Min Li, Felip Manya and Jordi Planes):
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.
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
the adaptive noise mechanisms: Hoos mechanism and a new adaptive noise
mechanism
based on the history of the most recent consecutive falsifications
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.
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.
Reference 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: 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
Reference:
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: 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: 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.
References:
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.
some useful links
SATLIB (a collection
of documents for SAT-based research)
CSPLib
(a problem library for constraints)
satlive
(a live site for news and discussions on SAT researches)
satex (Comparative experimentations
on complete sat solvers)
Journal on Satisfiability, Boolean
Modeling and Computation (JSAT)