English

Implementations of two Algorithms for the Threshold Synthesis Problem

Logic in Computer Science 2023-01-11 v1

Abstract

A linear pseudo-Boolean constraint (LPB) is an expression of the form a11++ammda_1 \cdot \ell_1 + \dots + a_m \cdot \ell_m \geq d, where each i\ell_i is a literal (it assumes the value 1 or 0 depending on whether a propositional variable xix_i is true or false) and a1,,am,da_1, \dots, a_m, d are natural numbers. An LPB represents a Boolean function, and those Boolean functions that can be represented by exactly one LPB are called threshold functions. The problem of finding an LPB representation of a Boolean function if possible is called threshold recognition problem or threshold synthesis problem. The problem has an O(m7t5)O(m^7 t^5) algorithm using linear programming, where mm is the dimension and tt the number of terms in the DNF input. It has been an open question whether one can recognise threshold functions through an entirely combinatorial procedure. Smaus has developed such a procedure for doing this, which works by decomposing the DNF and "counting" the variable occurrences in it. We have implemented both algorithms as a thesis project. We report here on this experience. The most important insight was that the algorithm by Smaus is, unfortunately, incomplete.

Keywords

Cite

@article{arxiv.2301.03667,
  title  = {Implementations of two Algorithms for the Threshold Synthesis Problem},
  author = {Jan-Georg Smaus and Christian Schilling and Fabian Wenzelmann},
  journal= {arXiv preprint arXiv:2301.03667},
  year   = {2023}
}
R2 v1 2026-06-28T08:08:03.343Z