Encode a given pseudo boolean constraint \(\sum_i a_i x_i \ge c\) into an equilavent formula in the form of \(\bigwedge_j \bigvee_k \sum_{l \in L_{j,k}} l \ge d_{j,k}\).

Perform normalizePBLinAtLeast and sort the terms in descending order of coefficients

\(\sum_{j=1}^i b_j s_j = \sum_{j=1}^i b_j (x_1, \ldots, x_j)\) is represented as a list of tuples consisting of \(b_j, j, [x_1, \ldots, x_j]\).

Convert PBLinSum to PrefixSum. The PBLinSum must be preprocessed before calling the function.

Algorithm 2 in the paper but with a bug fixed

Algorithm 2 in the paper

Algorithm 1 in the paper

A constraint \(s_i \ge c\) where \(s_i = x_1 + \ldots + x_i\) is represnted as a tuple of \(i\), \([x_1, \ldots, x_i]\), and \(c\).

Forget \(s_i\) and returns \(x_1 + \ldots + x_i \ge c\).

\((s_i \ge a) \Rightarrow (s_j \ge b)\) is defined as \((i \le j \wedge a \ge b) \vee (i \ge b \wedge i - a \le j - b)\).

Disjunction of BCLit

Remove redundant literals based on implyBCLit.

\(C \Rightarrow C'\) is defined as \(\forall l\in C \exists l' \in C' (l \Rightarrow l')\).

Conjunction of BCClause

Reduce BCCNF by reducing each clause using reduceBCClause and then remove redundant clauses based on implyBCClause.