=Paper=
{{Paper
|id=Vol-1782/paper_8
|storemode=property
|title=A Verified Decision Procedure for Pseudo-Boolean Formulas
|pdfUrl=https://ceur-ws.org/Vol-1782/paper_8.pdf
|volume=Vol-1782
|authors=Tobias Philipp,Anna Tigunova
|dblpUrl=https://dblp.org/rec/conf/plansig/PhilippT16
}}
==A Verified Decision Procedure for Pseudo-Boolean Formulas==
https://ceur-ws.org/Vol-1782/paper_8.pdf
A Verified Decision Procedure for Pseudo-Boolean Formulas
Tobias Philipp and Anna Tigunova
International Center for Computational Logic, Technische Universität Dresden, Germany
Abstract yearly evaluated in international SAT competitions. Their
performance over e.g. hardware and software verification [7]
Pseudo-Boolean formulas consist of constraints of the form has improved, enabling them to become widespread tools in
∑ni=1 wi · xi k, where xi are propositional literals, wi ∈ Z, the industry. Moreover, often formalizations of problems
k ∈ Z, and arise in planning, scheduling and optimization
problems. We describe an efficient and easily verifiable de- are close to the clause normal form. Therefore, the use SAT
cision procedure for pseudo-Boolean formulas, that is based solvers is an attractive approach to tackle these problems.
on encoding PB formulas into the propositional satisfiability Due to these reasons many translations from PB con-
problem with the cutting-edge sequential weighted counter straints into propositional formulas in conjunctive normal
encoding. State-of-the-art SAT solvers that emit unsatisfiabil- form have been proposed: naive, nested, watchdog [22],
ity proofs are used to solve the resulting instances. The com- adder- and sorting networks [21, 11], binary merge [20], bi-
bination of a verified translation to SAT, and certified SAT nary decision diagrams [11, 1], and the sequential weighted
solvers leads to a verified decision procedure for PB formu-
counter encoding (SWC) [13]. Specialized encodings also
las. The verification of the encoding is carried out in the Coq
proof assistant. exist for cardinality constraints [2, 26] that are subsumed by
PB constraints.
Among all these, we chose the SWC encoding due to
Introduction the following reasons. First, it produces in the PB bench-
The satisfiability problem is one of the most prominent prob- marks 2011 and 2010 less clauses in 99% of the cases than
lems in theoretical computer science and artificial intelli- the asymptotic best binary merge encoding [13]. Second,
gence and was successfully applied in planning [16, 25], SWC satisfies two important properties: unit propagation in
as well as scheduling [12]. In these applications pseudo- the encoding detects inconsistencies and maintain general-
Boolean (PB) constraints often occur. PB constraints can be ized arc consistency [13]. Third, experiments on all new
represented as ∑ni=1 wi · xi k, where xi are propositional lit- instances of the PB evaluation 2012 have shown that the
erals, wi ∈ Z, k ∈ Z, and hold if and only if the weighted sequential weighted counter encoding performs better than
sum over the xi literals is -related with k. For example, adder and sorting networks, watchdog and binary merge en-
the packing problem can be formalized by means of PB for- codings, within a timeout of 30 minutes [23]. Finally, the
mulas: we pack the given items of sizes a1 , . . . , an into the encoding is relatively simple to describe, which allows us to
minimal number of containers yi such that the volume V of verify it with little effort using interactive theorem provers
the container is not exceeded. Then, we obtain: such as Coq.
The correctness of the PB decision procedure is then re-
n duced to the correctness of the underlying SAT solver. Un-
∑ ai xi, j ≤ V yi for all i ∈ {1 . . . n} fortunately, SAT solver can be buggy: three solvers, that par-
j=1
ticipated in the SAT competition in 2009, and five solvers
Our research is based on the need for formalized and ver- that participated in the SAT competition in 2007 gave in-
ified decision procedures that do not depend on unverified correct results [8]. The critical case is when a formula is
components and pen and paper proofs. Our contribution is reported to be unsatisfiable, as unsatisfiability is hard to see.
an easy pipeline of an efficient encoding to solve PB con- Also subtle bugs in different components of satisfiability
straints, where each step is certified, leading to efficient and solvers were reported in [15]. Therefore, state-of-the-art
easily verifiable decision procedure for PB formulas. Fol- SAT solver like Riss or Lingeling [6] , emit certificates in
lowing Eén and Sörensson [11], we translate PB constraints the DRAT [29] format, which are afterwards checked by an
into formulas in conjunctive normal form, and run after- independent program, such as drat-trim [29]. Still, a proof
wards a SAT solver that finds a solution to the original PB of correctness of the translation from PB constraints to CNF
formula or reports unsatisfiability of the problem. This SAT- is necessary. Figure 1 presents our approach to the problem
based approach is highly successful since SAT solving has of justification of the whole procedure. It is a combination
significantly advanced over the last decades, and solvers are of a mechanically verified translation from PB constraints
into CNF and a certified SAT solver. Such a combination Propositional Logic
then forms a verified decision procedure for PB formulas. In propositional logic we consider an infinite set of proposi-
tional variables V . A literal L is either a propositional vari-
able A or its negation ¬A. The complement of a literal L is
denoted by L, i.e. A = ¬A and ¬A = A. Clauses are lists
Coq specification
pseudo-Boolean formulas of literals and represent disjunction. Formulas are lists of
and proofs
clauses, representing a conjunction.
Haskell code The semantics of formulas is built on interpretations. An
CNF Coq kernel interpretation I is a mapping from the set V of all Boolean
variables to the set {>, ⊥} of truth values, represented by
SAT solver the set of variables, which are true in this interpretation. The
interpretation I satisfies the variable A, in symbols I |= A,
if and only if A ∈ I. Similarly, I satisfies the clause C, in
model / DRAT proof symbols I |= C, if and only if there is a literal L ∈ C, such
that I |= L. For a formula F, the interpretation I satisfies the
formula F, in symbols I |= F, if and only if for every clause
drat trim C ∈ F, we find that the interpretation I satisfies the clause C.
A model I of a formula F is an interpretation I, that satisfies
the formula F. If such a model I of F exists, the formula F
SAT UNSAT unknown is satisfiable. Otherwise, the formula F is unsatisfiable.
Let C and D be two clauses and L be a literal such that
L ∈ C and L ∈ D. Then, the resolvent of C and D upon L
Figure 1: The certified SAT approach combined with a me- is (C \ {L}) ∪ (D \ {L}). A tautological clause is a clause
chanically verified PB encoding: PB formulas can be re- containing A and ¬A for some variable A.
duced to satisfiability of the propositional satisfiability ques-
tion. Then, the SAT solver emits a proof for unsatisfiability, DRAT Refutations
which can be checked independently. As the second step to certify the output of our system we
use drat-trim, which is a checker for unsatisfiability proofs
in DRAT format: The Resolution Asymmetric Tautology
The rest of this paper is structured as follows: First, we
(RAT) property is based on the notion of asymmetric literal
give a short introduction to the proof assistant Coq, propo-
addition [15], where ALAF (C) is defined as
sitional logic, the DRAT format for the certification of SAT
solvers, as well as PB-constraints and the SWC encoding. C ∪ {L | {L1 , . . . , Ln , L} ∈ F and {L1 , . . . , Ln } ⊆ C}
Then we present the formalization of the SWC encoding.
After that we describe the specification and present the proof We consider the recursive application of asymmetric literal
ideas. Then we focus on integration of all parts of the proce- addition:
dure, and evaluate our approach on selected instances from ALAF (C) ↑ 0 = C
the PB competition 2016. Finally, we discuss some future ALAF (C) ↑ n + 1 = ALAF (ALAF (C) ↑ n)
improvements.
A clause C is an asymmetric tautology (AT) w.r.t. the for-
mula F, if there is n ∈ N such that the clause ALAF (C) ↑ n
Background is a tautology.
Järvisalo et al. introduced the following redundancy crite-
The Coq Proof Assistant ria based on an asymmetric tautologies in [15]: The clause C
We use the Coq proof assistant [5] to write our specifica- is a resolution asymmetric tautology (RAT) upon L w.r.t. F,
tions and proofs. Coq is based on the calculus of induc- if (1) the clause C is an asymmetric tautology w.r.t. the for-
tive constructions [9] and combines higher-order logic with mula F, or (2) there is a literal L ∈ C such that the resolvent
a typed functional programming language. In Coq we de- of C and D upon L is an asymmetric tautology w.r.t. the
fine functions in the lambda calculus. Moreover, we can formula F for every D ∈ F with L ∈ D.
express mathematical theorems and can proof them interac- Several important techniques in SAT solvers can be char-
tively. The syntax of Coq is similar to that of other typed acterized in terms of RAT: bounded variable elimination and
functional programming languages. Accepted proofs can be addition [27, 10, 24, 19], blocked clause elimination [14],
independently checked by a small certification kernel. Fi- blocked clause addition [17, 15], probing [18], and extended
nally, we can automatically extract Haskell programs from resolution and reencoding [19, 28].
Coq theories, which give us fully verified programs. There- A DRAT refutation for a formula is a sequence of clauses
fore, Coq provides an essential link from the PB to the SAT to the empty clause having the RAT property with respect to
encoding, because it ensures the correctness of the transla- the preceding clauses, together with deletion information. If
tion. In this way we obtain a verified Haskell program that a DRAT refutation for a formula F exists, then F is unsatis-
transforms PB constraints into CNF. fiable.
x1 x2 ... xn Formalization
We carried out the formalization of the syntax and semantics
of propositional logic, PB constraints, and the SWC encod-
ing in the Coq interactive theorem prover. As most of the
s1,1 s2,1 sn−1,1 formalization is straightforward, we present only the details
... of SWC encoding.
s1,2 s2,2 sn−1,2
We express the sequential weighted counter encoding in
.. .. .. Coq as follows: let wf be a function wf : N 7→ N, that assigns
. . . weights to literals.
s1,k+1 s2,k+1 sn−1,k+1
Definition 1 (Formalization of SWC in Coq). The se-
quential weighted counter for a normalized PB constraint
Figure 2: Illustration of the sequential weighted counter as ∑ni=1 wi xi ≤ k, denoted by SWC(n, k, w f ), is a formula in
conjunctive normal form consisting of the following parts:
a circuit. Each box represents a unit that adds the weight of
the literal to the partial sum, if the variable xi is true. 1. The first formula states the monotonicity of the sum, as
only positive non-zero weights are allowed. If the sum up
to the variable xi is at least j, then the sum to the next
Pseudo-Boolean Constraints and the variable xi+1 is at least j. Formally,
Sequential Weighted Counter (¬si−1, j ∨ si, j ) for all 2 ≤ i < n and 1 ≤ j ≤ k (F1 )
We consider pseudo-Boolean constraints ∑ni=1 wi xi ≤ k
in normal form [3] that meet the following conditions: 2. The second formula states that the sum up to the variable
1. 1 ≤ k < n, 2. weights are between 1 and k, and 3. no xi must be at least wi , if xi is satisfied by the considered
literal occurs more than once. For example, the PB con- interpretation:
straint 2x1 + x2 + 2x1 ≤ 1 is not in normal form, since x1 (¬xi ∨ si, j ) for all 1 ≤ i < n, and 1 ≤ j ≤ wi + 1 (F2 )
occurs more than once. Notice that it is not a restriction to
consider PB constraints in normal form, as all PB constraints 3. The third formula states that the sum up to the variable
can be transformed into a semantically equivalent PB con- xi increases by wi :
straint in normal form. Moreover, normalized constraints do
occur in applications, such as in translations from maximum (¬si−1, j ∨¬xi ∨si, j+wi ) for all 2 ≤ i < n, 1 ≤ j < k −wi +1
satisfiability into PB optimization. (F3 )
A normalized PB constraint can then be transformed to an 4. The fourth formula expresses when an interpretation can-
equivalent propositional formula. For instance, the expres- not be a model of the PB-constraint, i.e. when the
sion 3x1 + 2x2 + 4x3 ≤ 5 is a normalized constraint, that is weighted sum exceeds k. Formally:
semantically equivalent to the following formula:
(¬si−1,k+1−wi ∨ ¬xi ) for all 1 ≤ 2 < n − 1 (F4 )
¬(x1 ∧ x3 ) ∧ ¬(x2 ∧ x3 )
Example 2 (SWC Encoding). Consider the PB-constraint
The sequential weighted counter (SWC) [13] is an en- 3x1 + 2x2 + 4x3 ≤ 5, where w f is a function giving the cor-
coding of normalized PB constraints into formulas in con- responding weights. Then SWC(3, 5, wf) = F1 ∧ F2 ∧ F3 ∧ F4 ,
junctive normal form. It generalizes the sequential counter where
encoding [26] for at-most-k constraints (expressions of the F1 = (¬s1,1 ∨ s2,1 ) ∧ (¬s1,2 ∨ s2,2 ) ∧ (¬s1,3 ∨ s2,3 )∧
form ∑ xi ≤ k, where only k variables can be mapped to >). (¬s1,4 ∨ s2,4 ) ∧ (¬s1,5 ∨ s2,5 )
SWC can also be seen as a variant of a BDD-based encod-
F2 = (¬x1 ∨ s1,1 ) ∧ (¬x1 ∨ s1,2 ) ∧ (¬x1 ∨ s1,3 )∧
ings for monotone predicates [1].
(¬x2 ∨ s2,1 ) ∧ (¬x2 ∨ s2,2 )
The SWC encoding works as follows: given a sequence
of variables x1 , . . . , xn and associated weights w1 , . . . , wn , the F3 = (¬s1,1 ∨ ¬x2 ∨ s2,3 ) ∧ (¬s1,2 ∨ ¬x2 ∨ s2,4 )∧
sequential weighted counter uses the auxiliary propositional (¬s1,3 ∨ ¬x2 ∨ s2,5 )
variables si, j , where 1 ≤ i ≤ n and 1 ≤ j ≤ k. The variable F4 = (¬s1,4 ∨ ¬x2 ) ∧ (¬s2,2 ∨ ¬x3 )
si, j expresses that the sum up to the ith variable is at least j.
Example 1. For instance, consider the PB-constraint Specification
3x1 + 2x2 + 4x3 < 5 and an interpretation I where Given a normalized PB constraint, its SWC encoding is se-
I(x1 ) = >, I(x2 ) = ⊥ and I(x3 ) = >. Then, the following mantically equivalent only with respect to the original vari-
variables are all mapped to > under I: ables, because we use auxiliary variables. Therefore, an in-
terpretation satisfying a PB-constraint must be extended to
s1,1 , s1,2 , s1,3 , s2,1 , s2,2 , s2,3 , s3,1 , s3,2 , s3,3 , a model over the SWC encoding while preserving the truth
value for the original PB variables. Formally, an interpreta-
s4,1 , s4,2 , s4,3 , s4,4 , s4,5 tion J is an extension of the interpretation I, if it agrees with
To get more insight into the encoding process, refer to the truth values for all literals of the form xi for every i ∈ N
Fig. 2, which illustrates the structure as a circuit. (in contrast to variables of the form si, j ).
The specification of encodings consists of two parts: com- 600
pleteness and soundness. Completeness means that when-
ever an interpretation satisfies the PB-constraint, it can
number of solved instances
be extended to an interpretation that satisfies the formula. 550
Soundness means that whenever an interpretation does not
satisfy the PB-constraint, it falsifies the formula: 500
Definition 2 (Encoding Specification). The formula F en-
codes a PB constraint ∑ wi xi ≤ k iff for every interpretation 450
I, we find the following:
• If I satisfies ∑ wi xi ≤ k, then there is an extension J of I
400
such that J is a model of F. pbsolver
• If I does not satisfy ∑ wi xi ≤ k, then I is not a model of F. sat4j
verified
350
Theorem 1 (Main Theorem). The formula SWC(n, k, wf) 0 5000 10000 15000 20000
encodes the ∑ wi xi ≤ k, if the weight function wf gives the timeout in seconds
corresponding weights.
Figure 3: Comparison of the two PB solvers pbsolver and
Proof of the Main Theorem sat4j with our verified checker on selected instances of the
Our proof of the main theorem is based on the informal PB evaluation 2016.
proofs given in [13] and [26], and splits in two essential
components:
1. Soundness Experimental Evaluation
The proof is done by contradiction. It uses the follow- We compare the verified PB solver with the two existing PB
ing intuition: suppose J is the model of SWC encoding. solvers sat4j and pbsolver. pbsolver is a MiniSAT-based
Therefore, its restriction I to the variables xi must also PB solver that combines several different encodings and
be a model of the PB-constraint. Otherwise, it would vi- chooses the best among them [23]. sat4j is a Java library for
olate one of the invariants, springing from the formulas solving Boolean satisfaction and optimization problems and
F1 . . . F4 , which essentially construct the SWC encoding. can also handle PB formulas [4]. For the evaluation, we con-
sidered formulas from the PB competition 2016 that were
2. Completeness
satisfaction problems containing only linear constraints and
To prove completeness we need to show that the model small integers (in total 777 formulas). The experiment was
I of PB formula can be extended a model J of the SWC performed on a cluster of Intel Xeon E5-2670 CPUs with 8
specification. cores and 20 MB level 3 cache that is shared by all cores.
For that we need to take the PB model I and show that we Each program was run on a single core, with a memory limit
can construct an interpretation, that assigns the variables of 2.5GB and a time limit of 6 hours.
si, j to truth values, such that they satisfy the constraints A dedicated normalization procedure was applied before
F1 , . . . , F4 . This can be done using following two prop- running the verified Haskell encoder. If we do not consider
erties: 1. the weighted sum is monotone, as long as he instances that timed out, the time needed for the dedicated
weights are positive, and 2. the extended model J does normalization procedure and our verified transformation is
not change the initial variables xi . in average 140 seconds, whereas the average run time of
For further details see [13]. the SAT solver and the DRAT checker is 624 seconds. The
solver sat4j solved 489 instances, and pbsolver as well as
Integration the verified PB program solved 563 instances, and the re-
Our decision procedure works as follows: It accepts a vari- sulting run times are visualized in Fig. 3. The performance
ant of the input format used in the PB competitions and eval- gap of pbsolver over our verified approach can be explained
uations, where a PB formula has to be given in normal form. that we use a better SAT solver. From the data we conclude
We then compute the SWC encoding, which is done by a that our verified PB solver is efficient enough to be useful in
program that was automatically extracted from the Coq the- practice.
ory. This is done for each occurring PB constraint. The re-
sulting formulas are then syntactically transformed into the Discussion & Conclusion
DIMACS CNF format such that it can be given to the SAT The contribution of this work is the introduction of a routine
solver. for solving PB formulas with the SAT approach, i.e. we en-
More precisely, at this step it is necessary to create unique code PB constraints using a mechanically verified program
variables si, j for each PB constraint and preserve the original and afterwards using a SAT solver that emits unsatisfiability
names of xk variables. Notice that this syntactical transfor- proofs that can be independently checked. For the trans-
mation was not verified using Coq. After running the certi- formation of PB constraints to conjunctive normal form the
fying SAT solver Lingeling, we check unsatisfiability results SWC encoding was used as it is highly-efficient in practice
with drat-trim. and easy to verify. The translation was formalized in the
Coq proof assistant. We claim that we have developed a [6] A. Biere. “Yet another Local Search Solver and Lin-
trustworthy decision procedure for checking satisfiability of geling and Friends Entering the SAT Competition
PB formulas, assuming that the Coq proof assistant as well 2014”. In: ed. by Anton Belov et al. Vol. B-2014-
as the proof checker are correct. 2. Department of Computer Science Series of Pub-
An alternative approach for developing a verified decision lications B. University of Helsinki, Helsinki, Finland,
procedure for the PB problem is to develop specialized rea- 2014, pp. 39–40.
soning procedures, and show them to be correct, or to use [7] Armin Biere et al. “Symbolic Model Checking Us-
a certifying-based approach: both methods seem to be more ing SAT Procedures instead of BDDs”. In: DAC 1999.
difficult than the presented approach. However, a major dis- 1999, pp. 317–320.
advantage of our approach is that some PB problems need [8] Robert Brummayer, Florian Lonsing, and Armin
specialized reasoning procedures, such as cardinality rea- Biere. “Automated Testing and Debugging of SAT
soning such as the Fourier Motzkin procedure, and there are and QBF Solvers”. English. In: SAT 2010. Ed. by
no available certifying SAT solvers that apply these meth- Ofer Strichman and Stefan Szeider. Vol. 6175. LNCS.
ods. Springer Berlin Heidelberg, 2010, pp. 44–57.
Our formalization of the problem contain specifications
and proofs for the SWC and the sequential counter encod- [9] Thierry Coquand and Gérard Huet. “The calculus
ing, which is optimized for cardinality constraints. For the of constructions”. In: Information and Computation
SWC encoding, we splitted the proof into 46 lemmas, for 76.2–3 (1988), pp. 95 –120.
the sequential counter encoding we used 94 lemmas. In to- [10] Niklas Eén and Armin Biere. “Effective Preprocess-
tal, the project consists 3800 lines of code. In the process ing in SAT Through Variable and Clause Elimina-
of formalization and proofs, we did not observe flaws in the tion”. In: SAT 2005. Ed. by Fahiem Bacchus and Toby
published proofs. The system is available at: Walsh. Vol. 3569. LNCS. Heidelberg: Springer, 2005,
https://iccl.inf.tu-dresden.de/web/VPB pp. 61–75.
We believe that the presented approach can easily be adapted [11] Niklas Eén and Niklas Sörensson. “Translating
for several other applications, such as weighted maximum pseudo-Boolean constraints into SAT”. In: JSAT 2
satisfiability, planning, and answer-set programming. These (2006). Ed. by Daniel Le Berre and Laurent Simon,
are widely used to model a large scope of problems, there- pp. 1–26.
fore, the system that we developed might become useful to [12] Peter Großmann et al. “Solving Periodic Event
produce verified proofs in multiple domains. We are also Scheduling Problems with SAT”. In: IEA/AIE 2012.
working on the question how we can express cardinality rea- Ed. by He Jiang et al. Vol. 7345. LNCS. Springer,
soning in the DRAT format to improve the performance of 2012, pp. 166–175. ISBN: 978-3-642-31086-7.
the presented approach. [13] S. Hölldobler, N. Manthey, and P. Steinke. “A Com-
pact Encoding of Pseudo-Boolean Constraints into
Acknowledgements The authors thank the ZIH of TU SAT”. In: Proc. 35th German Conf. on A.I. (KI 2012).
Dresden for providing the computational resources to pro- Ed. by B. Glimm and A. Krüger. Vol. 7526. LNCS.
duce the experimental data for the empirical evaluation. Heidelberg: Springer, 2012, pp. 107–118.
[14] Matti Järvisalo, Armin Biere, and Marijn Heule.
References “Blocked Clause Elimination”. In: TACAS 2010. Ed.
[1] Ignasi Abı́o et al. “BDDs for pseudo-Boolean con- by Javier Esparza and Rupak Majumdar. Vol. 6015.
straints: revisited”. In: SAT 2011. Ed. by Karem A. LNCS. Heidelberg: Springer, 2010, pp. 129–144.
Sakallah and Laurent Simon. Vol. 6695. LNCS. Hei- [15] Matti Järvisalo, Marijn J. H. Heule, and Armin
delberg: Springer, 2011, pp. 61–75. Biere. “Inprocessing rules”. In: IJCAR 2012. Ed.
[2] Roberto Ası́n et al. “Cardinality Networks and Their by Bernhard Gramlich, Dale Miller, and Uli Sat-
Applications”. In: SAT 2009. Ed. by Oliver Kullmann. tler. Vol. 7364. LNCS. Heidelberg: Springer, 2012,
Heidelberg: Springer, 2009, pp. 167–180. pp. 355–370.
[3] Peter Barth. A Davis-Putnam Based Enumeration [16] Henry A. Kautz and Bart Selman. “Planning as Sat-
Algorithm for Linear Pseudo-Boolean Optimization. isfiability”. In: ECAI 1992. Ed. by Bernd Neumann.
Tech. rep. Max Plank Institute for Computer Science, 1992, pp. 359–363.
1995. [17] Oliver Kullmann. “On a Generalization of Extended
[4] Daniel Le Berre and Anne Parrain. “The Sat4j library, Resolution”. In: Discrete Applied Mathematics 96-97
release 2.2”. In: JSAT 7.2-3 (2010), pp. 59–6. URL: (1999), pp. 149–176.
http://jsat.ewi.tudelft.nl/content/ [18] Inês Lynce and João P. Marques-Silva. “Probing-
volume7/JSAT7_4_LeBerre.pdf. Based Preprocessing Techniques for Propositional
[5] Yves Bertot and Pierre Castéran. Interactive Theorem Satisfiability”. In: ICTAI 2003. Sacramento, Califor-
Proving and Program Development, Coq’Art: The nia, USA: IEEE Computer Society, 2003, pp. 105–
Calculus of Inductive Constructions. Springer, 2010. 110. ISBN: 0–7695–2038–3.
[19] Norbert Manthey, Marijn J. H. Heule, and Armin
Biere. “Automated Reencoding of Boolean Formu-
las”. In: HVC 2012. Ed. by Armin Biere, Amir
Nahir, and Tanja Vos. Vol. 7857. LNCS. Heidelberg:
Springer, 2013, pp. 102–117.
[20] Norbert Manthey, Tobias Philipp, and Peter Steinke.
“A More Compact Translation of Pseudo-Boolean
Constraints into CNF Such That Generalized Arc
Consistency Is Maintained”. In: Annual German
Conference on AI (KI 2014). Ed. by Carsten Lutz
and Michael Thielscher. Vol. 8736. LNCS. Springer,
2014, pp. 123–134.
[21] David E. Muller and Franco P. Preparata. “Bounds to
Complexities of Networks for Sorting and for Switch-
ing”. In: Journal of the ACM 22.2 (1975), pp. 195–
201.
[22] Yacine Boufkhad Olivier Bailleux and Olivier Rous-
sel. “New Encodings of Pseudo-Boolean Constraints
into CNF”. In: SAT 2009. Ed. by Oliver Kullmann.
Heidelberg: Springer, 2009, pp. 181–194.
[23] Tobias Philipp and Peter Steinke. “PBLib – A C++
Toolkit for Encoding Pseudo-Boolean Constraints
into CNF”. In: SAT 2015. 2015.
[24] Jussi Rintanen. “Compact Representation of Sets of
Binary Constraints”. In: ECAI 2006. Ed. by Gerhard
Brewka et al. Vol. 141. Frontiers in Artificial Intel-
ligence and Applications. IOS Press, 2006, pp. 143–
147.
[25] Jussi Rintanen. “Engineering Efficient Planners with
SAT”. In: ECAI 2012. Ed. by Luc De Raedt et al.
Vol. 242. Frontiers in Artificial Intelligence and Ap-
plications. IOS Press, 2012, pp. 684–689.
[26] Carsten Sinz. “Towards an Optimal CNF Encoding
of Boolean Cardinality Constraints”. In: ed. by Peter
van Beek. Vol. 3709. LNCS. Springer, 2005, pp. 827–
831.
[27] Sathiamoorthy Subbarayan and Dhiraj K. Prad-
han. “NiVER: Non-increasing Variable Elimination
Resolution for Preprocessing SAT Instances”. In:
SAT 2004. Ed. by Holger H. Hoos and David G.
Mitchell. Vol. 3542. LNCS. Heidelberg: Springer,
2005, pp. 276–291.
[28] G. S. Tseitin. “On the complexity of derivations in
the propositional calculus”. In: Studies in Mathemat-
ics and Mathematical Logic Part II (1968), pp. 115–
125.
[29] Nathan Wetzler, Marijn J.H. Heule, and Warren A.
Hunt. “DRAT-trim: Efficient Checking and Trimming
Using Expressive Clausal Proofs”. In: SAT 2014. Ed.
by Carsten Sinz and Uwe Egly. Vol. 8561. LNCS.
Springer, 2014, pp. 422–429.