SAT Competition

SAT Competition 2023 is a competitive event for solvers of the Boolean Satisfiability (SAT) problem. The competition is organized as a satellite event to the SAT Conference 2023 and continues the series of the annual SAT Competitions and SAT-Races / Challenges.

The area of SAT Solving has seen tremendous progress over the last years. Many problems that seemed to be out of reach a decade ago can now be handled routinely. Besides new algorithms and better heuristics, refined implementation techniques turned out to be vital for this success.

To keep up the driving force in improving SAT solvers, we want to motivate implementers to present their work to a broader audience and to compare it with that of others. Researchers from both academia and industry are invited to submit their solvers and benchmarks.

For further information, please visit the SAT Competition website.

MaxSAT Evaluation

The 2023 MaxSAT Evaluation (MSE 2023) is the 18th edition of MaxSAT evaluations, the primary competition-style event focusing on the evaluation of MaxSAT solvers organized yearly since 2006.

The main goals of MaxSAT Evaluation 2023 are:

  • to assess the state of the art in the field of MaxSAT solvers,
  • to collect and re-distribute a heterogeneous MaxSAT benchmark set for further scientific evaluations, and
  • to promote MaxSAT as a viable option for solving instances of a wide range of NP-hard optimization problems.

For further information, please visit the MaxSAT Evaluation website.

Model Counting Competition aims to provide a venue for researchers working on model counting such as model counting (mc), weighted model counting/sum of products (wmc), projected model counting (pmc) within the realm but not restricting to Boolean satisfiability (SAT), satisfiability modulo theories (SMT), Answer set programming (ASP), and constraint programming (CP).

It encourages to meet, communicate, and discuss the latest theoretical and practical results, in particular results on novel solvers, related solver technologies, new theoretical advances, practical academic and industrial applications as well as the linking theory and practice.

For further information, please visit the Model Counting Competition website.


The goal of the QBFGallery is to empirically assess the state of the art in QBF and DQBF olving as well as collect and select expressive benchmarks. (D)QBF researchers and users are invited to contribute their solvers, tools, and benchmarks to be used for evaluation or participate in the organization of the evaluation.

Submission of new benchmarks related to (D)QBF applications which have been shown to be hard for QBF solvers in the past are particularly welcome.

For further information, please visit the QBFGallery website.