From arbitrary formulas to CNF and WCNF¶

Definitions¶

Below we define the BNF grammar for the different formalisms.

Common definitions are:

<BoolLiteral> ::= "true" | "false"

<BoolVar> ::= <Identifier>

<IntegerValue> ::= <Digit> | <Digit> <IntegerValue>

<Identifier> ::= <Letter> | <Letter> <Identifier>

<Digit> ::= "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9"

<Letter> ::= "a" | ... | "z" | "A" | ... | "Z"

<Comparator> ::= ("LT" | "LE" | "EQ" | "GE" | "GT")

Implicitly, boolean (and PB) expressions can be converted to integers by defining them as 1 (0) when they evaluate to true (false).

Expression¶

Arbitrary boolean expression.

<Expression> ::=
    <BoolVar>
    | <BoolLiteral>
    | <UnaryBoolOp>
    | <BinaryBoolOp>
    | <PbOp>

<IntExpression> ::=
    <Expression>
    | <IntegerValue>
    | <UnaryIntOp>
    | <BinaryIntOp>

<UnaryBoolOp> ::= "NOT" <Expression>

<BinaryBoolOp> ::= <Expression> ("AND" | "OR" | "IF" | "IFF") <Expression>

<UnaryIntOp> ::= "MINUS" <IntExpression>

<BinaryIntOp> ::= <IntExpression> ("ADD" | "MULTIPLY") <IntExpression>

<PbOp> ::= <IntExpression> <Comparator> <IntExpression>

Steps to convert from Expressions to CNF Boolean formulas¶

An EPB formula \(\varphi\) can be translated into a quasi-equivalent CNF Boolean formula \(\Omega\), as follows:

Convert \(\varphi\) into Negation Normal Form (NNF): That involves: (1) Remove all the implications in \(\varphi\). We traverse the formula in post-order, replacing \(F_1 \leftrightarrow F_2\) for \((\neg F_1 \vee F_2) \wedge (\neg F_2 \vee F_1)\), and \(F_1 \rightarrow F_2\) for \((\neg F_1 \vee F_2)\), and (2) traverse in pre-order, pushing down negations by applying the De Morgan's rule, Double Negation rule, and inverting the comparison operator (e.g. \(\le\) for \(>\) and so on).
Process top-level nested inequalities: For every top-level nested PB inequality in \(\varphi\), replace every non-atomic \(F_i\) in the inequality by a fresh auxiliary variable \(aux\). Now, all arithmetic expressions in \(\varphi\) are atomic inequalities (i.e. PB constraints for which we have an encoder to translate them into CNF).
Process atomic PB inequalities: Replace every PB constraint in \(\varphi\) by a fresh auxiliary variable \(aux\). Now, \(\varphi\) is a Boolean formula in NNF.
Convert \(\varphi\) to CNF: Add CNF(\(\varphi\)) to the output formula \(\Omega\).
Encode atomic PB inequalities: For each PB constraint \(\tau\) and corresponding \(aux\) from step 3: (1) (if needed) Normalize PB constraint and (2) add CNF(\(aux \rightarrow PBtoCnfEncoder(\tau)\) and \(\neg aux \rightarrow PBtoCnfEncoder(\neg \tau)\)) to \(\Omega\) .
Encode subformulas \(F_i\) from step 2: For each \(F_i\) and corresponding \(aux\) from step 2, apply recursively this procedure on \(aux \rightarrow F_i\) and \(\neg aux \rightarrow \neg F_i\).

Observations: Notice that, from a more general perspective, step 2 is applied whenever there is no encoder capable of translating the given expression directly into CNF. In such cases, we use the Tseitin transformation ¹, replacing subformulas with auxiliary Boolean variables so that the resulting expression can be encoded into CNF using an available encoder.

Regarding the application of the Tseitin transformation, one may wonder why in steps 5 and 6 we do not simply introduce equivalences of the form \(aux \leftrightarrow CNF(expr)\). This approach is correct only if \(CNF(expr)\) does not introduce additional auxiliary variables. Otherwise, the implication \(CNF(expr) \rightarrow aux\) is not sound. Indeed, it is possible to construct an interpretation that satisfies \(expr\) while falsifying \(aux\). This happens because the auxiliary variables introduced inside \(CNF(expr)\) may be assigned values that falsify some clause in \(CNF(expr)\), even though the original expression \(expr\) itself remains satisfied.

Also, we can make the Tseitin transformation more efficient by only working on one direction of implications in steps 5 and 6 as in ². To do this, we check if variable \(aux\) appears in \(\Omega\) with just one polarity. If the polarity is positive (negative) only work with \(aux \rightarrow expr\) (\(\neg aux \rightarrow \neg expr\)).

If our PBtoCnf encoder requires a normalized PB constraint as input, we follow these steps: (1) convert the PB constraint into \(\le\) expression, (2) move non-constant terms to the Left Hand Side, (3) convert all negative terms into positive by replacing \(-F\) for \(-(1-\neg F)\) and (4) move all constants to the Right Hand Side. See, for example, ³.

From multisets of weighted expressions to WCNF Boolean formulas¶

Finally, a multiset of Weighted expressions \(\phi\) can be translated into a MaxSAT equivalent WCNF Boolean formula \(\Omega\), as follows:

For each Weighted EPB formula \((w,\varphi) \in \phi\):\ If \(w = \infty\):
1. For each clause \(c \in CNF(\varphi)\), add hard clause \([c]\) to \(\Omega\).
If \(w \neq \infty\):
1. Create a fresh auxiliary variable \(aux\).
2. Add soft clause \((w,aux)\) to \(\Omega\).
3. For each clause \(c \in CNF(\varphi)\), add hard clause \([\neg aux, c]\) to \(\Omega\).
Observation: Notice that \(CNF(\varphi)\) corresponds to the previous procedure to transform from Expressions to CNF Boolean formulas.

G. S. Tseitin. On the complexity of derivation in propositional calculus. In Jörg H. Siekmann and Graham Wrightson, editors, Automation of Reasoning: 2: Classical Papers on Computational Logic 1967–1970, pages 466–483. Springer Berlin Heidelberg, Berlin, Heidelberg, 1983. URL: https://doi.org/10.1007/978-3-642-81955-1_28, doi:10.1007/978-3-642-81955-1_28. ↩
David A. Plaisted and Steven Greenbaum. A structure-preserving clause form translation. Journal of Symbolic Computation, 2(3):293–304, 1986. URL: https://www.sciencedirect.com/science/article/pii/S0747717186800281, doi:https://doi.org/10.1016/S0747-7171(86)80028-1. ↩
Jakob Nordström. Pseudo-boolean solving and optimization. Tutorial at the Simons Institute for the Theory of Computing, February 2021. “Satisfiability: Theory, Practice, and Beyond” Boot Camp. URL: https://jakobnordstrom.se/docs/presentations/TalkSimons2102_PseudoBooleanSolvingTutorial.pdf. ↩