Pysat: SAT technology in Python.
Copyright © 2018-2021 Alexey Ignatiev, Joao Marques-Silva, Antonio Morgado, is licensed under MIT.

PySAT is a Python (2.7, 3.4+) toolkit, which aims at providing a simple and unified interface to a number of state-of-art Boolean satisfiability (SAT) solvers as well as to a variety of cardinality and pseudo-Boolean encodings.

The purpose of PySAT is to enable researchers working on SAT and its applications and generalizations to easily prototype with SAT oracles in Python while exploiting incrementally the power of the original low-level implementations of modern SAT solvers.

Mathematical Insights into Algorithms for Optimization (MIAO).
Department of Computer Science University of Copenhagen and Department of Computer Science University of Lund.

The MIAO research group are conducting deeply theoretical, mathematical research on the foundations of efficient computations, and on the other hand working on the design of state-of-the-art applied algorithms that are meant to run blisteringly fast in practice.

Much of the activities of the group revolve around powerful algorithmic paradigms such as, e.g., Boolean satisfiability (SAT)solving, Gröbner basis computations, integer linear programming, constraint programming, and semidefinite programming.

Varp: A propositional logic library.
‍Copyright © 2021 Tony Rogvall, is licensed under MIT.

Varp is a language and toolset for stating and manipulating propositional logic formulas augmented  with finite domain and cardinality quantifiers, and some finite binary arithmetics. Varp also contains a Python library with low level constructs used in SAT solving algorithms.