PySAT: a Python toolkit for prototyping with SAT oracles

Alexey Ignatiev, Antonio Morgado, Joao Marques-Silva

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

31 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationTheory and Applications of Satisfiability Testing – SAT 2018
Subtitle of host publication21st International Conference, SAT 2018 Held as Part of the Federated Logic Conference, FloC 2018 Oxford, UK, July 9–12, 2018 Proceedings
EditorsOlaf Beyersdorff, Christoph M. Wintersteiger
Place of PublicationCham Switzerland
PublisherSpringer
Pages428-437
Number of pages10
ISBN (Electronic)9783319941448
ISBN (Print)9783319941431
DOIs
Publication statusPublished - 2018
Externally publishedYes
EventInternational Conference on Theory and Applications of Satisfiability Testing 2018 - Oxford, United Kingdom
Duration: 9 Jul 201812 Jul 2018
Conference number: 21st
http://sat2018.azurewebsites.net/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume10929
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Conference on Theory and Applications of Satisfiability Testing 2018
Abbreviated titleSAT 2018
CountryUnited Kingdom
CityOxford
Period9/07/1812/07/18
Internet address

Cite this