💻 High-Performance Solvers for NP-Hard Problems

Introduction

Welcome to the official repository for the solvers developed by Prof. Chu-Min Li and his research team at the University of Picardie Jules Verne.

My research focuses on the practical, state-of-the-art resolution of NP-hard problems, including core areas such as SAT, CSP, MaxSAT, MinSAT, MaxClique, and Graph Coloring (GCP).

Proven Excellence and Pioneering Work

Our commitment to innovation is validated by a strong track record of competition success. Notably, in 2025, my team and I achieved a major breakthrough by winning the SAT Competition with a significant margin using an LLM-enhanced SAT solver. This marks the first time a solver improved by Large Language Models has won a major SAT competition, establishing a new frontier in formal Generative AI.

As the first or corresponding author of these solvers, I am the chief architect and implemented a substantial part of their core code, ensuring mastery of every technical and algorithmic detail.

Feel free to contact me directly with any questions: chu-min.li@u-picardie.fr.

Organization of This Page

This page is designed for quick access to our most impactful tools and is organized as follows:

1. Recent Championship Solvers (2017–Present): Focusing on SAT and MaxSAT solvers that have secured medals in recent SAT Competitions and MaxSAT Evaluations.
2. MaxClique Solvers: A collection of highly efficient MaxClique solvers that have significantly advanced the limits of exact solving for this problem.
3. Foundational Solvers: Earlier solvers covering SAT, MaxSAT, MinSAT, MaxClique, and Graph Coloring, which established the basis of our current research.

Note on Authorship: The names of my students (Master, PhD, or Post-doc) are underlined in the corresponding solver references, highlighting their essential contributions to the work.

For a comprehensive view of my published work, please consult my DBLP or Google Scholar page.

Technical Note on Downloads

The source code for each solver is available under the MIT License. To download the code, please use the provided link (the solver name or the word "here").

• Firefox or Safari Users: A single click should initiate the download.
• Chrome or Chromium-based Users (released after 2018): You may need to right-click on the link, select "Save link as...", and then click "Save" in your recent download history.

Solvers for SAT since 2017:

These solvers won frequently medals in SAT competitions, including 5 gold medals (AE-Kissat2025-MAB in the main track and the SAT track in 2025, Kissat-MAB-ESA in the Anniversary track in 2022, Kissat-MAB-Hywalk in the main track in 2022, Maple_LCM in the main track in 2017), 1 silver medal (Kissat-MaB-ESA in the UNSAT subtrack of the anniversary track) and 2 bronze medals (AE-Kissat-bump in the UNSAT track in 2025, Maple_CM in the main track in 2018).

Ø  AE-Kissat2025-MAB : It is improved on top of Kissat_MAB using LLMs and won the gold medal of the main track of the SAT competition 2025 with a wide margin. This is the first time that a solver improved using LLMs wins a SAT competition. It also won the gold medal of the SAT track of the 2025 competition with an even wider margin. Its source code is available at the SAT competition web page, or here.

Ø  AE-Kissat-bump: It is improved on top of Kissat-bump using LLMs and won the bronze medal of the UNSAT track of the 2025 SAT competition. Its source code is available at the SAT competition web page, or here.

Reference for AE-Kissat2025-MAB and AE-Kissat-bump:

Hang Ding, Mao Luo, Chu-Min Li, Shunwei Li, Runyao Chen, Caiquan Xiong and Xinyun Wu : A Self-Optimizing Framework for SAT Solvers via Population Evolution and Large Language Model Collaboration. In Proceedings of SAT Competition 2025: Solver and Benchmark Descriptions, pages 15-17.

Ø  Kissat-MAB-ESA: It is developed on top of Kissat-MAB using a new variable ordering to eliminate variables in SAT instances. It won the Gold Medal in the anniversary track of SAT competition 2022 (Kissat_MAB_ESA) summarizing the last 20 competitions since the event's creation. It also won the silver medal of the UNSAT subtrack in this anniversary track. Its source code is available at the SAT competition web page, or here.

Reference:

Shuolin Li, Chu-Min Li, Mao Luo, Jordi Coll, Djamal Habet, Felip Manyà: A New Variable Ordering for In-processing Bounded Variable Elimination in SAT Solvers. In proceedings of IJCAI 2023: 1979-1987

Ø  Kissat-MAB-hywalk: It won the gold medal of the main track of the 2022 SAT competition. Its source code is available at the SAT competition web page, or here.

Reference:

Jiongzhi Zheng, Kun He, Zhuo Chen, Jianrong Zhou, and Chu-Min Li: Combining Hybrid Walking Strategy with Kissat_MAB, CaDiCaL, and LStech-Maple. In proceedings of SAT competition 2022 : Solver and Benchmark Descriptions, pages 20-21

Ø  Maple_CM : it won the bronze medal of the main track of the SAT competition 2018. 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 MaxSAT since 2021

Ø  MaxCDCL: a MaxSAT solver combining branch-and-bound and clause learning. It won the Exact Weighted Track in 2023 and the Exact Unweighted Track in 2024. 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, best paper award.

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

 

Earlier SAT solvers

The earlier SAT solvers I designed and developed before 2017 as the first or corresponding author also won frequently medals in SAT competitions: 1 gold medal (TNM in 2009), 5 silvers medals (G2WSAT in 2005, adaptg2wsat0 in 2007, Sattime in 2011, Sattime in 2013, BalancesZ in 2014), and 3 bronze medals (adaptg2wsat+ in 2007, adaptg2wsat2009++ in 2009, and SGSeq in 2014). See https://satcompetition.github.io/ and also details below.

Ø  TNM : 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 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.

 

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.

 

Ø  BalancedZ: A local search algorithm balancing intensification and diversification that won a silver medal in the 2014 SAT competition. Its source code is available here.

 

Reference:

 

Chu-Min Li, Chong Huang, and Ruchu Xu : Balance between intensification and diversification: two sides of the same coin. In proceedings of SAT competition 2014 : Solver and Benchmark Description, 2014, pages 10-11.

 

Ø  Sattime: 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 won a silver medal in the 2011 SAT competition and a silver medal in the 2013 SAT competition. 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.

      

Ø  Adaptg2wsat2009++ : 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: 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+ : 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: 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

Ø  SGSeq: It is a portfolio that runs our local search solver Sattime and a CDCL solver called Glucose to solve a SAT instance. It won a bronze medal in the 2014 SAT competition.

 

References: Chu-Min Li, Hua Jiang, and Ru Chu Xu, Description of SattimeGlucoseSeq. In proceedings of SAT competition 2014 : Solver and Benchmark Description, 2014, pages 76-76.

 

Ø  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

 

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

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.

 

Earlier MaxSAT solver

The earlier MaxSAT solver MaxSatz and its variants I developed as the first or corresponding author dominated MaxSAT Evaluations for several years since 2006.

Ø  Maxsatz: 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 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.

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.

Chu-Min Li, Zhe Quan, 2010, An efficient 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.