Circuit Satisfiability and Constraint Satisfaction Around Skolem Arithmetic
Theoretical Computer Science(2017)
摘要
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. [16] 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 [16] 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, \((\mathbb {N};\times )\), 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.
更多查看译文
关键词
Skolem Arithmetic,Circuit Satisfiability,Constraint Satisfaction Problem (CSPs),Presburger Arithmetic,Related CSPs
AI 理解论文
溯源树
样例
![](https://originalfileserver.aminer.cn/sys/aminer/pubs/mrt_preview.jpeg)
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要