PySAT: A Python toolkit for prototyping with SAT oracles. (English) Zbl 06916321

Ignatiev, Alexey; Morgado, Antonio; Marques-Silva, Joao

Beyersdorff, Olaf (ed.) et al., Theory and applications of satisfiability testing – SAT 2018. 21st international conference, SAT 2018, held as part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9–12, 2018. Proceedings. Cham: Springer (ISBN 978-3-319-94143-1/pbk; 978-3-319-94144-8/ebook). Lecture Notes in Computer Science 10929, 428-437 (2018).

Summary: Boolean satisfiability (SAT) solvers are at the core of efficient approaches for solving a vast multitude of practical problems. Moreover, albeit targeting an NP-complete problem, SAT solvers are increasingly used for tackling problems beyond NP. Despite the success of SAT in practice, modeling with SAT and more importantly implementing SAT-based problem solving solutions is often a difficult and error-prone task. This paper proposes the PySAT toolkit, which enables fast Python-based prototyping using SAT oracles and SAT-related technology. PySAT provides a simple API for working with a few state-of-the-art SAT oracles and also integrates a number of cardinality constraint encodings, all aiming at simplifying the prototyping process. Experimental results presented in the paper show that PySAT-based implementations can be as efficient as those written in a low-level language.
For the entire collection see [Zbl 1390.68015].

MSC:

68Q25	Analysis of algorithms and problem complexity
68T20	Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Software:

CPLEX; CryptoMiniSat; Glucose; Graphviz; Gurobi; Matplotlib; MiFuMax; MiniSat; NetworkX; NumPy; pandas; PBLib; Plingeling; pylgl; PyMiniSolvers; PyPI; PySAT; Python; PyTorch; SATisPy; Scikit; SciPy