The main research achievements of the laboratory, including various constraint satisfaction problem solvers and operations research optimization solvers, are all released as open-source. For detailed introductions and user manuals of the solvers and software tools, please refer to the relevant source code repositories or project homepages.

SAT Solvers

Name Introduction
X-SAT Optimized SAT solver for circuits
PRS Parallel SAT solver framework
PRS-distributed Distributed SAT solver
Relaxed Hybrid algorithm SAT solver
CCAnr + CP3 Local search SAT solver based on configuration checking and preprocessor
WalkSAT/SKC (implementation of Cai) Efficient implementation of the local search SAT solver WalkSAT

SMT Solvers

Name Introduction
AriParti Parallel SMT variable-level partitioning solver
Parti-Z3++ Distributed SMT variable-level partitioning solver
Z3++ Derived solver based on Z3, deeply integrating local search algorithms and complete algorithms
hybridSMT Hybrid algorithm SMT solver

Operations Research & Optimization Solvers

Name Introduction
Local-MIP Efficient local search solver for Mixed Integer Programming (MIP); the related paper won the Best Paper Award at CP 2024
ParaILP Parallel local search solver for Integer Linear Programming (ILP), deeply integrating local search and evolutionary algorithms; related paper was accepted at IJCAI 2024
PairLS Local search solver for MaxSMT, proposing a compensation operator; the related paper was accepted at FM 2024
LS-IMP Local search solver for Multiple Integer Linear Programming; the related paper was accepted at KDD 2024

MaxSAT/PBO Solvers

Name Introduction
NuWLS MaxSAT local search solver, used in the champion solver of the incomplete track in the 2022 International MaxSAT Competition
USW-LS MaxSAT local search solver, used in the champion solver of the incomplete track in the 2023 International MaxSAT Competition
NuPBO Pseudo-Boolean Optimization (PBO) local search solver, used in the solvers ranked first and second in the DEC-LIN track of the 2024 International PB Competition

EDA & Formal Verification Tools

Name Introduction
hybridCEC Combinational Equivalence Checking verifier
modelchecker modelchecking & verification