Integer feasibility and refutations in UTVPI constraints using bit-scaling

DOI10.1007/s00453-022-01048-1OpenAlexW4304190115MaRDI QIDQ2684489

Piotr J. Wojciechowski, K. Subramani and Vahan Mkrtchyan

Publication date: 16 February 2023

Published in: Algorithmica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00453-022-01048-1

zbMATH Keywords

UTVPI constraintsinteger feasibilityrefutationsbit-scaling

Mathematics Subject Classification ID

Analysis of algorithms (68W40) Integer programming (90C10) Nonnumerical algorithms (68W05) Combinatorics in computer science (68R05)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A combinatorial certifying algorithm for linear feasibility in UTVPI constraints
• On the complexity of cutting-plane proofs
• Weakly-relational shapes for numeric abstractions: Improved algorithms and proofs of correctness
• Optimal length resolution refutations of difference constraint systems
• The octagon abstract domain
• The intractability of resolution
• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• A certifying algorithm for lattice point feasibility in a system of UTVPI constraints
• Finding read-once resolution refutations in systems of 2CNF clauses
• On integer closure in a system of unit two variable per inequality constraints
• Feasibility checking in Horn constraint systems through a reduction based approach
• A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints
• Fourier-Motzkin elimination and its dual
• Analyzing read-once cutting plane proofs in Horn systems
• Incremental Satisfiability and Implication for UTVPI Constraints
• Outline of an algorithm for integer solutions to linear programs
• Minimum 2CNF Resolution Refutations in Polynomial Time
• Simple and Fast Algorithms for Linear and Integer Programs with Two Variables Per Inequality
• Lower bounds for cutting planes proofs with small coefficients
• 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
• Scaling Algorithms for the Shortest Paths Problem
• Optimal length tree-like resolution refutations for 2SAT formulas
• Frontiers of Combining Systems
• A Machine-Oriented Logic Based on the Resolution Principle
• Logic for Programming, Artificial Intelligence, and Reasoning

This page was built for publication: Integer feasibility and refutations in UTVPI constraints using bit-scaling