Scholarlink

<p>In this paper, we examine decision problems and optimization problems associated with linear programming. The problems we examine deal with different forms of linear refutations. Our focus is on three different forms of refutations, namely read-once refutations, tree-like refutations, and dag-like refutations. These forms of refutations differ in how they handle the reuse of constraints. Read-once refutations do not allow for the reuse of constraints. The only exception to this condition is if the constraint can be rederived using only unused constraints. Tree-like refutations do allow for the reuse of constraints. However, each time a constraint is reused, it needs to be rederived. This rederivation affects the length of the refutation. Dag-like refutations allow for the reuse of constraints without rederivation. Linear programming is in the complexity class <b>P</b> and hence, it must have short affirmative and disqualifying certificates. One of the more celebrated lemmata in linear programming is Farkas’ lemma, which establishes that both “yes" and “no" certificates can be thought of as solutions to complementary linear programs. Since then, it has been established that if a linear program is feasible, then it must have a solution which is bounded by a polynomial function of the input size. Our goal is to study the computational complexities of determining various constrained refutations for a given infeasible linear programming instance. We establish that checking if a linear program has a read-once refutation is <b>NP-complete</b>, even when it is defined by Binary Two Variable Per Inequality (BTVPI) constraints. Furthermore, the problems of finding the <b>shortest</b> read-once, tree-like, and dag-like refutations are <b>NPO PB-complete</b>, <b>NPO-complete</b> and <b>NPO PB-complete</b> respectively. We also show that the problems of finding bounded-length tree-like and dag-like refutations are <b>NP-hard</b>, even when each constraint has at most three non-zero coefficients.</p>

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Optimal length refutations of linear programs in selected proof systems under the ADD inference rule

  • 期刊论文

  • 发表日期：

    2026年3月17日

查看全文
  • K. Subramani,
  • Piotr Wojciechowski

摘要

In this paper, we examine decision problems and optimization problems associated with linear programming. The problems we examine deal with different forms of linear refutations. Our focus is on three different forms of refutations, namely read-once refutations, tree-like refutations, and dag-like refutations. These forms of refutations differ in how they handle the reuse of constraints. Read-once refutations do not allow for the reuse of constraints. The only exception to this condition is if the constraint can be rederived using only unused constraints. Tree-like refutations do allow for the reuse of constraints. However, each time a constraint is reused, it needs to be rederived. This rederivation affects the length of the refutation. Dag-like refutations allow for the reuse of constraints without rederivation. Linear programming is in the complexity class P and hence, it must have short affirmative and disqualifying certificates. One of the more celebrated lemmata in linear programming is Farkas’ lemma, which establishes that both “yes" and “no" certificates can be thought of as solutions to complementary linear programs. Since then, it has been established that if a linear program is feasible, then it must have a solution which is bounded by a polynomial function of the input size. Our goal is to study the computational complexities of determining various constrained refutations for a given infeasible linear programming instance. We establish that checking if a linear program has a read-once refutation is NP-complete, even when it is defined by Binary Two Variable Per Inequality (BTVPI) constraints. Furthermore, the problems of finding the shortest read-once, tree-like, and dag-like refutations are NPO PB-complete, NPO-complete and NPO PB-complete respectively. We also show that the problems of finding bounded-length tree-like and dag-like refutations are NP-hard, even when each constraint has at most three non-zero coefficients.