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-7MaRDI QIDQ2095546zbMATH OpenOpenAlexFDO

Authors 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

cutting plane proofsHorn constraint systemsNP-hardnesssoundness and completeness

Mathematics Subject Classification ID

Linear programming (90C05)

Recommendations

• Restricted cutting plane proofs in Horn constraint systems
• On the complexity of cutting-plane proofs
• Input Proofs and Rank One Cutting Planes
• Cutting planes, connectivity, and threshold logic
• Cutting planes and the parameter cutwidth

Cites work

• A combinatorial algorithm for Horn programs
• A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints
• Automated Reasoning
• Certifying algorithms
• Certifying algorithms for recognizing proper circular-arc graphs and unit circular-arc graphs
• Combining forward and backward abstract interpretation of Horn clauses
• Computing small unsatisfiable cores in satisfiability modulo theories
• Finding read-once resolution refutations in systems of 2CNF clauses
• Horn clause solvers for program verification
• scientific article; zbMATH DE number 6020480 (Why is no real title available?)
• scientific article; zbMATH DE number 1222561 (Why is no real title available?)
• scientific article; zbMATH DE number 1158761 (Why is no real title available?)
• scientific article; zbMATH DE number 2079335 (Why is no real title available?)
• scientific article; zbMATH DE number 1765669 (Why is no real title available?)
• scientific article; zbMATH DE number 2090312 (Why is no real title available?)
• scientific article; zbMATH DE number 1416629 (Why is no real title available?)
• scientific article; zbMATH DE number 7650340 (Why is no real title available?)
• Integral Extreme Points
• Lower bounds for cutting planes proofs with small coefficients
• Lower bounds for resolution and cutting plane proofs and monotone computations
• On the complexity of cutting-plane proofs
• Optimal length resolution refutations of difference constraint systems
• Outline of an algorithm for integer solutions to linear programs
• Program Development in Computational Logic
• Reducibility among combinatorial problems
• Restricted cutting plane proofs in Horn constraint systems
• The intractability of resolution

Cited in

(3)

• Exact and parameterized algorithms for read-once refutations in Horn constraint systems
• Restricted cutting plane proofs in Horn constraint systems
• Analyzing read-once cutting plane proofs in Horn systems

Describes a project that uses

Uses Software

• Yices
• z3

This page was built for publication: On the lengths of tree-like and dag-like cutting plane refutations of Horn constraint systems. Horn constraint systems and cutting plane refutations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2095546)