Recently, Strength-based Argumentation Frameworks (StrAFs) have been proposed
to model situations where some quantitative strength is associated with
arguments. In this setting, the notion of accrual corresponds to sets of
arguments that collectively attack an argument. Some semantics have already
been defined, which are sensitive to the existence of accruals that
collectively defeat their target, while their individual elements cannot.
However, until now, only the surface of this framework and semantics have been
studied. Indeed, the existing literature focuses on the adaptation of the
stable semantics to StrAFs. In this paper, we push forward the study and
investigate the adaptation of admissibility-based semantics. Especially, we
show that the strong admissibility defined in the literature does not satisfy a
desirable property, namely Dung's fundamental lemma. We therefore propose an
alternative definition that induces semantics that behave as expected. We then
study computational issues for these new semantics, in particular we show that
complexity of reasoning is similar to the complexity of the corresponding
decision problems for standard argumentation frameworks in almost all cases. We
then propose a translation in pseudo-Boolean constraints for computing (strong
and weak) extensions. We conclude with an experimental evaluation of our
approach which shows in particular that it scales up well for solving the
problem of providing one extension as well as enumerating them all.

本文致力于研究基于强度的论证框架中附加性的新义和双扩展的计算方法，提出了基于伪布尔约束的新的求解方法，并进行模拟实验，证明了该方法可行且可扩展。

基于强度论证的可容许性：复杂性与算法（带证明的扩展版本）

Admissibility in Strength-based Argumentation: Complexity and Algorithms (Extended Version with Proofs)

Learning pseudo-Boolean (PB) constraints in PB solvers exploiting cutting
planes based inference is not as well understood as clause learning in
conflict-driven clause learning solvers. In this paper, we show that PB
constraints derived using cutting planes may contain \emph{irrelevant
literals}, i.e., literals whose assigned values (whatever they are) never
change the truth value of the constraint. Such literals may lead to infer
constraints that are weaker than they should be, impacting the size of the
proof built by the solver, and thus also affecting its performance. This
suggests that current implementations of PB solvers based on cutting planes
should be reconsidered to prevent the generation of irrelevant literals.
Indeed, detecting and removing irrelevant literals is too expensive in practice
to be considered as an option (the associated problem is NP-hard.

本文研究了基于切割平面推理的 PB 求解器中的 PB 约束的学习问题，并揭示了使用切割平面推理导出的 PB 约束可能包含对约束的真值没有影响的文字，这些文字可能导致推出的约束比应该推出的约束要弱，从而影响求解器的证明长度和性能。因此建议在当前的基于切割平面推理的 PB 求解器实现中，应该重新考虑如何防止产生无关的文字。

关于伪布尔约束学习中无关文本的处理

On Irrelevant Literals in Pseudo-Boolean Constraint Learning

Pseudo-Boolean constraints, also known as 0-1 Integer Linear Constraints, are
used to model many real-world problems. A common approach to solve these
constraints is to encode them into a SAT formula. The runtime of the SAT solver
on such formula is sensitive to the manner in which the given pseudo-Boolean
constraints are encoded. In this paper, we propose generalized Totalizer
encoding (GTE), which is an arc-consistency preserving extension of the
Totalizer encoding to pseudo-Boolean constraints. Unlike some other encodings,
the number of auxiliary variables required for GTE does not depend on the
magnitudes of the coefficients. Instead, it depends on the number of distinct
combinations of these coefficients. We show the superiority of GTE with respect
to other encodings when large pseudo-Boolean constraints have low number of
distinct coefficients. Our experimental results also show that GTE remains
competitive even when the pseudo-Boolean constraints do not have this
characteristic.

提出了一种基于总和器编码的伪布尔约束通用编码方法（GTE），该方法不依赖系数的数量，且在大伪布尔约束中表现优越，同时在无此特征的约束下也具有竞争力。

伪布尔约束的广义总计数器编码

Generalized Totalizer Encoding for Pseudo-Boolean Constraints

Pseudo-Boolean constraints are omnipresent in practical applications, and
thus a significant effort has been devoted to the development of good SAT
encoding techniques for them. Some of these encodings first construct a Binary
Decision Diagram (BDD) for the constraint, and then encode the BDD into a
propositional formula. These BDD-based approaches have some important
advantages, such as not being dependent on the size of the coefficients, or
being able to share the same BDD for representing many constraints.
We first focus on the size of the resulting BDDs, which was considered to be
an open problem in our research community. We report on previous work where it
was proved that there are Pseudo-Boolean constraints for which no polynomial
BDD exists. We also give an alternative and simpler proof assuming that NP is
different from Co-NP. More interestingly, here we also show how to overcome the
possible exponential blowup of BDDs by phcoefficient decomposition. This allows
us to give the first polynomial generalized arc-consistent ROBDD-based encoding
for Pseudo-Boolean constraints.
Finally, we focus on practical issues: we show how to efficiently construct
such ROBDDs, how to encode them into SAT with only 2 clauses per node, and
present experimental results that confirm that our approach is competitive with
other encodings and state-of-the-art Pseudo-Boolean solvers.

该研究论文主要研究了基于二元决策图的 Pseudo-Boolean 约束编码技术，提出了使用系数分解方法克服爆炸性增长问题，并给出了第一个多项式广义弧一致的 ROBDD 编码算法。