=Paper=
{{Paper
|id=Vol-1335/wlp2014_paper2
|storemode=property
|title=Describing and Measuring the Complexity of
SAT encodings for Constraint Programs
|pdfUrl=https://ceur-ws.org/Vol-1335/wlp2014_paper2.pdf
|volume=Vol-1335
|dblpUrl=https://dblp.org/rec/conf/wlp/BauW14
}}
==Describing and Measuring the Complexity of
SAT encodings for Constraint Programs==
https://ceur-ws.org/Vol-1335/wlp2014_paper2.pdf
Describing and Measuring the Complexity of
SAT encodings for Constraint Programs
Alexander Bau? and Johannes Waldmann
HTWK Leipzig, Fakultät IMN, 04277 Leipzig, Germany
abau|waldmann@imn.htwk-leipzig.de
Abstract. The CO4 language is a Haskell-like language for specifying
constraint systems over structured finite domains. A CO4 constraint sys-
tem is solved by an automatic transformation into a satisfiability problem
in propositional logic that is handed to an external SAT solver.
We investigate the problem of predicting the size of formulas produced by
the CO4 compiler. The goal is to help the programmer in understanding
the resource consumption of CO4 on his program. We present a basic cost
model, with some experimental data, and discuss ongoing work towards
static analysis. It turns out that analysis steps will use constraint systems
as well.
1 Introduction
CO4 is a constraint programming language that allows to write a constraint
problem as declarative specification. The CO4 compiler solves it by transforming
the constraint to a propositional satisfiability problem, so that a SAT solver
can be applied. Syntactically, the language is a subset of the purely functional
programming language Haskell [3] that includes user-defined algebraic data types
and recursive functions defined by pattern matching, as well as higher-order
polymorphic types.
In CO4 , a constraint system over elements of set U is specified by a parametrized
predicate constraint : P × U → Bool, where P denotes the parameter domain.
Thus, constraint does not denote a single constraint, but a family of con-
straints. For a given constraint and parameter p ∈ P , u ∈ U is a solution if
constraint (p, u) = True.
For the CO4 compiler to generate a propositional encoding, the input constraint
is transformed into an abstract program constraint’ that operates on abstract
values. An abstract value represents an undetermined value of the input program
by encoding the constructor’s index using propositional formulas. Evaluating the
abstract program generates the final formula that is passed to the external SAT
solver.
It is desirable to predict the runtime of the SAT solver for a generated propo-
sitional encoding. Such a prediction is hard because as it depends on a lot of
design and implementation decisions of the SAT solver. Therefore we take the
?
This author is supported by ESF grant 100088525
size of the SAT encoding as a reasonable indicator for its hardness. To esti-
mate the size of the encoding, we introduce a cost model for abstract values
and abstract programs. This cost model captures two important facts: the size
of intermediate abstract values and the costs to evaluate them. Especially the
evaluation of case distinctions on abstract values is not obvious, and often they
cannot be evaluated in a straightforward manner.
This paper has three parts. The first part illustrates the syntax and seman-
tics of CO4 (Section 2) and gives an overview on of the propositional encoding
(Section 3). This is a summary of material that has already been published[1].
The second part presents current work on cost analysis: in Section 4 we present
our cost model, and in Section 5 we analyze the cost of the merge operation,
which is a basic operator in our translation scheme. Section 6 illustrates how the
current CO4 implementation measures concrete costs of SAT-compiled function
calls. The third part outlines future work in static analysis of CO4 programs.
Section 7 describes moded types and their inference, which will allow a more effi-
cient propositional encoding of case distinctions. Section 8 describes an approach
to bound function costs by resource types.
2 Syntax and Semantics of CO4
Syntactically, CO4 is a subset of Haskell. Domains are specified by algebraic data
types (ADT), where constructors enumerate the values of the type.
1 data Bool = False | True
2 data Color = Red | Green | Blue
3 data Monochrome = Black | White
4 data Pixel = Colored Color | Background Monochrome
CO4 supports recursive ADTs as well, but recursions must be restricted while
generating a propositional encoding. We do not deal with recursions in the scope
of this paper.
A constructor may be parametrized either by types or type variables.
1 data Pair a b = Pair a b
2 data Either a b = Left a | Right b
Inspecting the constructor of a value d of some ADT is done by a case
distinction on d (the discriminant of the case distinction):
1 case color of Blue -> True
2 otherwise -> False
Case distinctions provides conditional branching of the control-flow. Other
kinds of expressions in CO4 are constructor calls, applications, abstractions and
local bindings. CO4 provides restricted support of higher-order, polymorphic
functions. Besides type definitions, constraint systems in CO4 contain global
function bindings with constraint being the top-level function:
1 data Bool = False | True
2 data Color = Red | Green | Blue
3 data Monochrome = Black | White
4 data Pixel = Colored Color | Background Monochrome
5
6 constraint :: Bool -> Pixel -> Bool
7 constraint p u = case p of
8 False -> case u of Background m -> True
9 otherwise -> False
10 True -> isBlue u
11
12 isBlue :: Pixel -> Bool
13 isBlue u = case u of
14 Colored color -> case color of Blue -> True
15 otherwise -> False
16 Background m -> False
Listing 1.1. A trivial constraint over pixels
Semantically, a constraint system in CO4 over elements of set U is a binary
predicate constraint : P × U → Bool on U and some parameter domain P . In
Listing 1.1, P = Bool and U = Pixel.
For a given parameter p ∈ P , u ∈ U is a solution if constraint (p, u) = True.
One advantage of specifying constraint systems in a functional language like
CO4 is that a solution can be tested against the constraint simply by evaluat-
ing constraint (p, u). Note that CO4 expressions are evaluated strictly, while
Haskell features a non-strict evaluation strategy.
3 Propositional Encoding of CO4 constraints
In the following, we call the source constraint a concrete program. Concrete
programs operate on concrete values, e.g., the concrete program in Listing 1.1
operates on concrete values like False, White or Colored Red.
To find a solution u ∈ U for a constraint constraint : P × U → Bool and a
parameter p ∈ P , CO4 performs the following steps:
1. The concrete program is transformed into an abstract program. An abstract
program doesn’t operate on concrete values, but on abstract values.
2. Evaluating the abstract program for an abstract value that represents pa-
rameter p gives a formula f ∈ F in propositional logic.
3. An external SAT solver is called to find a satisfying assignment σ ∈ Σ for f .
4. If there is a satisfying assignment, the solution u ∈ U is constructed from
σ. Optionally, testing whether constraint p u = True ensures that there
are no implementation errors. This check must always succeed if there is a
solution.
In the following we briefly illustrate the first two steps of this process. Firstly,
an abstract program is generated from a given concrete program. This transfor-
mation not only modifies the program structure, the domain is changed as well.
Data Transformation An abstract program is an untyped, first-order and im-
perative program on abstract values.
Definition 1. Assume F being the set of propositional formulas. Then, the set
of abstract values A is the smallest set with A = F∗ × A∗ where F∗ denotes the
→
− −
set of sequences with elements from F. An abstract value a ∈ A is a tuple ( f , →
a)
→
− →
−
of flags f and arguments a .
An abstract value a ∈ A represents a (maybe unknown) value of a concrete
type T . The flags of an abstract value a ∈ A encode the indices of T ’s constructors
in binary code using propositional formulas.
Example 1. For an abstract value a1 ∈ A to represent a value of the ADT data
Color = Red | Green | Blue | Purple it must contain two flags f1 , f2 ∈ F
because Color has four constructors. Thus, a1 = ((f1 , f2 ), ()). a1 has no argu-
ments because none of Color’s constructors has any arguments.
Consider an ADT data Maybe a = Nothing | Just a and an abstract value
a2 ∈ A that is supposed to represent a value of type Maybe Color. As Maybe con-
sists of two constructors, one flag f3 ∈ F is needed to discriminate both. Thus,
(f3 , a1 ) is a proper value for a2 . Note that a2 has a single argument a1 that
encodes the constructor argument of type Color of Maybe’s Just constructor.
As the flags of an abstract value a ∈ A may contain propositional variables,
a can be decoded to different values according to the Boolean values that are
assigned to these variables. By decodeT : A ×Σ → T we denote a mapping from
abstract values and propositional assignments Σ to concrete values.
If the flags of an abstract value a ∈ A don’t contain propositional variables,
then the flags of a index a particular constructor and a can only be decoded to a
single concrete value. By encodeT : T → A we denote a mapping from concrete
values to abstract values that represent a fixed value.
Example 2. Recall the ADTs defined in Example 1 and assume the flags of an
abstract value reference a constructor’s index using binary code where the first
flag encodes the most significant bit. Then:
encodeColor (Blue) = ((True, False), ())
encodeMaybe Color (Just Blue) = (True, ((True, False), ()))
As we’ve omitted details about abstract values we don’t provide definitions
for encode and decode.
Program Transformation The program structure of abstract programs resem-
bles the structure of their concrete counterparts. The most important difference
concerns case distinctions: while concrete values may be examined by matching
on their constructor, this is often not possible for abstract values. That’s be-
cause an abstract value’s flags may contain propositional variables. Therefore, it
is undetermined which constructor is indexed by the flags and there is no way
to known which branch to evaluate. Thus, all branches must be evaluated and
their result is merged according to the discriminant of the case distinction.
Example 3. The following case distinction matches on a Boolean value x in a
concrete program:
r = case x of { False -> g ; True -> h }
In the abstract counterpart of this expression, the abstract values g 0 and h0 of
both branches are evaluated and merged according to x
r0 = let _1 = g 0
_2 = h0
in mergex0 (_1,_2)
where r0 (resp. x0 , g 0 , h0 ) denote the abstract counterpart of r (resp. x, g, h).
The function mergex : A∗ → A encodes a case distinction on a value x ∈ A
using the flags of x and the abstract values of all evaluated branches. We don’t
give a definition for merge, but illustrate its semantics by the following example.
Example 4. Recall the case distinction in Example 3 and assume r0 (resp. x0 , g 0 , h0 )
denotes the abstract counterpart of r (resp. x, g, h). The following two clauses
are emitted when evaluating mergex0 (g 0 , h0 ):
(x0 ≡ encodeBool (False) =⇒ r0 ≡ g 0 )
∧ (x0 ≡ encodeBool (True) =⇒ r0 ≡ h0 )
Informally, both clauses encode the semantics of the original case distinction
in terms of abstract values: r0 equals g 0 if x0 equals encodeBool (False), otherwise
r0 equals h0 .
However, if none of the flags of an abstract value contain any propositional
variables, then the constructor that is indexed by these flags can be determined
and the associated branch can be evaluated. In this case it is not necessary to
evaluate the other branches.
Evaluation of Abstract Programs The constraint : P × U → Bool function in
a concrete program has a counterpart constraint’ : A × A → A in the abstract
program of the same arity. Evaluating constraint’ p0 u0 on
– p0 = encodeP (p) for some parameter p ∈ P , and
– u0 ∈ A, which represents a undetermined value in U ,
gives a value a ∈ A that represents a Boolean value, i.e., a contains a single
flag f ∈ F. Solving f using an external SAT solver gives a satisfying assignment
σ ∈ Σ for all variables in f if there is such an assignment. The final solution
u ∈ U can be constructed by decodeU (u0 , σ).
We refer to [1] for more technical details on the transformation process.
4 Cost Model
We illustrate an approach for formalizing the costs associated with a function
in a CO4 program. For readability we stick to unary functions and omit details
about functions of higher arities.
We measure the cost of a function f : A → B in a concrete program by
analyzing its counter part f 0 : A → A in the corresponding abstract program.
The costs of f 0 depend on the size of its argument. Thus, we introduce a function
size : A → N to measure the size of an abstract value.
Example 5. There are at least two naive definitions for size: one that counts the
number of nested abstract values
n
→
− X
size1 ( f , (a1 , . . . , an )) = 1 + size1 (ai )
i=1
and one that counts the number of flags in an abstract value
n
X
size2 ((f1 , . . . , fm ), (a1 , . . . , an )) = m + size2 (ai )
i=1
Fixing a particular implementation for size, the cost of the abstract function
f 0 is described by a pair of functions sf , cf : N → N.
Definition 2. sf (n) gives the maximal output size for all arguments of f 0 with
size n or smaller:
sf (n) = max{size(f (encodeA (x))) | x ∈ A ∧ size(encodeA (x)) ≤ n}
Whereas sf quantifies the size of a function’s result, cf measures the evalu-
ation costs of f 0 .
Definition 3. cf (n) gives the evaluation costs for all arguments of f 0 with size
n or smaller
cf (n) = max{work(f, encodeA (x)) | x ∈ A ∧ size(encodeA (x)) ≤ n}
where work(f, x) equals the cost of evaluating f 0 (encodeA (x)) in the abstract
program.
We can instantiate this scheme in several ways: for example, work(f, x) could
give the number of propositional variables or clauses that are allocated while
computing the abstract value f 0 (encodeA (x)). Other techniques may include ad-
ditional characteristics about the propositional encoding, like the number of
literals or the depth of the formula.
5 Cost of merge
Example 4 illustrated the semantics of the merge operation on abstract values.
Now we quantify the cost of merge in terms of the cost model in Section 4.
Assume the following case distinction with n branches b1 , . . . , bn in a function
f:
f (x) = case x of C1 -> b1
...
Cn -> bn
Listing 1.2. A case distinction over n branches
where f 0 : A → A denotes the abstract counterpart of f . In order to evalu-
ate f 0 (x0 ) for some abstract argument x0 ∈ A we need to evaluate all abstract
branches b0i ∈ A for i ∈ [1, n] and merge the results by mergex0 (b01 , . . . , b0n ). We
denote the result of this merge by r0 ∈ A.
A first cost measure determines the numbers of variables that are needed to
represent the result of an application of merge (variable-cost).
Definition 4. workV (f, x) denotes the variable-cost of function f in Listing 1.2
and equals the maximum number of flags in the branches, i.e., if mi denotes the
number of flags in branch b0i for i ∈ [1, n], then
workV (f, x) = max{mi | 1 ≤ i ≤ n}
As the result of f 0 (x) must equal one of the branches b0i (c.f. Example 4) it
is reasonable for workV to assume that r0 must consist of the maximum number
of flags that are present in the abstract branches b0i ∈ A for 1 ≤ i ≤ n.
Furthermore, we define the clause-cost of an application of merge. Example 4
illustrated that the flags in a result of merge encode the case distinction in
terms of abstract values. The clause-costs represent the number of clauses in a
propositional formula that are needed to encode a case distinction.
Definition 5. workC (f, x) denotes the clause-cost of function f in Listing 1.2
where n denotes the number of branches:
workC (f, x) = 2 ∗ workV (f, x) ∗ n
workC is reasonable because two clauses are emitted for each of the workV (f, x)
flags in r0 and each of the n branches.
6 Profiling CO4
In the following we compare the profiling output of CO4 for some examples and
show the relation to the previously defined cost-model.
The first example illustrates the difference between the cost of evaluating a
concrete program and an abstract program.
1 data Bool = False | True deriving Show
2 data T = T1 | T2 | T3 deriving Show
3
4 g :: T -> Bool
5 g t = case t of T1 -> True
6 T2 -> False
7 T3 -> False
8
9 f1 :: Bool -> Bool
10 f1 b = case b of False -> g T1
11 True -> g T2
12
13 f2 :: Bool -> Bool
14 f2 b = g (case b of False -> T1
15 True -> T2)
Listing 1.3. Profiling two semantically equivalent functions
Listing 1.3 defines two functions f1,f2 with the same concrete semantics.
Assume f1’ (resp. f2’,g’) being the abstract counterpart of f1 (resp. f2,g).
Further assume that b ∈ A is an abstract value that represents an undetermined
value of type Bool. Then, evaluating f1’ b gives
("f1’", {numCalls = 1, numVariables = 1, numClauses = 4})
("g’", {numCalls = 2, numVariables = 0, numClauses = 0})
g’ does not allocate any variables nor clauses as its argument is constant in
both calls g T1 and g T2 in the concrete program. Thus, the case distinction in
g’ can be evaluated straightforwardly without applying merge.
f1’ is called once and allocates one variable (resp. four clauses). That matches
the workV (resp. workC ) cost function, because
– workV (f1, b) = max{1, 1} = 1 as each branch in f1’ is represented by an
abstract value with one flag (because Bool has two constructors)
– workC (f1, b) = 2 ∗ workV (f1, b) ∗ 2 = 4 as there are n = 2 branches in f1’
On the other hand, evaluating f2’ b gives
("f2’", {numCalls = 1, numVariables = 2, numClauses = 8})
("g’", {numCalls = 1, numVariables = 1, numClauses = 6})
Again, the profiling information matches with the cost functions workV and
workC defined in Section 5, because
– workV (f2, b) = max{2, 2} = 2 as each branch in f2’ is represented by an
abstract value with two flags (because T has three constructors)
– workC (f2, b) = 2 ∗ workV (f2, b) ∗ 2 = 8 as there are n = 2 branches in f2’
– workV (g, t) = max{1, 1, 1} = 1 as each branch in g’ is represented by an
abstract value with one flag (because Bool has two constructors)
– workC (g, t) = 2 ∗ workV (g, t) ∗ 3 = 6 as there are n = 3 branches in g’
Note that f2’ allocates more variables than f1’ because it merges branches
of type T, which has more constructors than Bool. In the second case, g’ is only
called once, but this time with an unknown argument: its argument indirectly
depends on the unknown b. Thus, g’ allocates variables and emits clauses.
We give a more complex example: CO4 has been applied to problems of
termination analysis of term rewriting systems. One exemplary problem is the
specification of a lexicographic path order (LPO) that proves the termination of
a given term rewriting system1 .
Profiling (inner-under):
("constraint’", {numCalls = 1, numVariables = 160, numClauses = 514})
("allHOInst’", {numCalls = 1, numVariables = 160, numClauses = 514})
("mapHOInst’", {numCalls = 4, numVariables = 157, numClauses = 506})
("globalLam’", {numCalls = 3, numVariables = 157, numClauses = 506})
("globalLamSat’", {numCalls = 3, numVariables = 157, numClauses = 506})
("lpo’", {numCalls = 41, numVariables = 154, numClauses = 500})
...
Listing 1.4. Exemplary inner-under-profiling
Listing 1.4 shows the inner-under-profiling for a LPO constraint. For each
function f in the abstract program, inner-under-profiling associates the number
of variables and clauses to f that has been allocated by f and by all func-
tions transitively called in f . Unsurprisingly, constraint’ allocates the most
resources according to inner-under-profiling as it is the top-level function in ev-
ery abstract program.
Profiling (inner):
("gtNat’", {numCalls = 9, numVariables = 36, numClauses = 171})
("lpo’", {numCalls = 41, numVariables = 30, numClauses = 92})
("ordNat’", {numCalls = 9, numVariables = 27, numClauses = 63})
("eqNat’", {numCalls = 19, numVariables = 27, numClauses = 99})
("and2’", {numCalls = 26, numVariables = 20, numClauses = 44})
("eqOrder’", {numCalls = 31, numVariables = 18, numClauses = 40})
...
Listing 1.5. Exemplary under-profiling
Listing 1.5 shows the under-profiling for a LPO constraint. For each function
f in the abstract program, under-profiling only associates the number of variables
and clauses to f that has been allocated by f . Listing 1.5 shows that for the
LPO constraint the abstract function gtNat’ allocates the most propositional
variables.
CO4 also provides information about the number of variables and clauses
allocated in the abstract program as a whole:
#variables: 167, #clauses: 517, #literals: 1365
1
available at https://github.com/apunktbau/co4/blob/master/test/CO4/
Example/LPO.hs
We give one more example: Listing 1.6 shows the profiling data for a CO4
specification of the n-queens problem (with n = 8)2 .
Profiling (inner-under):
("constraint’", {numCalls = 1, numVariables = 2324, numClauses = 6447})
("allSafe’", {numCalls = 9, numVariables = 2251, numClauses = 6237})
("safe’", {numCalls = 36, numVariables = 2244, numClauses = 6217})
("noAttack’", {numCalls = 28, numVariables = 2216, numClauses = 6140})
("equal’", {numCalls = 717, numVariables = 1724, numClauses = 5100})
("noDiagon’", {numCalls = 28, numVariables = 1488, numClauses = 4012})
("noStraight’", {numCalls = 28, numVariables = 700, numClauses = 2044})
...
Profiling (inner):
("equal’", {numCalls = 717, numVariables = 1724, numClauses = 5100})
("add’", {numCalls = 359, numVariables = 352, numClauses = 704})
("and2’", {numCalls = 101, numVariables = 100, numClauses = 291})
("not’", {numCalls = 84, numVariables = 84, numClauses = 168})
("less’", {numCalls = 65, numVariables = 64, numClauses = 184})
#variables: 2397, #clauses: 6522, #literals: 16697
Listing 1.6. Exemplary profiling for the n-queens problem (with n = 8)
Here, inner-profiling reveals that the equal’ function allocates the most re-
sources. This is reasonable because the n-queens constraint pair-wisely compares
the position of all queens in order to exclude all possibilities for two queens to
attack each other.
7 Moded Types and Mode Inference
For the future work on CO4 , we plan to develop a mode inference system that
allows the generation of propositional encodings with fewer variables and clauses.
That is desirable as smaller formulas are often solved in less time by a SAT solver.
Moded types allow the differentiation between expressions that are constant
during abstract evaluation and expressions that are not. This information would
allow the CO4 compiler to determine case distinctions that have a constant
discriminant, i.e., that can be evaluated during abstract evaluation without al-
locating any propositional variables.
In this context, a mode is either ! or ?. Mode ! states that the constructor
of a value is known during abstract evaluation, while mode ? states that the
constructor of a value is not known during abstract evaluation. A moded type is
a type that has been annotated by modes. For example, List! Bool? denotes a
list type, where each of list constructor is known, but each element of type Bool
has an unknown constructor. Thus, such a type encodes a list of known length
with unknown Boolean elements.
2
available at https://github.com/apunktbau/co4/blob/master/test/CO4/
Example/QueensSelfContained.hs
We consider a moded program to be a typed program where each type is
annotated by modes. For a moded program to be dynamically well-moded, it
is required that the constructor of all case distinctions’ discriminants must be
constant that have mode !, i.e., their flags are constant.
We plan to develop a static mode analysis as a safe approximation for dy-
namically well-moded programs. One possible approach for a mode inference
algorithm is the construction of a Boolean constraint (because there are two
different modes) that can be solved by a SAT solver.
A similar approach has been successfully applied to infer modes in for the
Mercury language[4].
8 Resource Types and Resource Inference
Mode analysis allows a more strict analysis on the estimated cost for a CO4
constraint system.
A possible approach to predict the resource cost is to annotate each function
in a CO4 constraint with a resource type, where a resource type for function
f according to the cost model introduced in Section 4 is a pair of functions
sf , cf : N → N.
A dynamically well-resource-typed program is a program where each function
f has a resource type annotation, so that for each call of f with argument x the
actual cost work(f, encode(x)) is less or equal to cf (size(encode(x))) for some
cost function work (see Section 4).
A resource-typed program is considered statically well-typed, if all resource
annotations are consistent with some sound set of rules for cost of case distinc-
tions, merge operations and function compositions.
These rules should guarantee that the static resource type is a safe approxi-
mation for actual costs. We are especially interested in polynomial upper bounds.
Related work consists of amortized resource analysis in Resource Aware ML
(RAML)[2], where polynomial potential functions are used as costs functions.
The coefficients for these polynomial are determined by a constraint system.
We want to emphasize again that this approach is ongoing work and there
are currently no results nor experimental data to verify it. We plan to extend
this approach into a reasonable formalism to capture the resource constraints of
CO4 programs in order to estimate the size of the propositional encodings.
References
1. Alexander Bau and Johannes Waldmann. Propositional Encoding of Constraints
over Tree-Shaped Data. In 22nd International Workshop on Functional and (Con-
straint) Logic Programming, 2013.
2. Jan Hoffmann, Klaus Aehlig, and Martin Hofmann. Multivariate Amortized Re-
source Analysis. ACM Trans. Program. Lang. Syst., 34(3):14:1–14:62, November
2012.
3. Simon Peyton Jones, editor. Haskell 98 Language and Libraries, The Revised Report.
Cambridge University Press, 2003.
4. David Overton, Zoltan Somogyi, and Peter J. Stuckey. Constraint-based mode
analysis of mercury. In PPDP, pages 109–120, 2002.