Optimal length resolution refutations of difference constraint systems

DOI10.1007/s10817-009-9139-4zbMath1184.68468OpenAlexW2039657946MaRDI QIDQ846163

K. Subramani and Vahan Mkrtchyan

Publication date: 1 February 2010

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-009-9139-4

zbMATH Keywords

resolution refutationFourier-Motzkin eliminationdifference constraint systemsminimum unsatisfiable subsetoptimal length

Mathematics Subject Classification ID

Related Items (15)

Empirical analysis of algorithms for the shortest negative cost cycle problem ⋮ Exact and parameterized algorithms for read-once refutations in Horn constraint systems ⋮ A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints ⋮ Analyzing read-once cutting plane proofs in Horn systems ⋮ On the negative cost girth problem in planar networks ⋮ Randomized algorithms for finding the shortest negative cost cycle in networks ⋮ Integer feasibility and refutations in UTVPI constraints using bit-scaling ⋮ Improved algorithms for optimal length resolution refutation in difference constraint systems ⋮ 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 ⋮ On approximating optimal weight ``no-certificates in weighted difference constraint systems ⋮ 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

Uses Software

• CHIP
• Yices

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A note on two problems in connexion with graphs
• On Fourier's algorithm for linear arithmetic constraints
• The intractability of resolution
• Fourier-Motzkin elimination extension to integer programming problems
• The densest hemisphere problem
• Handbook of proof theory
• Constraint-based scheduling: Applying constraint programming to scheduling problems.
• On subclasses of minimal unsatisfiable formulas
• Time bounded random access machines
• An exponential separation between the parity principle and the pigeonhole principle
• An analysis of totally clairvoyant scheduling
• Fourier-Motzkin elimination and its dual
• The Computational Complexity of Simultaneous Diophantine Approximation Problems
• The Shifting Bottleneck Procedure for Job Shop Scheduling
• Software reliability via run-time result-checking
• Simple and Fast Algorithms for Linear and Integer Programs with Two Variables Per Inequality
• Lower bounds for resolution and cutting plane proofs and monotone computations
• On deciding the non‐emptiness of 2SAT polytopes with respect to First Order Queries
• Automated Reasoning
• Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds
• A new approach to dynamic all pairs shortest paths
• The Complexity of Propositional Proofs
• Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
• Frontiers of Combining Systems
• A Machine-Oriented Logic Based on the Resolution Principle

This page was built for publication: Optimal length resolution refutations of difference constraint systems