Skip to main content

Research Repository

Advanced Search

Circuit Satisfiability and Constraint Satisfaction around Skolem Arithmetic

Glaßer, Christian; Jonsson, Peter; Martin, Barnaby

Circuit Satisfiability and Constraint Satisfaction around Skolem Arithmetic Thumbnail


Christian Glaßer

Peter Jonsson


We study interactions between Skolem Arithmetic and certain classes of Circuit Satisfiability and Constraint Satisfaction Problems (CSPs). We revisit results of Glaßer et al. [1] in the context of CSPs and settle the major open question from that paper, finding a certain satisfiability problem on circuits—involving complement, intersection, union and multiplication—to be decidable. This we prove using the decidability of Skolem Arithmetic. Then we solve a second question left open in [1] by proving a tight upper bound for the similar circuit satisfiability problem involving just intersection, union and multiplication. We continue by studying first-order expansions of Skolem Arithmetic without constants, (N;×), as CSPs. We find already here a rich landscape of problems with non-trivial instances that are in P as well as those that are NP-complete.

Journal Article Type Article
Acceptance Date Aug 31, 2017
Online Publication Date Sep 6, 2017
Publication Date Dec 5, 2017
Deposit Date Sep 8, 2017
Publicly Available Date Sep 6, 2018
Journal Theoretical Computer Science
Print ISSN 0304-3975
Publisher Elsevier
Peer Reviewed Peer Reviewed
Volume 703
Pages 18-36
Public URL


You might also like

Downloadable Citations