Plans regarding boolean threshold functions.
More...
Go to the source code of this file.
Detailed Description
Plans regarding boolean threshold functions.
 Todo:
 General threshold functions

With [Knuth, Vol. 4, Fascicle 0, Section 7.1.1] we consider the threshold functions f(x_1, ..., x_n) = 1 iff w_1 * x_1 + ... + w_n * x_n >= t for integer constants w_i.

As constraints, these conditions are also known as "pseudoboolean
constraints".

Since we are interested for example in CNF and DNFrepresentations, we also consider the negations, which (essentially) can be represented by allowing "<=" instead of ">=". How to call them? The above as "upper" threshold functions, while these as "lower" threshold functions?

Naming: threshold_bf(W), lthreshold_bf(W).

However, likely the CNF/DNFrepresentations should be handled in module PseudoBoolean; see Satisfiability/Lisp/PseudoBoolean/plans/general.hpp.
 Todo:
 Cardinality constraints

Important special cases of threshold functions are obtained when using w_i = 1 for all i.

So the conditions are x_1 + ... + x_n >= t resp. <= t.

Naming: cardinality_bf(n,t) resp. lcardinality_bf(n,t).

For the special case t=1 we use alo_bf(n) resp. amo_bf(n).

Clauseset realisations are considered in Satisfiability/Lisp/PseudoBoolean/plans/CardinalityConstraints.hpp.

The condition x_1 + ... + x_n = t is expressed by ecardinality_bf(n,t). See "The basic symmetric functions" below.
 Todo:
 The basic symmetric functions

The functions ecardinality_bf(n,t) run under different names:

E_t in [Wegener 87]: "exactlytfunction".

S_t(x_1,...,x_n) in [Knuth, Volume 4, Fascicle 0]: "basic
symmetric functions".
It seems there is no generally accepted name for them. How do we call them?

From these basic symmetric functions every symmetric boolean function can be computed.

[Knuth] uses S_T, where T is a subset of {0,1,...,n}, to denote the symmetric function which is true iff the number of ones of the input is an element of T. (Actually, [Knuth] uses a list T, which we better replace by a set.)

By the S_T we uniquely represent all 2^n symmetric functions.

Section 3.4 in [Wegener] presents short circuits for the basic symmetric functions.

Only one output is considered, i.e., the type is [n,1].

All n+1 basic symmetric functions together are represented by Shannon's "symmetric switching cicuit".

This boolean function is of type [n,n+1], where the output j is the ecardinality_bf(n,j).

We need to find literature on that.

The circuit is of size O(n^2); are there better ways? Apparently not.

The easiest representation seems to be as a boolean branching program with n+1 output nodes (for the possible countvalues), using a staircasegridstructure.
Definition in file Thresholds.hpp.