Incremental satisfiability and implication for UTVPI constraints

DOI10.1287/IJOC.1090.0369zbMATH Open1243.90141arXiv0709.2961OpenAlexW2113188188MaRDI QIDQ2899084FDOQ2899084

Authors: Andreas Schutt, Peter J. Stuckey 

Publication date: 28 July 2012

Published in: INFORMS Journal on Computing (Search for Journal in Brave)

Abstract: Unit two-variable-per-inequality (UTVPI) constraints form one of the largest class of integer constraints which are polynomial time solvable (unless P=NP). There is considerable interest in their use for constraint solving, abstract interpretation, spatial databases, and theorem proving. In this paper we develop a new incremental algorithm for UTVPI constraint satisfaction and implication checking that requires O(m + n log n + p) time and O(n+m+p) space to incrementally check satisfiability of m UTVPI constraints on n variables and check implication of p UTVPI constraints.

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

Recommendations

• On solving Boolean combinations of UTVPI constraints.
• Frontiers of Combining Systems
• Integer feasibility and refutations in UTVPI constraints using bit-scaling
• A Bit-Scaling Algorithm for Integer Feasibility in UTVPI Constraints
• An Optimal Algorithm for Computing the Integer Closure of UTVPI Constraints

zbMATH Keywords

satisfactionimplicationtwo-variable-per-inequality constraints

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Analysis of algorithms (68W40) Integer programming (90C10)

Cited In (16)

• Incremental closure for systems of two variables per inequality
• Incrementally closing octagons
• A Graphical Theorem of the Alternative for UTVPI Constraints
• On integer closure in a system of unit two variable per inequality constraints
• On solving Boolean combinations of UTVPI constraints.
• A Bit-Scaling Algorithm for Integer Feasibility in UTVPI Constraints
• On the parametrized complexity of read-once refutations in UTVPI+ constraint systems
• Trichotomy for integer linear systems based on their sign patterns
• Integer feasibility and refutations in UTVPI constraints using bit-scaling
• Pure Nash equilibria in graphical games and treewidth
• Frontiers of Combining Systems
• A certifying algorithm for lattice point feasibility in a system of UTVPI constraints
• A SAT-Based Decision Procedure for Mixed Logical/Integer Linear Problems
• General lower bounds and improved algorithms for infinite-domain CSPs
• An Improved Tight Closure Algorithm for Integer Octagonal Constraints
• A combinatorial certifying algorithm for linear feasibility in UTVPI constraints

This page was built for publication: Incremental satisfiability and implication for UTVPI constraints

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