Numerous problems in artificial intelligence can be expressed as conjunctions of constraints over Boolean variables, taking either the value 0 (false) or 1 (true), often represented with formulae in conjunctive normal form (CNF). On such representations, so-called modern SAT solvers are very efficient in practice. However, these solvers are limited by the weakness of the resolution proof system they use internally. A possible workaround is to replace this proof system by the cutting planes proof system, which also allows to deal with pseudo-Boolean constraints (authorizing the use of coefficients in the constraints). However, this is often not enough to offer time guarantees on the resolution of the considered problems, which are NP-complete. When such guarantees are needed (e.g., for applications involving interactions with users), one may compile the input problem into a different language, in which the wanted operations can be applied efficiently (ideally, in polynomial time). In this context, it is often convenient to consider graph or hypergraph representations of the input problem, which provide information about its structure. For instance, current compilers exploit the partitioning of these graphs to decide in which order variables should be assigned. In this presentation, we will present different (hyper)graph representations of CNF formulae, and study how their partitioning may allow to find smaller compiled form for these problems. We will also present how this technique may be extended to allow the compilation of pseudo-Boolean formulae.