A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints

DOI10.1007/s00453-019-00554-zzbMath1421.68181OpenAlexW2919232531MaRDI QIDQ2415363

Piotr Wojciechowki, K. Subramani and Vahan Mkrtchyan

Publication date: 21 May 2019

Published in: Algorithmica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00453-019-00554-z

zbMATH Keywords

NP-hardUTVPI constraintsdifference constraintsread-once refutationliteral-once refutation

Mathematics Subject Classification ID

Analysis of algorithms (68W40) Nonnumerical algorithms (68W05) Linear programming (90C05) Combinatorial optimization (90C27) Edge subsets with special properties (factorization, matching, partitioning, covering and packing, etc.) (05C70) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (13)

Exact and parameterized algorithms for read-once refutations in Horn constraint systems ⋮ Analyzing read-once cutting plane proofs in Horn systems ⋮ Reachability in choice networks ⋮ On the parallel complexity of constrained read-once refutations in UTVPI constraint systems ⋮ Integer feasibility and refutations in UTVPI constraints using bit-scaling ⋮ Unit read-once refutations for systems of difference constraints ⋮ Tree-like unit refutations in Horn constraint systems ⋮ Polynomial time algorithms for optimal length tree-like refutations of linear infeasibility in UTVPI constraints ⋮ Copy complexity of Horn formulas with respect to unit read-once resolution ⋮ On integer closure in a system of unit two variable per inequality constraints ⋮ On the parametrized complexity of Read-once refutations in UTVPI+ constraint systems ⋮ Analyzing unit read-once refutations in difference constraint systems ⋮ On the lengths of tree-like and dag-like cutting plane refutations of Horn constraint systems. Horn constraint systems and cutting plane refutations

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A combinatorial certifying algorithm for linear feasibility in UTVPI constraints
• Optimal length resolution refutations of difference constraint systems
• The octagon abstract domain
• The intractability of resolution
• The directed subgraph homeomorphism problem
• The complexity of read-once resolution
• Finding read-once resolution refutations in systems of 2CNF clauses
• Improved algorithms for optimal length resolution refutation in difference constraint systems
• An Efficient Implementation of Edmonds' Algorithm for Maximum Matching on Graphs
• Simple and Fast Algorithms for Linear and Integer Programs with Two Variables Per Inequality
• Parametric dispatching of hard real-time tasks
• Scaling Algorithms for Weighted Matching in General Graphs
• The Complexity of Propositional Proofs
• Frontiers of Combining Systems
• Combinatorial optimization. Theory and algorithms.

This page was built for publication: A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints