NP Satisfiability for Arrays as Powers

2021/09/11 by Rodrigo Raya, Raya, Rodrigo, Viktor Kunčak +1
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #cs.LO

paper · pdf · doi:10.48550/arxiv.2109.05363

arxiv created 2021/09/11 · arxiv updated 2021/09/14

Abstract

We show that the satisfiability problem for the quantifier-free theory of product structures with the equicardinality relation is in NP. As an application, we extend the combinatory array logic fragment to handle cardinality constraints. The resulting fragment is independent of the base element and index set theories.

Related

• Combinatory Array Logic with Sums
• NP Decision Procedure for Monomial and Linear Integer Constraints
• Encoding and Reasoning about Arrays in Constraint Logic Programming with Sets
• Polynomial definability in constraint languages with few subpowers
• On the Combination of the Bernays-Schönfinkel-Ramsey Fragment with Simple Linear Integer Arithmetic