A reduction from unbounded linear mixed arithmetic problems into bounded problems

DOI10.1007/978-3-319-94205-6_22OpenAlexW4298890824MaRDI QIDQ1799094

Martin Bromberger

Publication date: 18 October 2018

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

zbMATH Keywords

linear arithmeticlinear transformationsconstraint solvinginteger arithmeticSMTmixed arithmetic

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (1)

SPASS-SATT. A CDCL(LA) solver

Uses Software

• z3
• SMTInterpol
• CVC4
• MathSAT5

This page was built for publication: A reduction from unbounded linear mixed arithmetic problems into bounded problems