Incremental satisfiability and implication for UTVPI constraints

DOI10.1287/IJOC.1090.0369MaRDI QIDQ2899084zbMATH OpenOpenAlexFDO

Authors Andreas Schutt, Peter J. Stuckey

Publication date 28 July 2012

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

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

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)

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.

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

Cited in

(16)

• An Improved Tight Closure Algorithm for Integer Octagonal Constraints
• 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
• A certifying algorithm for lattice point feasibility in a system of UTVPI constraints
• Frontiers of Combining Systems
• A SAT-Based Decision Procedure for Mixed Logical/Integer Linear Problems
• General lower bounds and improved algorithms for infinite-domain CSPs
• 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)