# pseudoboolean_constraints_from_a_knowledge_representation_perspective__c6d1d076.pdf Pseudo-Boolean Constraints from a Knowledge Representation Perspective Daniel Le Berre1,2, Pierre Marquis1,2,3, Stefan Mengel1, Romain Wallon1,2 1CRIL-CNRS UMR 8188, Lens, France 2Universit e d Artois 3 Institut Universitaire de France leberre@cril.fr, marquis@cril.fr, mengel@cril.fr, wallon@cril.fr We study pseudo-Boolean constraints (PBC) and their special case cardinality constraints (CARD) from the perspective of knowledge representation. To this end, the succinctness of PBC and CARD is compared to that of many standard propositional languages. Moreover, we determine which queries and transformations are feasible in polynomial time when knowledge is represented by PBC or CARD, and which are not (unconditionally or unless P = NP). In particular, the advantages and disadvantages compared to CNF are discussed. 1 Introduction Many applications in AI are based on propositional information. When dealing with such applications, an important issue is thus choosing a representation from a given language, for the information that is suited to the way that the information is processed [Gogic et al., 1995]. However there exist dozens of languages for representing propositional information. The large number of candidate languages is explained by the fact that there is no single language that is the best for all potential tasks to be achieved on propositional information. Indeed, the right choice typically depends on the way the information is primarily reported and on the efficiency of the computations which must be made on it for the application at hand. Thus, one needs to consider selection criteria to make an informed choice [Darwiche and Marquis, 2002]. In many cases, propositional information represents laws or constraints which must be aggregated conjunctively. In such cases, the language CNF consisting of conjunctions of propositional clauses is often used. Thus, many benchmarks corresponding to various AI applications (and many applications outside the AI area as well) are encoded as CNF formulae, most often in the standard DIMACS format [DIMACS, 1993]. The focus on CNF is justified by the fact that clauses are basic objects, which can be interpreted as very simple if-then rules, and encoded and handled in a straightforward way (as lists of literals). Moreover, there is a rich ecosystem around CNF formulae with preprocessors, solvers and benchmark instances from many fields, see e.g. [SATLIB, 1999; Biere et al., 2009]. However, CNF suffers from some weaknesses. Clauses are somewhat too simple to express some important constraints. For instance, it is shown in [Dixon, 2004] that stating that, in a given set of m variables, at least n of them must be set to true cannot be carried out using a number of clauses that is polynomial in n in general without adding any new variables, which is undesirable in some settings (see the conclusion of the paper). In order to encode such constraints in a compact way, generalizations of the clause representation have been considered, in particular the so-called pseudo-Boolean constraints (linear equations or inequalities over literals), strongly related to threshold functions [Crama and Hammer, 2011], and their special case cardinality constraints (pseudo-Boolean constraints where each literal has a coefficient equal to one). These two constraints regularly arise naturally in many settings. Obviously enough, any clause Wk i=1 li can be turned in linear time into an equivalent cardinality constraint of the form Pk i=1 li 1 so all information represented by a CNF formula can easily be transformed into a cardinality constraint representation. Pseudo-Boolean constraints have also attracted attention due to associated proof systems, like the cutting planes system, that have been introduced for proving the inconsistency of a conjunction of such constraints [Cook et al., 1987; Hooker, 1988; Nordstr om, 2015]. The cutting planes proof system is known to p-simulate the well-known resolution proof system, the underlying of modern SAT solvers, which means that there exists a fixed polynomial p such that every refutation of size l in the latter proof system can be turned into a refutation of size p(l) in the former proof system. However, the converse does not hold: there are families of inconsistent CNF formulae over n variables for which any resolution proof of a contradiction is of size exponential in n, while when the formulae are encoded in a natural way as pseudo-Boolean constraints, cutting planes refutations of size linear in n exist. This is the case for the family of inconsistent pigeonhole instances [Haken, 1985; Krishnamurthy, 1985]. This explains why several dedicated solvers that aim to take advantage of the strength of the cutting planes system have been implemented [Barth, 1995; Dixon and Ginsberg, 2002; Chai and Kuehlmann, 2003; Sheini and Sakallah, 2006; Le Berre and Parrain, 2010]. In this paper, we do not consider issues about proof systems but instead analyse the properties of the language PBC of pseudo-Boolean constraints and those of its subset, the lan- Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18) guage CARD of cardinality constraints, concerning the representation of propositional information. In this direction, several questions have to be considered concerning the spatial efficiency of the two languages (i.e., their ability to represent propositional information using little space) as well as their temporal efficiency (i.e., the ability to exhibit a number of queries and transformations which are tractable when the information used is encoded in the language). Of specific interest are the advantages and disadvantages of PBC and CARD compared to CNF. For instance, it is known that the language CNF is not more succinct than the language FBDD of free binary decision diagrams. Does this also hold for PBC or CARD? It is also known that deciding whether a consistent conjunction of literals implies a CNF formula can be done in polynomial time. Does this still hold for PBC or CARD representations? Addressing those issues in a principled way amounts to considering the criteria used in the knowledge compilation map for comparing target compilation languages [Darwiche and Marquis, 2002]. Though neither PBC nor CARD can be considered as compilation languages (since none of them offers a polynomial-time algorithm for deciding consistency), we argue that the criteria (succinctness, polynomial-time queries and transformations) used to compare compilation languages are meaningful for other propositional languages since they provide a systematic approach to the questions above. Thus, in the following, the relative succinctness of PBC and CARD compared to many standard propositional languages (CNF, NNF, OBDD, etc.) is determined. Then, we examine whether the queries and transformations which are considered in the knowledge compilation map are supported efficiently by PBC and CARD or not (which amounts to deciding whether a polynomial-time algorithm for carrying out the query or the transformation exists or not unconditionally or unless P = NP). Our results show that, on the one hand, despite the extra succinctness of CARD and PBC compared to CNF, their relation to standard propositional languages like DNF, OBDD, FBDD is the same: those languages which are incomparable to CNF w.r.t. succinctness are also incomparable to PBC w.r.t. succinctness. On the other hand, the improvement w.r.t. spatial efficiency which results from such a switch does not imply the loss of many tractable queries or transformations: all the queries and all the transformations, offered by CNF except SFO and BC are preserved. 2 Preliminaries We consider a propositional setting based on a finite set of propositional variables. A literal is a variable or its negation and a clause is a disjunction of literals. All the representations considered in the following are interpreted in the classical way, so that the notions of consistency, validity, entailment, equivalence are the standard ones. |= denotes entailment and denotes equivalence. The size of a representation ϕ, denoted |ϕ|, is the number of elementary symbols used in ϕ (integers are represented in binary notation). 2.1 Pseudo-Boolean Constraints Among all the propositional representations considered in the following we are specifically interested in pseudo-Boolean constraints. Definition 2.1 (Pseudo-Boolean constraint). A pseudo Boolean constraint is of the form Pn i=1 aili k, where n is some non-negative integer, i {1, . . . , n}, ai Z, li is a literal, {<, , =, , >} and k Z. Each ai is called a weight and k is called the degree of the constraint. A normalized pseudo-Boolean constraint is a pseudo Boolean constraint of the form Pn i=1 aili k, where i {1, . . . , n}, ai N, k N and each variable appears only once in the constraint, either positively or negatively. From now on, we assume that all the pseudo-Boolean constraints under consideration are normalized. This assumption is harmless, computationally speaking: Proposition 2.2 ([Barth, 1995; Roussel and Manquinho, 2009]). Any pseudo-Boolean constraint can be turned in polynomial time into an equivalent, normalized pseudo Boolean constraint, or a conjunction of such constraints. In the following, we also focus on a specific family of pseudo-Boolean constraints, consisting of cardinality constraints. A cardinality constraint is a normalized pseudo Boolean constraint of the form Pn i=1 li k where n is some non-negative integer. Definition 2.3 (PBC, CARD). PBC (resp. CARD) is the language of conjunctions of normalized pseudo-Boolean constraints (resp. cardinality constraints). In this paper, we use the following inference rules to reason with pseudo-Boolean constraints: Saturation. Let κ be a (normalized) pseudo-Boolean constraint κ = Pn i=1 aili k where for some i0 in {1, . . . , n}, ai0 > k. Then, ai0 can be replaced by k without changing the models of the constraint. Division. Let κ be a (normalized) pseudo-Boolean constraint κ = Pn i=1 aili k and an integer α > 0. κ entails the constraint Pn i=1 ai α , where x denotes the smallest integer greater or equal to x. Moreover, if α is a divisor of each ai, then κ is equivalent to the latter constraint. Note that, in the division rule, we do not require k to be divisible by α. This property allows the proof system to be more powerful than resolution [Cook et al., 1987]. For example, the constraint 2x + 2y + 2z 3 becomes x + y + z 2, which eliminates some non-integral solutions. 2.2 Knowledge Compilation Map The knowledge compilation map reported in [Darwiche and Marquis, 2002] is a systematic, multi-criteria comparative analysis of propositional representation languages. The choice of a language L is then guided by its spatial efficiency (its succinctness) and its temporal efficiency (the queries and transformations it offers, viewed as properties of L). Succinctness. Succinctness captures the (relative) ability of a language to represent information using little space, and yields a pre-order s. A propositional language L1 is said to be at least as succinct as another language L2, denoted Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18) L1 s L2, if and only if there exists a polynomial p such that for every formula α L2, there exists an equivalent formula β L1 where |β| p(|α|). When L1 s L2 and L2 s L1, we write L1 1, and let us consider M the model of κ such that x is satisfied, and any literal which is in κ is falsified, except x. In this interpretation, we necessarily have Pm i=1 li 1, since only x is satisfied by construction. Indeed, if x positively appears in κ , then Pm i=1 li = 1. Otherwise, Pm i=1 li = 0. In both cases, since we have assumed k > 1, κ is not satisfied, so M is not a model of κ . This contradicts that κ |= κ , so k 1. Since κ is supposed to be non-valid, k cannot be equal to 0, so k = 1. The only way to represent κ as a conjunction of cardinality constraints is then to use clauses, since all these constraints must be implied by κ. However, thanks to Proposition 4.1.4 from [Dixon, 2004], we have that an exponential number of clauses is required to represent κ, and this completes the proof. Proposition 3.2. NNF s PBC. Sketch of Proof. Let κ = Pn i=1 aili k be a pseudo Boolean constraint. It is well known that any pseudo-Boolean constraint Pn i=1 aili k can be represented by an equivalent NNF representation of polynomial size (see e.g. [Vollmer, 1999]). Now, when a conjunction of pseudo-Boolean constraints is considered, an NNF representation of it consists of the conjunction of all these elementary NNF representations one per pseudo-Boolean constraint. As an immediate consequence of [Dixon, 2004] (Proposition 4.1.4), we have the following result: Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18) Proposition 3.3. CARD 0. Claim 3.9. For all j {1, . . . , n}, xj or yj appears positively in κ. Sketch of Proof. If neither xj nor yj appear in Var(κ), then the model of ϕ satisfying xj and yj but falsifying all the literals of κ is not a model of κ, which contradicts ϕ |= κ. Claim 3.10. For all j {1, . . . , n}, if xj appears positively in κ, and yj does not, then the weight of xj is k. Symmetrically, for all j {1, . . . , n}, if yj appears positively in κ, and xj does not, then the weight of yj is k. Sketch of Proof. If only xj appears positively in κ, say xj = lj0, and aj0 < k, then the model of ϕ satisfying both xj and yj but falsifying all the other literals of κ is not a model of κ, which contradicts ϕ |= κ. The proof for the case when only yj appears positively in κ is similar. Claim 3.11. For all j {1, . . . , n}, if xj and yj appear positively in κ, then the sum of their weights is at least equal to k. Sketch of Proof. If both xj and yj appear positively as lj0 and lj1 in κ, respectively, and aj0 + aj1 < k, then the model of ϕ satisfying these two literals but falsifying all the others of κ is not a model of κ, which contradicts ϕ |= κ. Claim 3.12. Without loss of generality, κ can contain only positive literals. Sketch of Proof. If yj appears in κ, let κ be the pseudo Boolean constraint obtained by removing the literal yj from κ. The case where xj appears in κ follows symmetrically. Any model M of ϕ is a model of κ . Indeed, if M satisfies yj, then it is obviously a model of κ . Otherwise, there exists i = j such that M satisfies xi and yi, and by Claims 3.9, 3.10 and 3.11, κ is also satisfied by M. So, ϕ |= κ , and since we obviously have that κ |= κ, it is possible to replace κ by κ without losing information. All negative literals can be removed by repeating the same argument. Let K = Vm j=1 κj be any conjunction of pseudo-Boolean constraints such that ϕ K. Thanks to the previous results, we have: j {1, . . . , m}, κj = Pn i=1 a0,i,jxi + a1,i,jyi kj, with, i {1, . . . , n}, a0,i,j + a1,i,j kj by applying Claim 3.11. Any counter-model of ϕ must be a counter-model of K. It remains to show, in the rest of this proof, that a subset of these counter-models requires the use of an exponential number of pseudo-Boolean constraints to get a formula logically equivalent to ϕ. Any interpretation satisfying for all i {1, . . . , n} exactly one of xi or yi cannot be a model of K, since it is not a model of ϕ. Then, it must not satisfy at least one of the constraints Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18) κj. Formally, this means that the following property must be satisfied. Property ( ). For any function f : {1, . . . , n} {0, 1}, there exists j {1, . . . , m} such that Pn i=1 af(i),i,j < kj For each of the inequalities induced by ( ), we define a tuple (f(1), . . . , f(n)) Bn. We claim that two inequalities associated with such tuples which have a Hamming distance at least equal to 2 cannot be satisfied for a same j. Otherwise, let (f1(1), . . . , f1(n)) and (f2(1), . . . , f2(n)) be two tuples with a Hamming distance at least equal to 2 for a same j. Their associated inequalities are (1) Pn i=1 af1(i),i,j < kj and (2) Pn i=1 af2(i),i,j < kj. Since the Hamming distance between the two tuples is at least equal to 2, there exists α, β {1, . . . , n}, with α = β, such that f1(α) = f2(α) and f1(β) = f2(β). By adding (1) and (2), since f1 and f2 take their values in {0, 1}, we get: a0,α,j + a1,α,j + a0,β,j + a1,β,j i=1 i {α,β} (af1(i),i,j + af2(i),i,j) < 2kj However, this is impossible since Claim 3.11 gives us a0,α,j + a1,α,j kj and a0,β,j + a1,β,j kj, so a0,α,j + a1,α,j + a0,β,j + a1,β,j 2kj. So, we need two distinct constraints to satisfy the inequalities of ( ) associated with these tuples. Claim 3.13. There exists a set of 2n 1 tuples of Bn having pairwise Hamming distance at least 2. Sketch of Proof. Consider the set S of solutions over {0, 1} of Pn i=1 zi is equivalent to 0 mod 2. The elements of S have pairwise Hamming distance at least 2. Finally, S contains 2n 1 elements since any assignment to z1, . . . , zn 1 can be extended to a solution in S. Hence, to get satisfied, the system of inequalities associated with these tuples requires at least 2n 1 distinct constraints. So, representing ϕ as a conjunction of pseudo-Boolean constraints requires exponentially many constraints. The remaining succinctness results reported in Figure 1 are easy consequences of the previous one, taking advantage of the transitivity of s and of the succinctness results given in [Darwiche and Marquis, 2002; Bova et al., 2016]. 4 Querying Pseudo-Boolean Constraints We now present the results about the queries offered by PBC and CARD summarized in Table 1. Proposition 4.1. CARD does not satisfy CO, CE, EQ, SE, CT and ME, unless P = NP. Proof. Since the translation of any CNF formula into a conjunction of cardinality constraints can be done in polynomial time, and since CNF does not satisfy any of these properties, unless P = NP, the claim follows. CO VA CE IM EQ SE CT ME CARD PBC Table 1: Properties of CARD and PBC about queries. A means that the query is offered by the language, and a means that it is not the case, unless P = NP. CD FO SFO C BC C BC C CARD ? PBC Table 2: Properties of CARD and PBC about transformations. A means that the language offers the transformation, whereas a means that it does not unless P = NP and a means that it does not unconditionally. Since CARD is a sublanguage of PBC, we get: Corollary 4.2. PBC does not satisfy CO, CE, EQ, SE, CT and ME, unless P = NP. We also have that: Proposition 4.3. PBC and CARD satisfy VA. Proof. A conjunction of pseudo-Boolean constraints is valid if and only if all of its constraints are valid. This is the case if and only if all the constraints have a degree equal to 0, which can be checked in polynomial time. Since PBC and CARD satisfy VA and CD (cf. Section 5), the following corollary follows immediately by Lemma A.7 from [Darwiche and Marquis, 2002]. Corollary 4.4. PBC and CARD satisfy IM. 5 Transforming Pseudo-Boolean Constraints Finally, we present the results we have obtained about the transformations offered by PBC and CARD. They are summarized in Table 2. Proposition 5.1. PBC and CARD satisfy CD. Proof. Computing the conditioning of any formula from PBC (resp. CARD) is easily done by replacing, in each constraint, every literal of the conditioning term by a Boolean constant. This produces, after a trivial normalization step made in polynomial time, a conjunction of pseudo-Boolean constraints (resp. cardinality constraints). Proposition 5.2. CARD and PBC satisfy both BC and C. Proof. Given a conjunctively-interpreted set of formulae from CARD (resp. PBC), computing the conjunction of these formulae can trivially be done in polynomial time. Proposition 5.3. CARD does not satisfy BC. Proof. Let ϕ be the disjunction of the two cardinality constraints κ = y 1 (κ y) and κ = P2n i=1 xi n. It is easy to see that ϕ is equivalent to ny + P2n i=1 xi n. As shown in the proof of Proposition 3.1, a representation of this constraint using only cardinality constraints requires exponentially many constraints. Hence, the claim follows. Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18) Proposition 5.4. PBC does not satisfy BC. Proof. To prove this result, we show that any representation of the inequality = P2n i=1 xi = n, which is equivalent to the disjunction of P2n i=1 xi n+1 and P2n i=1 xi n+1, requires an exponential number of pseudo-Boolean constraints when n 2. Let us consider a non-valid pseudo-Boolean constraint κ = Pm i=1 aili k, such that |= κ, with Var(κ) Var( ). Let us note L+ and L the sets of positive and negative literals of κ, respectively. Claim 5.5. We have Var(κ) = Var( ). Sketch of Proof. Consider I a counter-model of κ. Since |= κ, I satisfies n of the xi. If x in Var( ) but x Var(κ), then the interpretation I defined by I = I {x} satisfies n + 1 of the xi, so it is a model of , but not a model of κ, which contradicts |= κ. Claim 5.6. We have |L+| = |L |. Proof. If |L+| < |L |, then by Claim 5.5, we necessarily have |L | > n. The interpretation M = {xi|xi L } satisfies strictly more than n of the xi, so it is a model of , but not a model of κ. If |L | < |L+|, then by Claim 5.5, we necessarily have |L+| > n. The interpretation M = {xi|xi L } satisfies strictly less than n of the xi, so it is a model of , but not a model of κ. In both cases, |= κ is contradicted, so |L+| = |L |. Claim 5.7. We have i {1, . . . , m}, ai = k. Proof. Let us suppose that i0 {1, . . . , m}, ai0 < k and that the variable associated with li0 is xi 0. There are two possible cases: either xi 0 L+ or xi 0 L . If xi 0 L+, let us consider the interpretation M = {xi 0} {xi|xi L }. Then, by Claims 5.5 and 5.6, M satisfies n + 1 of the xi, so it is a model of . Otherwise, xi 0 L and let us consider the interpretation M = {xi|xi L }\{xi 0}. Then, M satisfies (n 1) of the xi, so it is a model of . In both cases, Pn i=1 aili = ai 0 < k, so M is not a model of κ. |= κ is contradicted, so i {1, . . . , m}, ai = k. Thus, the division rule gives that κ = Pm i=1 kli k Pm i=1 li 1, in other words, κ is equivalent to a clause. The only way to represent as a conjunction of pseudo-Boolean constraints is then to use clauses, since all the constraints must be implied by . However, requires an exponential number of clauses to be represented without introducing any new variable. Indeed, a clause as the ones we have produced in this proof can only eliminate a single counter-model of , since all those clauses contain all the variables, and there exist 2n n counter-models. Hence, the claim follows. Corollary 5.8. CARD and PBC satisfy neither C nor C. We also have that: Proposition 5.9. PBC does not satisfy SFO. Proof. Let κ and κ be the two pseudo-Boolean constraints defined by P2n i=1 xi n + 1 and P2n i=1 xi n + 1, respectively. Let us consider, for s a newly introduced variable, the formulae κs = (n + 1)s + P2n i=1 xi n + 1 and κ s = (n + 1)s + P2n i=1 xi n + 1, which are obtained from κ and κ in polynomial time. Let ϕ = κs κ s. By construction, ϕ|s κ and ϕ| s κ. So, x ϕ κ κ . If an algorithm existed to forget a single variable in a set of pseudo-Boolean constraints, then one could use it to compute in polynomial time the disjunction of κ and κ . However, we have proven that it is not possible (cf. Proposition 5.4). Then, so it is for the forgetting of a single variable in a conjunction of pseudo-Boolean constraints. Corollary 5.10. PBC does not satisfy FO. We also have that: Proposition 5.11. CARD does not satisfy FO, unless P = NP. Proof. As for CNF, if CARD satisfied FO, then it would be possible to compute CO on a formula from CARD in polynomial time. Indeed, a formula is consistent precisely when the representation obtained by forgetting all its variables in it evaluates to true (which can be tested easily since the set of variables of the resulting formula is empty). 6 Conclusion We have studied the language PBC of pseudo-Boolean constraints and the language CARD of cardinality constraints from a knowledge representation perspective. Our results show that switching from CNF to CARD and then to PBC increases the succinctness of the representations but does not lead to languages that would be at least as succinct as other propositional languages, like DNF, OBDD, or FBDD. Interestingly, such a switch does not lead to the loss of any tractable query that is supported by CNF. As to the transformations, both PBC and CARD lose BC, and PBC loses SFO as well. No transformation is gained w.r.t. CNF. Accordingly, when dealing with applications involving propositional representations but not requiring to perform any transformation among SFO and BC, we now know that the languages PBC and CARD are valuable alternatives to CNF due to the succinctness increase they may lead to. Of course, every PBC representation Σ can be turned in linear time into a CNF representation Φ which is not equivalent to it, but has the same logical consequences over the variables occurring in Σ. The translations used to go from Σ to Φ (especially those reported in [Plaisted and Greenbaum, 1986; Tseitin, 1968]) consist in introducing in Φ additional variables not occurring in Σ (in fact, Σ is equivalent to the formula we get by forgetting those variables in Φ). Since such translations can be achieved in linear time, the size of Φ is also linear in that of Σ. While using Φ instead of Σ is a feasible alternative for answering certain queries over the variables occurring in Σ, it must be noted that Φ cannot be substituted to Σ in every setting, i.e., for answering any query or achieving any transformation. For instance, Φ and Σ do Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18) not have the same implicants in the general case. In addition the queries and transformations offered by the language of CNF with some existentially quantified variables (alias the existential closure of CNF) do not coincide with those offered by PBC and CARD [Fargier and Marquis, 2008]. All this explains why the extra succinctness of PBC and CARD compared to CNF can be considered as a decisive advantage for some applications. Acknowledgements The authors are grateful to the anonymous reviewers for their numerous comments. These comments greatly helped to improve the presentation of the paper. Part of this work was supported by the French Ministry for Higher Education and Research, the Hauts-de-France Regional Council through the Contrat de Plan Etat R egion (CPER) DATA and an EC FEDER grant. [Barth, 1995] Peter Barth. A Davis-Putnam based Enumeration Algorithm for Linear Pseudo-Boolean Optimization. Technical Report MPI-I-95-2, Max-Planck Institut F ur Informatik, 1995. [Biere et al., 2009] Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2009. [Bova et al., 2016] Simone Bova, Florent Capelli, Stefan Mengel, and Friedrich Slivovsky. Knowledge Compilation Meets Communication Complexity. In IJCAI 16, pages 1008 1014, 2016. [Bryant, 1986] Randal E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput., 35(8):677 691, 1986. [Chai and Kuehlmann, 2003] Donald Chai and Andreas Kuehlmann. A fast pseudo-Boolean constraint solver. In DAC 03, pages 830 835, 2003. [Cook et al., 1987] William Cook, Collette R. Coullard, and Gy orgy Tur an. On the Complexity of Cutting-plane Proofs. Discrete Appl. Math., 18(1):25 38, 1987. [Crama and Hammer, 2011] Yves Crama and Peter L. Hammer. Boolean Functions: Theory, Algorithms, and Applications. Cambridge University Press, 2011. [Darwiche and Marquis, 2002] Adnan Darwiche and Pierre Marquis. A Knowledge Compilation Map. Journal of Artificial Intelligence Research, 17(1):229 264, 2002. [Darwiche, 1999] Adnan Darwiche. Compiling knowledge into decomposable negation normal form. In IJCAI 99, pages 284 289, 1999. [Darwiche, 2001] Adnan Darwiche. Decomposable negation normal form. J. ACM, 48(4):608 647, 2001. [DIMACS, 1993] DIMACS. Satisfiability: Suggested Format. DIMACS Challenge. DIMACS, 1993. [Dixon and Ginsberg, 2002] Heidi E. Dixon and Matthew L. Ginsberg. Inference methods for a pseudo-boolean satisfiability solver. In AAAI 02, pages 635 640, 2002. [Dixon, 2004] Heidi Dixon. Automating Pseudo-Boolean Inference Within a DPLL Framework. Ph D thesis, University of Oregon, 2004. [Fargier and Marquis, 2008] H el ene Fargier and Pierre Marquis. Extending the knowledge compilation map: Closure principles. In ECAI 08, pages 50 54, 2008. [Gogic et al., 1995] Goran Gogic, Henry Kautz, Christos Papadimitriou, and Bart Selman. The comparative linguistics of knowledge representation. In IJCAI 95, pages 862 869, 1995. [Haken, 1985] Armin Haken. The intractability of resolution. Theoretical Computer Science, 39:297 308, 1985. [Hooker, 1988] John N. Hooker. Generalized resolution and cutting planes. Annals of Operations Research, 12(1):217 239, 1988. [Krishnamurthy, 1985] Balakrishnan Krishnamurthy. Short proofs for tricky formulas. Acta Informatica, 22:253 275, 1985. [Le Berre and Parrain, 2010] Daniel Le Berre and Anne Parrain. The SAT4J library, Release 2.2, System Description. Journal on Satisfiability, Boolean Modeling and Computation, 7:59 64, 2010. [Nordstr om, 2015] Jakob Nordstr om. On the Interplay Between Proof Complexity and SAT Solving. ACM SIGLOG News, 2(3):19 44, 2015. [Plaisted and Greenbaum, 1986] David A. Plaisted and Steven Greenbaum. A structure-preserving clause form translation. Journal of Symbolic Computation, 2(3):293 304, 1986. [Quine, 1952] Willard V. Quine. The problem of simplifying truth functions. The American Mathematical Monthly, 59(8):521 531, 1952. [Roussel and Manquinho, 2009] Olivier Roussel and Vasco M. Manquinho. Pseudo-Boolean and Cardinality Constraints. In Handbook of Satisfiability, pages 695 733. 2009. [SATLIB, 1999] SATLIB. The Satisfiability Library, 1999. http://www.cs.ubc.ca/ hoos/SATLIB/index-ubc.html. [Sheini and Sakallah, 2006] Hossein M. Sheini and Karem A. Sakallah. Pueblo: A Hybrid Pseudo-Boolean SAT Solver. JSAT, 2(1-4):165 189, 2006. [Tseitin, 1968] Gregory S. Tseitin. On the complexity of derivation in propositional calculus, chapter Structures in Constructive Mathematics and Mathematical Logic, pages 115 125. 1968. [Vollmer, 1999] Heribert Vollmer. Complexity Measures and Reductions. In Introduction to Circuit Complexity: A Uniform Approach. Springer-Verlag New York, Inc., 1999. Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18)