Circuit Satisfiability and Constraint Satisfaction around Skolem Arithmetic

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

Abstract

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.

Citation

Glaßer, C., Jonsson, P., & Martin, B. (2017). Circuit Satisfiability and Constraint Satisfaction around Skolem Arithmetic. Theoretical Computer Science, 703, 18-36. https://doi.org/10.1016/j.tcs.2017.08.025

• 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
• DOI: https://doi.org/10.1016/j.tcs.2017.08.025
• Public URL: https://durham-repository.worktribe.com/output/1345411