On the lengths of tree-like and dag-like cutting plane refutations of Horn constraint systems. Horn constraint systems and cutting plane refutations

DOI10.1007/s10472-022-09800-7OpenAlexW4281788412MaRDI QIDQ2095546

Yanyan Li

Publication date: 17 November 2022

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-022-09800-7

zbMATH Keywords

NP-hardnesssoundness and completenesscutting plane proofsHorn constraint systems

Mathematics Subject Classification ID

Linear programming (90C05)

Uses Software

• Yices
• z3

Cites Work

• Certifying algorithms
• On the complexity of cutting-plane proofs
• Optimal length resolution refutations of difference constraint systems
• Certifying algorithms for recognizing proper circular-arc graphs and unit circular-arc graphs
• The intractability of resolution
• Finding read-once resolution refutations in systems of 2CNF clauses
• Restricted cutting plane proofs in Horn constraint systems
• A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints
• A combinatorial algorithm for Horn programs
• Horn Clause Solvers for Program Verification
• Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories
• Outline of an algorithm for integer solutions to linear programs
• Lower bounds for cutting planes proofs with small coefficients
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Reducibility among Combinatorial Problems
• Combining Forward and Backward Abstract Interpretation of Horn Clauses
• Automated Reasoning
• Integral Extreme Points
• Program Development in Computational Logic
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item