Circuit satisfiability and constraint satisfaction around Skolem Arithmetic

Funding Agencies|EPSRC [EP/L005654/1]; Swedish Research Council (VR) [621-2012-3239]
We study interactions between Skolem Arithmetic and certain classes of Circuit Satisfiability and Constraint Satisfaction Problems (CSPs). We revisit results of Glasser 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; x), 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. (C) 2017 Elsevier B.V. All rights reserved.

NATURVETENSKAP Matematik Diskret matematik hsv//swe
NATURAL SCIENCES Mathematics Discrete Mathematics hsv//eng
Circuit satisfiability; Constraint satisfaction; Skolem Arithmetic; Computational complexity

Jonsson, PeterLinköpings universitet,Programvara och system,Tekniska fakulteten(Swepub:liu)petjo00 (författare)
Martin, BarnabyUniversity of Durham, England (författare)
Julius Maximilian University, GermanyProgramvara och system (creator_code:org_t)

Ingår i:Theoretical Computer Science: ELSEVIER SCIENCE BV703, s. 18-360304-39751879-2294

Av författaren/redakt...: Glasser, Christi ...; Jonsson, Peter; Martin, Barnaby

Om ämnet

Kungliga biblioteket hanterar dina personuppgifter i enlighet med EU:s dataskyddsförordning (2018), GDPR. Läs mer om hur det funkar här.
Så här hanterar KB dina uppgifter vid användning av denna tjänst.