NP satisfiability for arrays as powers

DOI10.1007/978-3-030-94583-1_15MaRDI QIDQ2152659zbMATH OpenOpenAlexFDO

Authors R. Raja, Viktor Kuncak

Publication date 8 July 2022

Full work available at URL https://arxiv.org/abs/2109.05363

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Logic in computer science (03B70)

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.

Recommendations

• Schemata of formulæ in the theory of arrays
• Cardinality constraints for arrays (decidability results and applications)
• Array Folds Logic
• Verification, Model Checking, and Abstract Interpretation
• Decision procedures for extensions of the theory of arrays

Cites work

• scientific article; zbMATH DE number 53151 (Why is no real title available?)
• A Bound on Solutions of Linear Integer Equalities and Inequalities
• Array Folds Logic
• Carathéodory bounds for integer cones
• Cardinality constraints for arrays (decidability results and applications)
• Deciding Boolean algebra with Presburger arithmetic
• Decision procedures for extensions of the theory of arrays
• Decision procedures for flat array properties
• Dominoes and the complexity of subclasses of logical theories
• On direct products of theories
• Ordered sets in the calculus of data structures
• Program verification. Fundamental issues in computer science
• The computational complexity of logical theories
• The first order properties of products of algebraic systems
• Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
• Verification, Model Checking, and Abstract Interpretation
• What Else Is Decidable about Integer Arrays?

Cited in

(4)

• Succinct ordering and aggregation constraints in algebraic array theories
• Multiple permitting and array noncomputability
• Interpolation Results for Arrays with Length and MaxDiff
• A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)

Describes a project that uses

Uses Software

• z3

This page was built for publication: NP satisfiability for arrays as powers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2152659)