Solution Counting for CSP and SAT with Large Tree-Width
Рассмотрена проблема подсчета количества решений задачи совместимости ограничений (Constraint Satisfaction Problem). Для ее решения был адаптирован метод обратного прослеживания с ацикличным представлением графа ограничений (Backtracking with Tree-Decomposition). Предложен точный алгоритм, сложность...
Saved in:
| Published in: | Управляющие системы и машины |
|---|---|
| Date: | 2011 |
| Main Authors: | , , |
| Format: | Article |
| Language: | English |
| Published: |
Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України
2011
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/82919 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Solution Counting for CSP and SAT with Large Tree-Width / A. Favier, S. de Givry, Ph. Jégou // Управляющие системы и машины. — 2011. — № 2. — С. 4-13, 70. — Бібліогр.: 36 назв. — англ. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1859633660017246208 |
|---|---|
| author | Favier, A. de Givry, S. Jégou, P. |
| author_facet | Favier, A. de Givry, S. Jégou, P. |
| citation_txt | Solution Counting for CSP and SAT with Large Tree-Width / A. Favier, S. de Givry, Ph. Jégou // Управляющие системы и машины. — 2011. — № 2. — С. 4-13, 70. — Бібліогр.: 36 назв. — англ. |
| collection | DSpace DC |
| container_title | Управляющие системы и машины |
| description | Рассмотрена проблема подсчета количества решений задачи совместимости ограничений (Constraint Satisfaction Problem). Для ее решения был адаптирован метод обратного прослеживания с ацикличным представлением графа ограничений (Backtracking with Tree-Decomposition). Предложен точный алгоритм, сложность которого экспоненциально зависит от ширины дерева, и приближенный алгоритм, экспоненциально зависящий от размера максимальной клики.
The problem of counting the number of solutions of a CSP is considered. For solving the problem the Backtracking with a Tree-Decomposition method was adapted. The exact algorithm is suggested which has the worst-time complexity exponential in a tree width, as well as iterative algorithm that has computational complexity exponential in a maximum clique size.
Розглянуто проблему підрахунку кількості розв’язків задачі сумісності обмежень (Constraint Satisfaction Problem). Для її розв’язку було адаптовано метод зворотного простеження з ациклічним поданням графа обмежень (Backtracking with Tree-Decomposition). Запропоновано точний алгоритм, складність якого експоненційно залежить від ширини дерева, і наближений алгоритм, експоненційно залежний від розміру максимальної кліки.
|
| first_indexed | 2025-12-07T13:13:54Z |
| format | Article |
| fulltext |
4 УСиМ, 2011, № 2
UDC 519.157
A. Favier, S. de Givry, Ph. Jégou
Solution Counting for CSP and SAT with Large Tree-Width
Рассмотрена проблема подсчета количества решений задачи совместимости ограничений (Constraint Satisfaction Problem). Для
ее решения был адаптирован метод обратного прослеживания с ацикличным представлением графа ограничений (Backtracking
with Tree-Decomposition). Предложен точный алгоритм, сложность которого экспоненциально зависит от ширины дерева, и
приближенный алгоритм, экспоненциально зависящий от размера максимальной клики.
The problem of counting the number of solutions of a CSP is considered. For solving the problem the Backtracking with a Tree-
Decomposition method was adapted. The exact algorithm is suggested which has the worst-time complexity exponential in a tree width,
as well as iterative algorithm that has computational complexity exponential in a maximum clique size.
Розглянуто проблему підрахунку кількості розв’язків задачі сумісності обмежень (Constraint Satisfaction Problem). Для її
розв’язку було адаптовано метод зворотного простеження з ациклічним поданням графа обмежень (Backtracking with Tree-
Decomposition). Запропоновано точний алгоритм, складність якого експоненційно залежить від ширини дерева, і наближений
алгоритм, експоненційно залежний від розміру максимальної кліки.
Abstract
This paper deals with the challenging problem
of counting the number of solutions of a CSP, de-
noted #CSP. Recent progress has been made using
search methods, such as Backtracking with Tree-
Decomposition (BTD) [Jégou and Terrioux, 2003],
which exploit the constraint graph structure in or-
der to solve CSPs. We propose to adapt BTD for
solving the #CSP problem. The resulting exact
counting method has a worst-case time complex-
ity exponential in a specific graph parameter,
called tree-width. For problems with a sparse con-
straint graph but a large tree-width, we propose an
iterative method which approximates the number
of solutions by solving a partition of the set of
constraints into a collection of partial chordal sub-
graphs. Its time complexity is exponential in the
maximum clique size – the clique number – of the
original problem, which can be much smaller than
its tree-width. Experiments on CSP and SAT
benchmarks show the practical efficiency of our
proposed approaches1.
1. Introduction
The Constraint Satisfaction Problem (CSP) for-
malism offers a powerful framework for repre-
senting and solving efficiently many problems.
Finding a solution is NP-complete. A more diffi-
cult problem consists in counting the number of
Keywords: solution counting, constraint satisfaction prob-
lem, dynamic programming, approximate counting, chordal
graph, graph coloring.
1A preliminary version appears in [Favier et al., 2009].
solutions. This problem, denoted #CSP, is known
to be #P-complete [Valiant, 1979]. This problem
has numerous applications in computer science,
particularly in AI, e.g. in approximate reasoning
[Roth, 1996], in belief revision [Darwiche, 2001],
in diagnosis [Kumar, 2002], in guiding backtrack
search heuristics to find solutions to CSPs
[Zanarini and Pesant, 2009], and in other domains
outside computer science such as in statistical
physics [Burton and Steif, 1994] or in computa-
tional biology for protein structure prediction
[Mann et al., 2007].
In the literature, two principal classes of ap-
proaches have been proposed. In the first class,
methods find exactly the number of solutions in
exponential time. In the second class, methods
give approximations in a reasonable time. For the
first class, a natural approach consists in extend-
ing classical search algorithms such as FC or
MAC in order to enumerate all solutions. But the
more solutions there are, the longer it takes to
enumerate them.
Here, we are interested in search methods that
exploit the problem structure, providing time and
space complexity bounds. This is the case for the
d-DNNF compiler c2d [Darwiche, 2004] and
AND/OR graph search [Dechter and Mateescu,
2004, 2007] for counting. We propose to adapt
Backtracking with Tree-Decomposition (BTD)
[Jégou and Terrioux, 2003] to #CSP. This method
was initially proposed for solving structured
CSPs. Our modifications to BTD, resulting in an
УСиМ, 2011, № 2 5
algorithm called #BTD, are similar to what has
been done in the AND/OR context [Dechter and
Mateescu, 2004, 2007], except that #BTD is based
on a cluster tree-decomposition instead of a
pseudo-tree, which naturally enables #BTD to ex-
ploit dynamic variable orderings inside clusters
whereas AND/OR search uses a static ordering.
Most of the recent work on counting has been
realized on a specific case of #CSP called #SAT,
the model counting problem associated with SAT
[Valiant, 1979]. Exact methods for #SAT extend
systematic SAT solvers, adding component analy-
sis [Bayardo and Pehoushek, 2000] (Relsat solver)
and caching [Sang et al., 2004] (Cachet, further
improved by sharpSAT [Thurley, 2006] ) for effi-
ciency purposes.
Approaches using approximations estimate the
number of solutions. They propose poly-time or
exponential time algorithms which should offer
reasonably good approximations of the number of
solutions, with theoretical guarantees about the
quality of the approximation, or not. Most of the
work has been done by sampling either the origi-
nal OR search space [Wei and Selman, 2005,
Gomes et al., 2007a, Gogate and Dechter, 2007,
Kroc et al., 2008], or the original AND/OR search
space [Gogate and Dechter, 2008]. All these
methods except that in [Gogate and Dechter,
2008] provide a lower bound on the number of
solutions with a high-confidence interval obtained
by randomly assigning variables until solutions
are found. A possible drawback of these ap-
proaches is that they might find no solution within
a given time limit due to inconsistent partial as-
signments. For large and complex problems, this
results in zero lower bounds or it requires time-
consuming parameter (e.g. sample size) tuning in
order to avoid this problem. Another solution is to
rely on a complete search method, withdrawing
any time limit, in order to check whether every
variable assignment made during the sampling
process is globally consistent or not and then
backtrack as done in [Gogate and Dechter, 2007].
Another approach involves reducing the search
space by adding streamlining XOR constraints
[Gomes et al., 2006, 2007b]. However, it does not
guarantee that the resulting problem is easier to
solve. A good overview of state-of-the-art exact
and approximate counting methods for #SAT is
given in [Gomes et al., 2009].
In this paper, we propose to relax the problem,
by partitioning the set of constraints into a collec-
tion of structured chordal subproblems. Each sub-
problem is then solved using #BTD. Finally, an
approximate number of solutions on the whole pro-
blem is obtained by combining the results of each
subproblem. The resulting approximate method is
called Approx#BTD. The task of counting the
number of solutions of each subproblem should be
relatively easy if the original instance has a sparse
graph. In fact, it depends on the tree-width of the
subproblems, which is bounded by the maximum
clique size of the original instance called the clique
number. In the case of a sparse graph, we expect
this number to be small. This also forbids using
our approach for CSPs with global constraints (i.e.
having a complete constraint graph) or proposi-
tional CNF formulae with very large clauses.
Approx#BTD gives also a trivial upper bound on
the number of solutions.
Other relaxation-based counting methods have
been tried in the literature such as mini-bucket
elimination and iterative join-graph propagation
[Kask et al., 2004], or in the related context of
Bayesian inference, iterative belief propagation
and the edge deletion framework [Choi and Dar-
wiche, 2006]2. These approaches do not exploit
the local structure of the instances as it is done by
search methods such as #BTD , thanks to local
consistency and dynamic variable ordering.
In the next section, we introduce notation and
the notion of a tree-decomposition. Section 3 de-
scribes #BTD for exact counting and Section 4
presents Approx#BTD for approximate counting.
Experimental results are given in Section 5, then
we conclude.
2. Preliminaries
A Constraint Satisfaction Problem [Montanari,
1974] is a quadruplet = ( , , , )X D C R . X is a set
2It starts by solving an initial polytree-structured sub-
problem, further augmented by progressively recovering some
edges, until the whole problem is solved. Approx#BTD starts
directly with a possibly larger chordal subproblem.
6 УСиМ, 2011, № 2
of n variables with finite domains D. The domain
of variable xi X with [1, ]i n is denoted xi
d D .
The maximum domain size is [1, ]= | |max i n xi
d d .
C is a set of m constraints. Each constraint c C
is a set
1
{ , , }c ck
x x X of variables. The prob-
lem is called a binary CSP if all the constraints
have 2k . A relation cr R is associated with
each constraint c such that cr represents the set of
allowed tuples over
1c ck
x xd d for the assignment
of the variables in c. Note that we can also define
constraints by using functions or predicates for
instance. An assignment of 1= { , , }kY x x X is
a tuple 1= ( , , )kv v from
1x xk
d d . We note
the assignment 1( , , )kv v in the more meaningful
form 1 1( , , )k kx v x v . The projection of a tup-
le over a subset of variables c Y is denoted
[ ]c . A constraint c is said satisfied by if c Y
and [ ] cc r , violated otherwise. is said con-
sistent with respect to a given subproblem if it sat-
isfies all its constraints. A solution is an assign-
ment of all the variables satisfying all the con-
straints.
The structure of a CSP can be represented by
the graph (X, C), called the constraint graph,
whose vertices are the variables of X and with an
edge between two vertices if the corresponding
variables share a constraint in C. A graph is chor-
dal if every cycle of length at least four has a
chord, i.e. an edge joining two non-consecutive
vertices along the cycle.
A tree-decomposition [Robertson and Seymour,
1986] of a CSP is a pair ( , ) with = ( , )I F
a tree with vertices I and edges F and
= { : }i i I a family of subsets of X, such that
each cluster i is a node of and satisfies: (1)
=i I i X , (2) for each constraint c C , there
exists i I with ic , (3) for all , ,i j k I , if k
is on a path from i to j in , then i j k . The
width of a tree-decomposition ( , ) is equal to
| | 1max i I i . The tree-width of is the mini-
mum width over all its tree-decompositions. Find-
ing an optimal tree-decomposition is NP-Hard
[Arnborg et al., 1987].
A tree-decomposition can be found by triangu-
lation of (i.e. adding edges to) the constraint graph
such that it becomes chordal and then by search-
ing the maximal cliques of the triangulated con-
straint graph (resulting in the clusters ) and fi-
nally by selecting a maximum spanning tree on
the cluster graph with edges between i and j if
i j and edge weights equal to | |i j .
In the experiments, we used the Min-Fill greedy
heuristic (it locally adds the minimum number of
edges to the constraint graph), a very usual heuris-
tic aimed at the production of tree-decompositions
with a small tree-width [Rose, 1970].
In the following, from a tree-decomposition,
we consider a rooted tree ( , )I F with root 1 and
we note ( )iSons the set of son clusters of i and
( )iDesc the set of variables which belong to i
or to any descendant j of i in the subtree
rooted in i .
Example 1. Consider the CSP the constraint
graph of which is provided in Fig. 1, a. We assume
that each domain is { , , , }a b c d and each constraint
= { , }ij i jc x x has a relation
ijcr such that =i jx x ,
which defines a graph coloring problem.
A – A constraint graph b – Its tree-decomposition
Fig. 1. A tree-decomposition of a small problem with 8 variables
Fig. 1, b represents an optimal tree-decomposi-
tion for the chordal graph of Fig. 1, a. We have
1 1 2 3= { , , }x x x , 2 2 3 4 5={ , , , }x x x x , 3 = 4 5 6{ , , }x x x ,
and 4 3 7 8={ , , }x x x . For instance, Desc(2)=22=
= 2 3 4 5 6{ , , , , }x x x x x . The tree-width is 3.
УСиМ, 2011, № 2 7
3. Exact solution counting with #BTD
The essential property of a tree decomposition
is that assigning ij ( ( )j iSons ) by the as-
signment separates the initial problem into two
subproblems, which can then be solved independ-
ently and the product of their number of solutions
returned as the total number of solutions. The first
subproblem, denoted / [ ]j i j and rooted in j, is
defined by the variables in Desc(j), with variables
ij assigned by , and by all the constraints
involving at least one variable in Desc(j)\ i. The
remaining constraints, together with the variables
they involve, define the remaining subproblem.
A tree search backtracking algorithm can ex-
ploit this property by using a suitable variable as-
signment ordering: the variables of any cluster i
must be assigned before the variables that remain
in its son clusters. In this case, for any cluster
( )j iSons , once ij is assigned, the sub-
problem rooted in j conditioned by the current
assignment of ij can be solved independ-
ently of the rest of the problem. The exact number
of solutions nb of this subproblem / [ ]j i j , cal-
led a #good and represented by a pair ( [ ],i j
nb), can be recorded, which means it will never be
computed again for the same assignment of ij.
This is why algorithms such as BTD [Jégou and
Terrioux, 2003] and AND/OR graph search
[Dechter and Mateescu, 2004, 2007], exploiting
the related notions of structural goods and pseudo-
tree [Freuder and Quinn, 1985] respectively, are
able to keep their time (and space) complexity ex-
ponential in the size of the largest cluster only.
We denote /j the number of solutions of sub-
problem / [ ]j i j compatible with an assignment
of (ij) Y, Y j. It corresponds to the
number of extensions of on Desc(j) satisfying
all the constraints in / [ ]j i j . The total number
of solutions of is S1/.
Example 2. Consider the CSP in Example 1.
1 2 8( , , , )x x x is a suitable variable ordering for
the tree-decomposition of Fig. 1, b. Given
1 2 3= ( , , )x a x b x c , the variable set of
2/ [ ]1 2 is 2( )Desc , (with
2 3
={ }, ={ }x xd b d c and
4 5 6
= = = { , , , }x x xd d d a b c d ) and its constraint set
is 24 25 34 35 45 46 56{ , , , , , , }c c c c c c c .
For instance, 2/ 3/( , ) 3/( , )4 5 4 5
= =x a x d x d x a
= 2 + 2 = 4. And the number of solutions of 4/( )3x c
is 4/ = 6 . Thus, there are 2/ 4/ = 24 ex-
tensions of being solutions of . Note that for
4/( )3x c , 3(( ),6)x c is a #good. So, for any
other assignment of 1 with 3x assigned to c,
it is not necessary to compute the number of solu-
tions of 4/ [ ]1 4 because the #good 3(( ),6)x c
will be exploited in this case. The total number of
solutions is 1/ = 576 .
#BTD is described in Algorithm 1. Given an as-
signment , a cluster i , and a set
i
V of unassig-
ned variables of i , #BTD (, i ,
i
V ) looks for the
number /i of extensions of on ( )iDesc
such that [ \ ] = [ \ ]i ii i
V V . The first call is
#BTD ( 1 1, , ) and it returns the number of so-
lutions 1/ . Inside a cluster i , it proceeds clas-
sically by assigning a value to a variable and by
backtracking if any constraint is violated. When
every variable in i is assigned, #BTD computes
the number of solutions of the subproblem rooted
in the first son of i , if there is one (otherwise the
current subproblem is totally assigned and con-
tains only one solution). More generally, let us
consider j , a son of i . Given a current assign-
ment of i , #BTD checks whether the assign-
ment [ ]i j corresponds to a #good. If so,
#BTD multiplies the recorded number of solutions
with the current number of solutions NbSol
( /i ). Otherwise, it extends on ( )jDesc in
8 УСиМ, 2011, № 2
order to compute its number of consistent exten-
sions nb ( /j ). Then, it records the #good
( [ ], )i j nb . #BTD computes the number of
solutions of the subproblem rooted in the next son
of i . Finally, when each son of i has been ex-
amined, #BTD tries to modify the current assign-
ment of i . The number of solutions of the sub-
problem rooted in i is the sum of solution counts
for every assignment of i .
Theorem 1. #BTD is sound, complete and ter-
minates.
Proof. #BTD exploits two kinds of problem
decomposition. The first one is based on condi-
tioning. The second one is based on tree-
decomposition. In the first case (Else branch start-
ing at line 2 in Algorithm 1), let x
a be the sub-
problem derived from by assigning variable x to
value a. We have =
x
x
aa d . We denote Sol
the set of solutions of and =| |ol . For any
two distinct values a and b of xd , we have
=x x
a b
ol ol
. Thus, the set { | }x
a
xol a d
is a partition of ol and = x
axa d
.
In the second case of problem decomposition
(If branch starting at line 1 in Algorithm 1), we are
dealing with independent subproblems. Two CSPs
1 1 1 1 1= ( , , , )X D C R and 2 2 2 2 2= ( , , , )X D C R are
independent if and only if 1 2 =X X . If
1 2= with 1 and 2 two independent
subproblems, then the solutions of is the Carte-
sian product of the solutions of 1 and 2 . There-
fore,
1 2
= . In the case of a tree-
decomposition, given a cluster i and an assign-
ment of Y X such that ( ) = i iDesc Y , we
have all the subproblems / [ ] ,j ji j
( )iSons mutually independent. Then has
/ /( )
=
j i
i jSons
consistent extensions on
( )iDesc .
If ( , )I nb is a #good of ][/ jij such that
[ ] =i jC C , then has nb consistent exten-
sions on ( )jDesc C : / =j nb .
Theorem 2. #BTD has time complexity in
1( )wn m d and space complexity in ( )sn s d .
Proof. Space complexity. #BTD only records
#goods. These are assignments on the intersec-
tions i j with j a son of i . Therefore, if s
is the size of the largest of these intersections,
#BTD has a space complexity of ( )sn s d be-
cause the number of these intersections is bounded
by n, while the number of #goods associated to
one intersection is bounded by sd and the size of
a #good is at most s.
Time complexity. In the worst case, #BTD ex-
plores all the clusters (at most n) and tries all the
values of every variable inside each cluster, each
time checking at most m constraints at line 3.
УСиМ, 2011, № 2 9
Thanks to its #good recording mechanism, it
never explores the same cluster with the same as-
signment of its variables twice. The number of
assignments of a cluster is bounded by 1wd with
= max | | 1ii
w , the width of the tree-decom-
position. Consequently, #BTD has a time com-
plexity in 1( )wn m d .
In practice, for problems with a large tree-
width, #BTD may run out of time and memory, as
shown in Section 5. In this case, we are interested
in an approximate method.
4. Approximate solution counting with
Approx#BTD
We consider here CSPs with a large tree-width
but a sparse constraint graph. We define a collec-
tion of easy-to-solve subproblems of an original
problem by partitioning the set of constraints,
that is the set of edges in the constraint graph in
the case of a binary CSP. The constraint graph
( , )X C will be partitioned into k subgraphs
1 1( , )X E , , ( , )k kX E , such that =iX X ,
=iE C and =iE . We add the extra prop-
erty that each ( , )i iX E is chordal (without adding
extra edges as for building a tree-decomposition).
Thus, each ( , )i iX E will be associated to a chordal
subproblem i (with corresponding sets of vari-
ables iX and constraints iE ), which should have a
small tree-width and be efficiently solved using
#BTD.
Assume that
i
is the number of solutions for
each subproblem i , 1 i k . We will estimate
the number of solutions of exploiting the fol-
lowing property. Let be any assignment of X,
we denote ( ) the probability of « is a
solution of P». We have ( ) =
xx X
d
,
assuming a uniform prior probability distribution
among the different value assignments. We also
have
1 2( ) = ( )k =
1 2 1
1 1
= ( ) ( | )
( | ).k k
In order to simplify these conditional probabili-
ties, we assume probability independence between
the ( )i terms, which is true only if =iX .
Thus, we have
1 2( ) ( ) ( ) ( ).k
Now, we can easily deduce the following prop-
erty in order to estimate .
Property 1. Given a CSP = ( , , , )X D C R and
a partition 1{ ,..., }k of induced by a partition
of C in k elements.
=1
i
i
k
x
i x Xx
x X
d
d
. (1)
Recall that this approximation returns an exact
answer if all the subproblems are independent
( =iX ) or = 1k ( is already chordal as in
Example 1) or if there exists an inconsistent sub-
problem i ( has no solution)3. Moreover, we
can provide a trivial upper bound on the number
of solutions due to the fact that each subproblem
i is a relaxation of (the same argument is used
in [Pesant, 2005] to construct an upper bound):
[1, ]
min i
i
x
i k x Xx
x X
d
d
(2)
Approx#BTD is described in Algorithm 2.
Applied to a problem with constraint graph
( , )X C , the method builds a partition 1{ ,..., }kE E
of C such that the constraint graph ( , )i iX E is
chordal for all 1 i k . Each chordal subgraph is
produced by the MaxChord algorithm4 [Dear-
3Due to the celling function in Equation 1, if the ap-
proximation returns zero then has no solution.
4MaxChord+ returns a maximal subgraph for binary
CSPs. For non-binary CSPs, we do not guarantee subgraph
maximality and add to the subproblem all the constraints
totally included in the extracted chordal subgraph. In Figure 2,
the edge {x3,x5} has been removed from the first part be-
10 УСиМ, 2011, № 2
ing et al., 1988], described in Algorithm 3. An ex-
ample of a partition found by Approx#BTD is
given in Figure 2. Subproblems associated to
(Xi, Ei) are solved with #BTD. The method returns
an approximation to the number of solutions of
based on Property 1.
Theorem 3. Approx#BTD is sound, complete
and terminates.
Proof. It suffices to prove that we have a parti-
tion of the constraints at the end of the while loop
in order to be able to apply Property 1. This can be
easily shown by induction using the invariants
=1= i
j jX X X and « 1 2= ( , , , , )iQ C E E E
is a partition of C» inside the loop.
Theorem 4. Approx#BTD has time complex-
ity in 2 1( )wn m d and space complexity in
( )sn s d with < 1 1s w c w n .
Proof. Space complexity. Approx#BTD has the
same space complexity as #BTD applied on the larg-
est subproblem i w.r.t. the largest cluster inter-
section denoted , , , [1, ]= | |max i i i
u v
i i
u v i k u vs .
Time complexity. The number of iterations of
Approx#BTD is less than n. At each step, the
cause it is associated to the ternary constraint {x3, x4x5} not
totally included in this part.
first variable considered by MaxChord at line 4
will have all its constraints totally included in the
maximal chordal subgraph. Each chordal subgraph
and its associated optimal tree-decomposition can
be computed in ( )O nm [Dearing et al., 1988].
Thus, the time complexity of Approx#BTD is in
2 1( )wn m d with the largest subproblem tree-
width , [1, ]= | | 1max i i
u
i
i k uw . Because each i
is a partial chordal subgraph of , its tree-width
w is equal to the maximum clique size in its sub-
graph [Fulkerson and Gross, 1965] which is by
definition less than or equal to the maximum
clique size of the original problem, called the
clique number c , inferior to the problem tree-
width 1w .
5. The experimental results
We implemented #BTD and Approx#BTD
counting methods on top of toulbar2 C++
solver5. The experimentations were performed on
5http://mulcyber.toulouse.inra.fr/projects/toulbar2/ ver-
sion 0.8.1.
УСиМ, 2011, № 2 11
a Linux 2.6 GHz Intel Xeon computer with 2GB.
Reported times (total CPU times as given by the
#SAT solvers or reported by the bash command
«time» if not) are in seconds. For #BTD and
Approx#BTD, the total time does not include the
task of finding a variable elimination ordering6.
We limit to one hour the time spent for solving a
given instance. Inside #BTD (line 3), we use gen-
eralized arc consistency (only for constraints with
2 or 3 unassigned variables) instead of backward
checking, for efficiency reasons. The min domain
/max degree dynamic variable ordering, modified
by a conflict back-jumping heuristic [Lecoutre et
al., 2006], is used inside the clusters. Our methods
exploit a binary branching scheme. The variable is
assigned to its first value or this value is removed
from the domain.
а – An original problem b – The first part c – The second part
Fig. 2. A partition of a CSP with 6 variables found by Approx#BTD.
The original problem has 5 binary constraints ({x1,x2}, {x1,x4},
{x1,x6}, {x2,x3}, {x5,x6}), and one ternary constraint {x3,x4,x5}.
We have k = 2, w’ = 2, c = w =3
We performed experiments on SAT and CSP
benchmarks7. We selected academic (random k-
SAT wff, All-Interval Series ais, Towers of Hanoi
hanoi) and industrial (circuit fault analysis ssa and
bit, logistics planning logistics) satisfiable in-
stances. CSP benchmarks are graph coloring instan-
ces (counting the number of optimal solutions).
For #SAT solvers only, CSP instances are trans-
lated into SAT by using the direct encoding (one
Boolean variable per domain value, one clause per
domain to enforce at least one domain value is
selected, and a set of binary clauses to forbid mul-
tiple value selection).
6Which was always fast to compute (linear complexity).
7From www.satlib.org, www.satcompetition.org and
mat.gsia.cmu.edu/COLOR02/.
5.1. The evaluation of exact methods
We compared #BTD with state-of-the-art #SAT
solvers Relsat [Bayardo and Pehoushek, 2000]
v2.02, Cachet [Sang et al., 2004] v1.22 (with a
default memory limit of 5 MB), sharpSAT [Thur-
ley, 2006] v1.1, and also c2d [Darwiche, 2004]
v2.20 which also exploits the problem structure
(with a default memory limit of 512 MB and a
limit of 64 MB for storing its d-DNNF). c2d and
#BTD methods use the Min-Fill variable elimina-
tion ordering heuristic (except for hanoi where we
used the default file order) to construct a tree-
decomposition / d-DNNF.
Our results are summarized in Table 1. The co
T a b l e 1. Comparison of exact methods. Legend: mem: out of
memory, – : out of time (for c2d, * : out of memory
for storing NNF)
c2d
s
h
a
r
p
S
A
T
C
a
c
h
e
t
R
e
l
s
a
t
#B
T
D
n
(Bool-
vars)
d w
Time Time Time Time Time
SAT
wff.3.100.150 100 39 1.8e21 * mem – – mem
wff.3.150.525 150 92 1.4e14 * mem 266. 2509 mem
wff.4.100.500 100 80 – * mem – – mem
ssa7552-038 1501 25 2.84e40 0.15 0.06 0.22 67 0.65
ssa7552-158 1363 9 2.56e31 0.10 0.03 0.07 3 0.19
ssa7552-159 1363 11 7.66e33 0.09 0.04 0.07 4 0.27
ssa7552-160 1391 12 7.47e32 0.12 0.04 0.08 5 0.30
2bitcomp_5 125 36 9.84e15 0.43 0.05 0.14 1 16.24
2bitmax_6 252 2 58 2.10e29 17.00 0.87 1.51 20 mem
ais6 61 41 24 0.05 0.01 0.03 <1 0.08
ais8 113 77 40 0.51 0.17 0.58 <1 3.27
ais10 181 116 296 16.64 4.13 29.19 6 543
ais12 265 181 1328 1147 161. 2173 229 –
logistics.a 828 116 3.8e14 – 0.17 3.78 10 mem
logistics.b 843 107 2.3e23 – 1.38 12.34 433 mem
hanoi4 718 46 1 7.18 1.11 32.64 3 1.87
hanoi5 1931 58 1 – mem – – 26.75
CSP (Graph Coloring)
2-Insertions_3 37 (148) 4 9 6.84e13 235. mem – – 7.80
2-Insertions_4 149 (596) 4 38 – – mem – – –
DSJC125.1 125 (625) 5 65 – – mem – – mem
games120 120 (1080) 9 41 – – mem – – mem
GEOM30a 30 (180) 6 6 4.98e14 0.86 5.53 – – 0.10
GEOM40 40 (240) 6 5 4.1e23 1.00 mem – – 0.09
le450_5a 450 (2250) 5 315 3840 – 32.31 318 326 1100
le450_5b 450 (2250) 5 318 120 – 13.12 227 187 1364
le450_5c 450 (2250) 5 315 120 – 2.18 19.09 57 47.53
le450_5d 450 (2250) 5 299 960 – 4.40 14.60 36 92.03
Mug100_1 100 (400) 4 3 1.3e37 0.19 23.88 – – 0.02
myciel5 47 (282) 6 21 – – mem – – mem
lumns are: instance name, number of variables (and
also the number of Boolean variables on translated
12 УСиМ, 2011, № 2
CSP instances), maximum domain size, width of
the tree-decomposition, exact number of solutions
if known, time for c2d, sharpSAT, Cachet,
Relsat, and #BTD. We noticed that #BTD can
solve instances with relatively small tree-widths
(except for ais and le450 which have few solu-
tions). Exact #SAT solvers generally perform bet-
ter than #BTD on SAT instances (except for ha-
noi5), with sharpSAT obtaining the best results,
but have difficulties on translated CSP instances.
Here, #BTD maintaining arc consistency performed
better than #SAT solvers using unit propagation.
5.2. Evaluation of approximate methods
Table 2 gives an analysis of Approx#BTD on the
tested instances. The columns are: instance name,
T a b l e 2. Analysis of Approx#BTD performance and subprob-
lem features
n d w w k Time
SAT
wff.3.100.150 100 1.80e21 39 3 6 3.10e21 5.05e27 0.03
wff.3.150.525 150 1.14e14 92 3 13 1.58e15 1.13e42 0.18
wff.4.100.500 100 – 80 6 48 1.59e16 4.87e29 0.47
ssa7552-038 1501 2.84e40 25 6 4 9.33e38 3.79e142 1.34
ssa7552-158 1363 2.56e31 9 5 3 2.22e25 1.41e79 0.77
ssa7552-159 1363 7.66e33 11 5 3 6.53e27 6.33e88 0.85
ssa7552-160 1391 7.47e32 12 5 3 4.50e26 3.36e106 1.09
2bitcomp_5 125 9.84e15 36 6 4 8.61e16 6.81e27 0.02
2bitmax_6 252 2 2.10e29 58 6 4 4.53e29 7.19e45 0.10
ais6 61 24 41 12 8 1 1.81e9 0.04
ais8 113 40 77 16 11 1 3.49e15 0.20
ais10 181 296 116 21 23 1 2.06e22 0.84
ais12 265 1328 181 26 23 1 3.19e29 2.47
logistics.a 828 3.8e14 116 10 24 1 4.91e180 14.85
logistics.b 843 2.3e23 107 13 25 1 2.15e169 14.08
hanoi4 718 1 46 10 8 1 4.26e106 1.40
hanoi5 1931 1 58 12 11 1 4.48e309 16.05
CSP (Graph Coloring)
2-Insertions_3 37 4 6.84e13 9 1 3 1.91e13 6.00e17 0.01
2-Insertions_4 149 4 – 38 1 6 1.30e22 1.64e71 0.07
DSJC125.1 125 5 – 65 3 7 1.23e13 2.27e70 0.12
games120 120 9 – 41 8 6 1.12e78 1.92e99 9.84
GEOM30a 30 6 4.98e14 6 5 2 7.29e14 1.81e15 0.04
GEOM40 40 6 4.1e23 5 5 2 4.8e23 1.72e24 0.01
le450_5a 450 5 3840 315 4 13 1 2.41e216 3.17
le450_5b 450 5 120 318 4 13 1 5.72e213 3.23
le450_5c 450 5 120 315 4 20 1 1.49e201 7.42
le450_5d 450 5 960 299 4 20 1 8.58e200 7.38
mug100_1 100 4 1.3e37 3 2 2 5.33e37 7.18e41 0.01
myciel5 47 6 – 21 1 8 7.70e17 8.53e32 0.03
myciel6 95 7 – 35 1 13 5.49e29 9.80e73 0.19
myciel7 191 8 – 66 1 21 4.25e35 2.96e161 1.23
number of variables, maximum domain size, exact
number of solutions if known, width of the tree-
decomposition for the original problem, maximum
width of the tree-decomposition for all the chordal
subproblems, number of subproblems in the parti-
tion, approximate number of solutions and upper-
bound on the number of solutions as given by
Equation 2, and time for Approx#BTD.
Our approximate method exploits a partition of
the constraint graph in such a way that the result-
ing subproblems to solve have a small tree-width
on these instances (w 26). It has the practical
effect that the method is relatively fast whatever
the original tree-width. Notice that the upper-
bound is generally very poor even with a small
number of subproblems (e.g. ssa).
We also compared Approx#BTD with the ap-
proximation method SampleCount [Gomes et
al., 2007a]. With parameters (s = 20, t = 7, = 1),
SampleCount-LB provides an estimated lower
bound on the number of solutions with a high-
confidence interval (99% confidence), after seven
runs. With parameters (s = 20, t = 1, = 0), called
SampleCount-A in the following table, it gives
only an approximation without any guarantee, af-
ter the first run of SampleCount-LB.
Our results are summarized in Table 3. The co-
lumns are : instance name, exact number of soluti-
ons if known, approximate number of solutions and
time for Approx#BTD and SampleCount-A,
and estimated lower bound on the number of so-
lutions and time for SampleCount-LB. The qua-
T a b l e 3. Comparison of approximate methods. Legend: – : out
of time (1 hour)
Approx#BTD
Sample
Count-A
Sample
Count-LB
ˆ
T
im
e
ˆ
T
im
e
ˆ
T
im
e
SAT
wff.3.100.150 1.8e21 3.10e21 0.1 1.37e21 959.8 – –
wff.3.150.525 1.4e14 1.58e15 0.2 3.80e14 0.7 2.53e12 4.6
wff.4.100.500 – 1.59e16 0.5 4.15e16 2045.0 – –
ssa7552-038 2.84e40 9.33e38 1.3 1.11e40 134.0 3.54e38 1162.0
ssa7552-158 2.56e31 2.22e25 0.8 1.43e30 14.1 1.43e30 177.0
ssa7552-159 7.66e33 6.53e27 0.8 6.49e34 32.8 1.64e32 182.0
ssa7552-160 7.47e32 4.50e26 1.1 5.08e32 144.0 2.31e31 1293.0
2bitcomp_5 9.84e15 8.61e16 0.1 4.37e15 0.2 3.26e15 1.2
2bitmax_6 2.10e29 4.53e29 0.1 1.62e29 1.7 2.36e26 10.3
ais6 24 1 0.1 12 0.1 12 0.2
ais8 40 1 0.2 16 1.5 12 15.9
ais10 296 1 0.8 124 45.9 20 312.0
ais12 1328 1 2.5 0 9.2 0 9.2
logistics.a 3.8e14 1 14.8 7.25e11 171.0 0 605.0
logistics.b 2.3e23 1 14.1 2.13e23 199.0 0 229.0
hanoi4 1 1 1.4 0 5.2 0 5.2
hanoi5 1 1 16.0 0 6.1 0 6.2
УСиМ, 2011, № 2 13
Approx#BTD SampleCount-A SampleCount-LB
ˆ
T
im
e
ˆ
T
im
e
ˆ
T
im
e
CSP (Graph Coloring)
2-Insertions_3 6.84e13 1.91e13 0.1 4.73e12 1.0 4.73e12 7.4
2-Insertions_4 – 1.30e22 0.1 0 3.8 0 3.8
DSJC125.1 – 1.23e13 0.1 0 73.1 0 73.2
games120 – 1.12e78 9.8 7.33e64 13.8 1.35e61 91.1
GEOM30a 4.98e14 7.29e14 0.1 1.23e13 0.4 3.28e12 3.7
GEOM40 4.1e23 4.8e23 0.1 2.14e20 1.5 6.50e19 9.3
le450_5a 3840 1 3.2 0 8.6 0 8.6
le450_5b 120 1 3.2 0 8.6 0 8.6
le450_5c 120 1 7.4 0 110.0 0 111.0
le450_5d 960 1 7.4 0 4.6 0 54.6
mug100_1 1.3e37 5.33e37 0.1 4.2e34 2.1 4.20e34 15.6
myciel5 – 7.69e17 0.1 7.29e17 0.9 7.29e17 6.4
myciel6 – 5.49e29 0.2 9.38e40 4.5 7.42e36 30.7
myciel7 – 4.26e35 1.2 1.37e80 27.7 5.56e74 163.0
lity of the approximation found by Approx#BTD is relatively
good and it is comparable (except for ssa, logistics, and my-
ciel6-7 benchmarks) to SampleCount-A, which takes more
time.
For graph coloring, Approx#BTD outperforms also a de-
dicated CSP approach producing an estimated lower bound:
2_Insertion_3 2.3e12, games120 4.5e42, and mug100_1
1.0e28 in 1 minute each; myciel5 4.1e17 in 12 minutes,
times were measured on a 3.8GHz Xeon as reported in
[Gomes et al., 2007b].
6. Conclusion
In this paper, we have proposed two methods for counting
solutions of CSPs. These methods are based on a structural
decomposition of CSPs. We have presented an exact method,
which is adapted to problems with a small tree-width. For prob-
lems with a large tree-width and a sparse constraint graph, we
have presented a new approximate method whose quality is
comparable with existing methods, which is much faster than
other approaches, and which requires no parameter tuning (ex-
cept for the choice of a tree decomposition heuristic). Exploring
other structural parameters [Nishimura et al., 2007, Samer and
Szeider, 2010] should deserve future work. A practical im-
provement of our approach would be to impose a limit on the
maximum clique size of the extracted chordal subproblems
when the original problem has large arity constraints or a large
clique number. Conversely, denser non-chordal subproblems
could be produced and solved in an anytime manner as done in
[Choi and Darwiche,2006] when the original problem has a
small clique number.
A direction of future work is also to extend our approach
to the problem of (approximate) inference in probabilistic
discrete graphical models.
1. Arnborg S., Corneil D., Proskurowski A. Complexity
of finding embeddings in a k-tree // SIAM J. of Dis-
crete Mathematics. – 1987. – N 8. – P. 277–284.
2. Bayardo R., Pehoushek J. Counting models using con-
nected components // Proc. of AAAI-00. – Austin,
Texas. – 2000. – P. 157–162.
3. Burton R., Steif J. Nonuniqueness of measures of maxi-
mal entropy for subshifts of finite type // Ergodic theory
and dynamical system, 1994.
4. Choi A., Darwiche A. An edge deletion semantics for be-
lief propagation and its practical impact on approxima-
tion quality // Proc. of AAAI-06. – 2006. – P. 1107–1114.
5. Darwiche A. On the tractable counting of theory mod-
els and its applications to truth maintenance and belief
revision // J. of Applied Non-classical Logic. – 2001. –
N 11. – P. 11–34.
6. Darwiche A. New advances in compiling cnf to decom-
posable negation normal form // Proc. of ECAI-04.
Valencia, Spain. – 2004. – P. 328–332.
7. Dearing P., Shier D., Warner D. Maximal chordal sub-
graphs // Discrete Applied Mathematics. – 1988. –
20(3). – P. 181–190.
8. Dechter R., Mateescu R. And/or search spaces for graphi-
cal models // Artif. Intell. – 2007. – 171(2–3). – P. 73–106.
9. Dechter R., Mateescu R. The impact of and/or search
spaces on constraint satisfaction and counting // Proc.
of CP-04. Toronto, CA. – 2004. – P. 731–736.
10. Favier A., de Givry S., Jégou P. Exploiting problem
structure for solution counting // Proc. of CP-09, Lis-
bon, Portugal. – 2009. – P. 335–343.
11. Freuder E., Quinn M. Taking advantage of stable sets
of variables in constraint satisfaction problems // Proc.
of IJCAI-85. Los Angeles, CA. – 1985. – P. 1076–1078.
12. Fulkerson D., Gross O. Incidence matrices and interval
graphs // Pacific J. Math. – 1965. – 15(3). – P. 835–855.
13. Gogate V., Dechter R. Approximate counting by sam-
pling the backtrack-free search space // Proc. of
AAAI-07. Vancouver, CA. – 2007. – P. 198–203.
14. Gogate V., Dechter R. Approximate Solution Sampling
(and Counting) on AND/OR search spaces // Proc. of
CP-08. Sydney, AU. – 2008. – P. 534–538.
15. Gomes C., Sabharwal A., Selman B. Model counting:
A new strategy for obtaining good bounds // Proc. of
AAAI-06. Boston, MA. – 2006. – P. 534–538.
16. From sampling to model counting / C. Gomes, J. Hoff-
mann, A. Sabharwal et al. // Proc. of IJCAI-07. Hydera-
bad, India. – 2007. – P. 2293–2299.
17. Counting CSP solutions using generalized XOR constraints
/ C. Gomes,W-J. van Hoeve, A. Sabharwal et al. // Proc. of
AAAI-07. Vancouver, BC. – 2007. – P. 204–209.
18. Gomes C., Sabharwal A., Selman B. Handbook of Satis-
fiability, chapter 20, Model Counting. IOS Press, 2009.
19. Jégou P., Terrioux C. Hybrid backtracking bounded by
tree-decomposition of constraint networks // Artificial
Intelligence. – 2003. – 146. – P. 43–75.
20. Kask K., Dechter R., Gogate V. New look-ahead schemes
for constraint satisfaction // Proc. of AI&M, 2004.
21. Kroc L., Sabharwal A., Selman B. Leveraging belief
propagation, backtrack search, and statistics for model
counting // Proc. of CPAIOR-08. Paris, France. – 2008. –
P. 127–141.
End on the page 70
70 УСиМ, 2011, № 2
Ending of the article by A. Favier et al.
22. Kumar T. A model counting characterization of diag-
noses // Proc. of the 13th International Work-shop on
Principles of Diagnosis, 2002.
23. Last conflict based reasoning / C. Lecoutre, L. Sais,
S. Tabary, V. Vidal // Proc. of ECAI-06. Trento, It-
aly. – 2006. – P. 133–137.
24. Mann M., Tack G., Will S. Decomposition during search
for propagation-based constraint solvers. CoRR, abs/
0712.2389, 2007.
25. Montanari U. Network of constraints: Fundamental
properties and applications to picture processing // Inf.
Sci. – 1974. – N 7. – P. 95–132.
26. Nishimura N., Ragde P., Szeider S. Solving #SAT us-
ing vertex covers // Acta Inf. – 2007. – 44(7). –
P. 509–523.
27. Pesant G. Counting solutions of CSPs: A structural ap-
proach // Proc. of IJCAI-05. Edinburgh, Scotland. –
2005. – P. 260–265.
28. Robertson N., Seymour P. Graph minors II: Algo-
rithmic aspects of tree-width // Algorithms. – 1986. –
N 7. – P. 309–322.
29. Rose D. Tringulated graphs and the elimination process
// J. of Mathematical Analysis and its Applications. –
1970. – N 32.
30. Roth D. On the hardness of approximate reasoning
// Artificial Intelligence. – 1996. – 82(1–2). – P. 273–302.
31. Samer M., Szeider S. Algorithms for propositional model
counting // J. of Discrete Algorithms. – 2010. – N 8. –
P. 50–64.
32. Combining component caching and clause learning for
effective model counting / T. Sang, F. Bacchus,
P. Beame et al. // In SAT-04, Vancouver, Canada,
2004.
33. Thurley M. SharpSAT – counting models with advan-
ced component caching and implicit BCP // Proc. of
SAT-06. Seattle, WA. – 2006. – P. 424–429.
34. Valiant L. The complexity of computing the permanent
// Theoretical Computer Sciences. – 1979. – N 8. –
P. 189–201.
35. Wei W., Selman B. A new approach to model counting
// Proc. of SAT-05. St. Andrews, UK. – 2005. – P. 324–
339.
36. Zanarini A., Pesant G. Solution counting algorithms
for constraint-centered search heuristics // Constraints. –
2009. – 14(3). – P. 392–413.
© A. Favier, S.de Givry, INRA MIA Toulouse, France;
Ph. Jégou, Universitè Paul Cèzanne, Marseille, France, 2011
3.pdf
70.pdf
<<
/ASCII85EncodePages false
/AllowTransparency false
/AutoPositionEPSFiles true
/AutoRotatePages /None
/Binding /Left
/CalGrayProfile (Dot Gain 20%)
/CalRGBProfile (sRGB IEC61966-2.1)
/CalCMYKProfile (U.S. Web Coated \050SWOP\051 v2)
/sRGBProfile (sRGB IEC61966-2.1)
/CannotEmbedFontPolicy /Error
/CompatibilityLevel 1.4
/CompressObjects /Tags
/CompressPages true
/ConvertImagesToIndexed true
/PassThroughJPEGImages true
/CreateJobTicket false
/DefaultRenderingIntent /Default
/DetectBlends true
/DetectCurves 0.0000
/ColorConversionStrategy /CMYK
/DoThumbnails false
/EmbedAllFonts true
/EmbedOpenType false
/ParseICCProfilesInComments true
/EmbedJobOptions true
/DSCReportingLevel 0
/EmitDSCWarnings false
/EndPage -1
/ImageMemory 1048576
/LockDistillerParams false
/MaxSubsetPct 100
/Optimize true
/OPM 1
/ParseDSCComments true
/ParseDSCCommentsForDocInfo true
/PreserveCopyPage true
/PreserveDICMYKValues true
/PreserveEPSInfo true
/PreserveFlatness true
/PreserveHalftoneInfo false
/PreserveOPIComments true
/PreserveOverprintSettings true
/StartPage 1
/SubsetFonts true
/TransferFunctionInfo /Apply
/UCRandBGInfo /Preserve
/UsePrologue false
/ColorSettingsFile ()
/AlwaysEmbed [ true
]
/NeverEmbed [ true
]
/AntiAliasColorImages false
/CropColorImages true
/ColorImageMinResolution 300
/ColorImageMinResolutionPolicy /OK
/DownsampleColorImages true
/ColorImageDownsampleType /Bicubic
/ColorImageResolution 300
/ColorImageDepth -1
/ColorImageMinDownsampleDepth 1
/ColorImageDownsampleThreshold 1.50000
/EncodeColorImages true
/ColorImageFilter /DCTEncode
/AutoFilterColorImages true
/ColorImageAutoFilterStrategy /JPEG
/ColorACSImageDict <<
/QFactor 0.15
/HSamples [1 1 1 1] /VSamples [1 1 1 1]
>>
/ColorImageDict <<
/QFactor 0.15
/HSamples [1 1 1 1] /VSamples [1 1 1 1]
>>
/JPEG2000ColorACSImageDict <<
/TileWidth 256
/TileHeight 256
/Quality 30
>>
/JPEG2000ColorImageDict <<
/TileWidth 256
/TileHeight 256
/Quality 30
>>
/AntiAliasGrayImages false
/CropGrayImages true
/GrayImageMinResolution 300
/GrayImageMinResolutionPolicy /OK
/DownsampleGrayImages true
/GrayImageDownsampleType /Bicubic
/GrayImageResolution 300
/GrayImageDepth -1
/GrayImageMinDownsampleDepth 2
/GrayImageDownsampleThreshold 1.50000
/EncodeGrayImages true
/GrayImageFilter /DCTEncode
/AutoFilterGrayImages true
/GrayImageAutoFilterStrategy /JPEG
/GrayACSImageDict <<
/QFactor 0.15
/HSamples [1 1 1 1] /VSamples [1 1 1 1]
>>
/GrayImageDict <<
/QFactor 0.15
/HSamples [1 1 1 1] /VSamples [1 1 1 1]
>>
/JPEG2000GrayACSImageDict <<
/TileWidth 256
/TileHeight 256
/Quality 30
>>
/JPEG2000GrayImageDict <<
/TileWidth 256
/TileHeight 256
/Quality 30
>>
/AntiAliasMonoImages false
/CropMonoImages true
/MonoImageMinResolution 1200
/MonoImageMinResolutionPolicy /OK
/DownsampleMonoImages true
/MonoImageDownsampleType /Bicubic
/MonoImageResolution 1200
/MonoImageDepth -1
/MonoImageDownsampleThreshold 1.50000
/EncodeMonoImages true
/MonoImageFilter /CCITTFaxEncode
/MonoImageDict <<
/K -1
>>
/AllowPSXObjects false
/CheckCompliance [
/None
]
/PDFX1aCheck false
/PDFX3Check false
/PDFXCompliantPDFOnly false
/PDFXNoTrimBoxError true
/PDFXTrimBoxToMediaBoxOffset [
0.00000
0.00000
0.00000
0.00000
]
/PDFXSetBleedBoxToMediaBox true
/PDFXBleedBoxToTrimBoxOffset [
0.00000
0.00000
0.00000
0.00000
]
/PDFXOutputIntentProfile ()
/PDFXOutputConditionIdentifier ()
/PDFXOutputCondition ()
/PDFXRegistryName ()
/PDFXTrapped /False
/CreateJDFFile false
/Description <<
/ARA <FEFF06270633062A062E062F0645002006470630064700200627064406250639062F0627062F0627062A002006440625064606340627062100200648062B062706260642002000410064006F00620065002000500044004600200645062A064806270641064206290020064406440637062806270639062900200641064A00200627064406450637062706280639002006300627062A0020062F0631062C0627062A002006270644062C0648062F0629002006270644063906270644064A0629061B0020064A06450643064600200641062A062D00200648062B0627062606420020005000440046002006270644064506460634062306290020062806270633062A062E062F062706450020004100630072006F0062006100740020064800410064006F006200650020005200650061006400650072002006250635062F0627063100200035002E0030002006480627064406250635062F062706310627062A0020062706440623062D062F062B002E0635062F0627063100200035002E0030002006480627064406250635062F062706310627062A0020062706440623062D062F062B002E>
/BGR <FEFF04180437043f043e043b043704320430043904420435002004420435043704380020043d0430044104420440043e0439043a0438002c00200437043000200434043000200441044a0437043404300432043004420435002000410064006f00620065002000500044004600200434043e043a0443043c0435043d04420438002c0020043c0430043a04410438043c0430043b043d043e0020043f044004380433043e04340435043d04380020043704300020043204380441043e043a043e043a0430044704350441044204320435043d0020043f04350447043004420020043704300020043f044004350434043f0435044704300442043d04300020043f043e04340433043e0442043e0432043a0430002e002000200421044a04370434043004340435043d043804420435002000500044004600200434043e043a0443043c0435043d044204380020043c043e0433043004420020043404300020044104350020043e0442043204300440044f0442002004410020004100630072006f00620061007400200438002000410064006f00620065002000520065006100640065007200200035002e00300020043800200441043b0435043404320430044904380020043204350440044104380438002e>
/CHS <FEFF4f7f75288fd94e9b8bbe5b9a521b5efa7684002000410064006f006200650020005000440046002065876863900275284e8e9ad88d2891cf76845370524d53705237300260a853ef4ee54f7f75280020004100630072006f0062006100740020548c002000410064006f00620065002000520065006100640065007200200035002e003000204ee553ca66f49ad87248672c676562535f00521b5efa768400200050004400460020658768633002>
/CHT <FEFF4f7f752890194e9b8a2d7f6e5efa7acb7684002000410064006f006200650020005000440046002065874ef69069752865bc9ad854c18cea76845370524d5370523786557406300260a853ef4ee54f7f75280020004100630072006f0062006100740020548c002000410064006f00620065002000520065006100640065007200200035002e003000204ee553ca66f49ad87248672c4f86958b555f5df25efa7acb76840020005000440046002065874ef63002>
/CZE <FEFF005400610074006f0020006e006100730074006100760065006e00ed00200070006f0075017e0069006a007400650020006b0020007600790074007600e101590065006e00ed00200064006f006b0075006d0065006e0074016f002000410064006f006200650020005000440046002c0020006b00740065007200e90020007300650020006e0065006a006c00e90070006500200068006f006400ed002000700072006f0020006b00760061006c00690074006e00ed0020007400690073006b00200061002000700072006500700072006500730073002e002000200056007900740076006f01590065006e00e900200064006f006b0075006d0065006e007400790020005000440046002000620075006400650020006d006f017e006e00e90020006f007400650076015900ed007400200076002000700072006f006700720061006d0065006300680020004100630072006f00620061007400200061002000410064006f00620065002000520065006100640065007200200035002e0030002000610020006e006f0076011b006a016100ed00630068002e>
/DAN <FEFF004200720075006700200069006e0064007300740069006c006c0069006e006700650072006e0065002000740069006c0020006100740020006f007000720065007400740065002000410064006f006200650020005000440046002d0064006f006b0075006d0065006e007400650072002c0020006400650072002000620065006400730074002000650067006e006500720020007300690067002000740069006c002000700072006500700072006500730073002d007500640073006b007200690076006e0069006e00670020006100660020006800f8006a0020006b00760061006c0069007400650074002e0020004400650020006f007000720065007400740065006400650020005000440046002d0064006f006b0075006d0065006e0074006500720020006b0061006e002000e50062006e00650073002000690020004100630072006f00620061007400200065006c006c006500720020004100630072006f006200610074002000520065006100640065007200200035002e00300020006f00670020006e0079006500720065002e>
/DEU <FEFF00560065007200770065006e00640065006e0020005300690065002000640069006500730065002000450069006e007300740065006c006c0075006e00670065006e0020007a0075006d002000450072007300740065006c006c0065006e00200076006f006e002000410064006f006200650020005000440046002d0044006f006b0075006d0065006e00740065006e002c00200076006f006e002000640065006e0065006e002000530069006500200068006f006300680077006500720074006900670065002000500072006500700072006500730073002d0044007200750063006b0065002000650072007a0065007500670065006e0020006d00f60063006800740065006e002e002000450072007300740065006c006c007400650020005000440046002d0044006f006b0075006d0065006e007400650020006b00f6006e006e0065006e0020006d006900740020004100630072006f00620061007400200075006e0064002000410064006f00620065002000520065006100640065007200200035002e00300020006f0064006500720020006800f600680065007200200067006500f600660066006e00650074002000770065007200640065006e002e>
/ESP <FEFF005500740069006c0069006300650020006500730074006100200063006f006e0066006900670075007200610063006900f3006e0020007000610072006100200063007200650061007200200064006f00630075006d0065006e0074006f00730020005000440046002000640065002000410064006f0062006500200061006400650063007500610064006f00730020007000610072006100200069006d0070007200650073006900f3006e0020007000720065002d0065006400690074006f007200690061006c00200064006500200061006c00740061002000630061006c0069006400610064002e002000530065002000700075006500640065006e00200061006200720069007200200064006f00630075006d0065006e0074006f00730020005000440046002000630072006500610064006f007300200063006f006e0020004100630072006f006200610074002c002000410064006f00620065002000520065006100640065007200200035002e003000200079002000760065007200730069006f006e0065007300200070006f00730074006500720069006f007200650073002e>
/ETI <FEFF004b00610073007500740061006700650020006e0065006900640020007300e4007400740065006900640020006b00760061006c006900740065006500740073006500200074007200fc006b006900650065006c007300650020007000720069006e00740069006d0069007300650020006a0061006f006b007300200073006f00620069006c0069006b0065002000410064006f006200650020005000440046002d0064006f006b0075006d0065006e00740069006400650020006c006f006f006d006900730065006b0073002e00200020004c006f006f0064007500640020005000440046002d0064006f006b0075006d0065006e00740065002000730061006100740065002000610076006100640061002000700072006f006700720061006d006d006900640065006700610020004100630072006f0062006100740020006e0069006e0067002000410064006f00620065002000520065006100640065007200200035002e00300020006a00610020007500750065006d006100740065002000760065007200730069006f006f006e00690064006500670061002e000d000a>
/FRA <FEFF005500740069006c006900730065007a00200063006500730020006f007000740069006f006e00730020006100660069006e00200064006500200063007200e900650072002000640065007300200064006f00630075006d0065006e00740073002000410064006f00620065002000500044004600200070006f0075007200200075006e00650020007100750061006c0069007400e90020006400270069006d007000720065007300730069006f006e00200070007200e9007000720065007300730065002e0020004c0065007300200064006f00630075006d0065006e00740073002000500044004600200063007200e900e90073002000700065007500760065006e0074002000ea0074007200650020006f007500760065007200740073002000640061006e00730020004100630072006f006200610074002c002000610069006e00730069002000710075002700410064006f00620065002000520065006100640065007200200035002e0030002000650074002000760065007200730069006f006e007300200075006c007400e90072006900650075007200650073002e>
/GRE <FEFF03a703c103b703c303b903bc03bf03c003bf03b903ae03c303c403b5002003b103c503c403ad03c2002003c403b903c2002003c103c503b803bc03af03c303b503b903c2002003b303b903b1002003bd03b1002003b403b703bc03b903bf03c503c103b303ae03c303b503c403b5002003ad03b303b303c103b103c603b1002000410064006f006200650020005000440046002003c003bf03c5002003b503af03bd03b103b9002003ba03b103c42019002003b503be03bf03c703ae03bd002003ba03b103c403ac03bb03bb03b703bb03b1002003b303b903b1002003c003c103bf002d03b503ba03c403c503c003c903c403b903ba03ad03c2002003b503c103b303b103c303af03b503c2002003c503c803b703bb03ae03c2002003c003bf03b903cc03c403b703c403b103c2002e0020002003a403b10020005000440046002003ad03b303b303c103b103c603b1002003c003bf03c5002003ad03c703b503c403b5002003b403b703bc03b903bf03c503c103b303ae03c303b503b9002003bc03c003bf03c103bf03cd03bd002003bd03b1002003b103bd03bf03b903c703c403bf03cd03bd002003bc03b5002003c403bf0020004100630072006f006200610074002c002003c403bf002000410064006f00620065002000520065006100640065007200200035002e0030002003ba03b103b9002003bc03b503c403b103b303b503bd03ad03c303c403b503c103b503c2002003b503ba03b403cc03c303b503b903c2002e>
/HEB <FEFF05D405E905EA05DE05E905D5002005D105D405D205D305E805D505EA002005D005DC05D4002005DB05D305D9002005DC05D905E605D505E8002005DE05E105DE05DB05D9002000410064006F006200650020005000440046002005D405DE05D505EA05D005DE05D905DD002005DC05D405D305E405E105EA002005E705D305DD002D05D305E405D505E1002005D005D905DB05D505EA05D905EA002E002005DE05E105DE05DB05D90020005000440046002005E905E005D505E605E805D5002005E005D905EA05E005D905DD002005DC05E405EA05D905D705D4002005D105D005DE05E605E205D505EA0020004100630072006F006200610074002005D5002D00410064006F00620065002000520065006100640065007200200035002E0030002005D505D205E805E105D005D505EA002005DE05EA05E705D305DE05D505EA002005D905D505EA05E8002E05D005DE05D905DD002005DC002D005000440046002F0058002D0033002C002005E205D905D905E005D5002005D105DE05D305E805D905DA002005DC05DE05E905EA05DE05E9002005E905DC0020004100630072006F006200610074002E002005DE05E105DE05DB05D90020005000440046002005E905E005D505E605E805D5002005E005D905EA05E005D905DD002005DC05E405EA05D905D705D4002005D105D005DE05E605E205D505EA0020004100630072006F006200610074002005D5002D00410064006F00620065002000520065006100640065007200200035002E0030002005D505D205E805E105D005D505EA002005DE05EA05E705D305DE05D505EA002005D905D505EA05E8002E>
/HRV (Za stvaranje Adobe PDF dokumenata najpogodnijih za visokokvalitetni ispis prije tiskanja koristite ove postavke. Stvoreni PDF dokumenti mogu se otvoriti Acrobat i Adobe Reader 5.0 i kasnijim verzijama.)
/HUN <FEFF004b0069007600e1006c00f30020006d0069006e0151007300e9006701710020006e0079006f006d00640061006900200065006c0151006b00e90073007a00ed007401510020006e0079006f006d00740061007400e100730068006f007a0020006c006500670069006e006b00e1006200620020006d0065006700660065006c0065006c0151002000410064006f00620065002000500044004600200064006f006b0075006d0065006e00740075006d006f006b0061007400200065007a0065006b006b0065006c0020006100200062006500e1006c006c00ed007400e10073006f006b006b0061006c0020006b00e90073007a00ed0074006800650074002e0020002000410020006c00e90074007200650068006f007a006f00740074002000500044004600200064006f006b0075006d0065006e00740075006d006f006b00200061007a0020004100630072006f006200610074002000e9007300200061007a002000410064006f00620065002000520065006100640065007200200035002e0030002c0020007600610067007900200061007a002000610074007400f3006c0020006b00e9007301510062006200690020007600650072007a006900f3006b006b0061006c0020006e00790069007400680061007400f3006b0020006d00650067002e>
/ITA <FEFF005500740069006c0069007a007a006100720065002000710075006500730074006500200069006d0070006f007300740061007a0069006f006e00690020007000650072002000630072006500610072006500200064006f00630075006d0065006e00740069002000410064006f00620065002000500044004600200070006900f900200061006400610074007400690020006100200075006e00610020007000720065007300740061006d0070006100200064006900200061006c007400610020007100750061006c0069007400e0002e0020004900200064006f00630075006d0065006e007400690020005000440046002000630072006500610074006900200070006f00730073006f006e006f0020006500730073006500720065002000610070006500720074006900200063006f006e0020004100630072006f00620061007400200065002000410064006f00620065002000520065006100640065007200200035002e003000200065002000760065007200730069006f006e006900200073007500630063006500730073006900760065002e>
/JPN <FEFF9ad854c18cea306a30d730ea30d730ec30b951fa529b7528002000410064006f0062006500200050004400460020658766f8306e4f5c6210306b4f7f75283057307e305930023053306e8a2d5b9a30674f5c62103055308c305f0020005000440046002030d530a130a430eb306f3001004100630072006f0062006100740020304a30883073002000410064006f00620065002000520065006100640065007200200035002e003000204ee5964d3067958b304f30533068304c3067304d307e305930023053306e8a2d5b9a306b306f30d530a930f330c8306e57cb30818fbc307f304c5fc59808306730593002>
/KOR <FEFFc7740020c124c815c7440020c0acc6a9d558c5ec0020ace0d488c9c80020c2dcd5d80020c778c1c4c5d00020ac00c7a50020c801d569d55c002000410064006f0062006500200050004400460020bb38c11cb97c0020c791c131d569b2c8b2e4002e0020c774b807ac8c0020c791c131b41c00200050004400460020bb38c11cb2940020004100630072006f0062006100740020bc0f002000410064006f00620065002000520065006100640065007200200035002e00300020c774c0c1c5d0c11c0020c5f40020c2180020c788c2b5b2c8b2e4002e>
/LTH <FEFF004e006100750064006f006b0069007400650020016100690075006f007300200070006100720061006d006500740072007500730020006e006f0072011700640061006d00690020006b0075007200740069002000410064006f00620065002000500044004600200064006f006b0075006d0065006e007400750073002c0020006b00750072006900650020006c0061006200690061007500730069006100690020007000720069007400610069006b007900740069002000610075006b01610074006f00730020006b006f006b007900620117007300200070006100720065006e006700740069006e00690061006d00200073007000610075007300640069006e0069006d00750069002e0020002000530075006b0075007200740069002000500044004600200064006f006b0075006d0065006e007400610069002000670061006c006900200062016b007400690020006100740069006400610072006f006d00690020004100630072006f006200610074002000690072002000410064006f00620065002000520065006100640065007200200035002e0030002000610072002000760117006c00650073006e0117006d00690073002000760065007200730069006a006f006d00690073002e>
/LVI <FEFF0049007a006d0061006e0074006f006a00690065007400200161006f00730020006900650073007400610074012b006a0075006d00750073002c0020006c0061006900200076006500690064006f00740075002000410064006f00620065002000500044004600200064006f006b0075006d0065006e007400750073002c0020006b006100730020006900720020012b00700061016100690020007000690065006d01130072006f00740069002000610075006700730074006100730020006b00760061006c0069007401010074006500730020007000690072006d007300690065007300700069006501610061006e006100730020006400720075006b00610069002e00200049007a0076006500690064006f006a006900650074002000500044004600200064006f006b0075006d0065006e007400750073002c0020006b006f002000760061007200200061007400760113007200740020006100720020004100630072006f00620061007400200075006e002000410064006f00620065002000520065006100640065007200200035002e0030002c0020006b0101002000610072012b00200074006f0020006a00610075006e0101006b0101006d002000760065007200730069006a0101006d002e>
/NLD (Gebruik deze instellingen om Adobe PDF-documenten te maken die zijn geoptimaliseerd voor prepress-afdrukken van hoge kwaliteit. De gemaakte PDF-documenten kunnen worden geopend met Acrobat en Adobe Reader 5.0 en hoger.)
/NOR <FEFF004200720075006b00200064006900730073006500200069006e006e007300740069006c006c0069006e00670065006e0065002000740069006c002000e50020006f0070007000720065007400740065002000410064006f006200650020005000440046002d0064006f006b0075006d0065006e00740065007200200073006f006d00200065007200200062006500730074002000650067006e0065007400200066006f00720020006600f80072007400720079006b006b0073007500740073006b00720069006600740020006100760020006800f800790020006b00760061006c0069007400650074002e0020005000440046002d0064006f006b0075006d0065006e00740065006e00650020006b0061006e002000e50070006e00650073002000690020004100630072006f00620061007400200065006c006c00650072002000410064006f00620065002000520065006100640065007200200035002e003000200065006c006c00650072002000730065006e006500720065002e>
/POL <FEFF0055007300740061007700690065006e0069006100200064006f002000740077006f0072007a0065006e0069006100200064006f006b0075006d0065006e007400f300770020005000440046002000700072007a0065007a006e00610063007a006f006e00790063006800200064006f002000770079006400720075006b00f30077002000770020007700790073006f006b00690065006a0020006a0061006b006f015b00630069002e002000200044006f006b0075006d0065006e0074007900200050004400460020006d006f017c006e00610020006f007400770069006500720061010700200077002000700072006f006700720061006d006900650020004100630072006f00620061007400200069002000410064006f00620065002000520065006100640065007200200035002e0030002000690020006e006f00770073007a0079006d002e>
/PTB <FEFF005500740069006c0069007a006500200065007300730061007300200063006f006e00660069006700750072006100e700f50065007300200064006500200066006f0072006d00610020006100200063007200690061007200200064006f00630075006d0065006e0074006f0073002000410064006f0062006500200050004400460020006d00610069007300200061006400650071007500610064006f00730020007000610072006100200070007200e9002d0069006d0070007200650073007300f50065007300200064006500200061006c007400610020007100750061006c00690064006100640065002e0020004f007300200064006f00630075006d0065006e0074006f00730020005000440046002000630072006900610064006f007300200070006f00640065006d0020007300650072002000610062006500720074006f007300200063006f006d0020006f0020004100630072006f006200610074002000650020006f002000410064006f00620065002000520065006100640065007200200035002e0030002000650020007600650072007300f50065007300200070006f00730074006500720069006f007200650073002e>
/RUM <FEFF005500740069006c0069007a00610163006900200061006300650073007400650020007300650074010300720069002000700065006e007400720075002000610020006300720065006100200064006f00630075006d0065006e00740065002000410064006f006200650020005000440046002000610064006500630076006100740065002000700065006e0074007200750020007400690070010300720069007200650061002000700072006500700072006500730073002000640065002000630061006c006900740061007400650020007300750070006500720069006f006100720103002e002000200044006f00630075006d0065006e00740065006c00650020005000440046002000630072006500610074006500200070006f00740020006600690020006400650073006300680069007300650020006300750020004100630072006f006200610074002c002000410064006f00620065002000520065006100640065007200200035002e00300020015f00690020007600650072007300690075006e0069006c006500200075006c0074006500720069006f006100720065002e>
/RUS <FEFF04180441043f043e043b044c04370443043904420435002004340430043d043d044b04350020043d0430044104420440043e0439043a043800200434043b044f00200441043e043704340430043d0438044f00200434043e043a0443043c0435043d0442043e0432002000410064006f006200650020005000440046002c0020043c0430043a04410438043c0430043b044c043d043e0020043f043e04340445043e0434044f04490438044500200434043b044f00200432044b0441043e043a043e043a0430044704350441044204320435043d043d043e0433043e00200434043e043f0435044704300442043d043e0433043e00200432044b0432043e04340430002e002000200421043e043704340430043d043d044b04350020005000440046002d0434043e043a0443043c0435043d0442044b0020043c043e0436043d043e0020043e0442043a0440044b043204300442044c002004410020043f043e043c043e0449044c044e0020004100630072006f00620061007400200438002000410064006f00620065002000520065006100640065007200200035002e00300020043800200431043e043b043504350020043f043e04370434043d043804450020043204350440044104380439002e>
/SKY <FEFF0054006900650074006f0020006e006100730074006100760065006e0069006100200070006f0075017e0069007400650020006e00610020007600790074007600e100720061006e0069006500200064006f006b0075006d0065006e0074006f0076002000410064006f006200650020005000440046002c0020006b0074006f007200e90020007300610020006e0061006a006c0065007001610069006500200068006f0064006900610020006e00610020006b00760061006c00690074006e00fa00200074006c0061010d00200061002000700072006500700072006500730073002e00200056007900740076006f00720065006e00e900200064006f006b0075006d0065006e007400790020005000440046002000620075006400650020006d006f017e006e00e90020006f00740076006f00720069016500200076002000700072006f006700720061006d006f006300680020004100630072006f00620061007400200061002000410064006f00620065002000520065006100640065007200200035002e0030002000610020006e006f0076016100ed00630068002e>
/SLV <FEFF005400650020006e006100730074006100760069007400760065002000750070006f0072006100620069007400650020007a00610020007500730074007600610072006a0061006e006a006500200064006f006b0075006d0065006e0074006f0076002000410064006f006200650020005000440046002c0020006b006900200073006f0020006e0061006a007000720069006d00650072006e0065006a016100690020007a00610020006b0061006b006f0076006f00730074006e006f0020007400690073006b0061006e006a00650020007300200070007200690070007200610076006f0020006e00610020007400690073006b002e00200020005500730074007600610072006a0065006e006500200064006f006b0075006d0065006e0074006500200050004400460020006a00650020006d006f0067006f010d00650020006f0064007000720065007400690020007a0020004100630072006f00620061007400200069006e002000410064006f00620065002000520065006100640065007200200035002e003000200069006e0020006e006f00760065006a01610069006d002e>
/SUO <FEFF004b00e40079007400e40020006e00e40069007400e4002000610073006500740075006b007300690061002c0020006b0075006e0020006c0075006f00740020006c00e400680069006e006e00e4002000760061006100740069007600610061006e0020007000610069006e006100740075006b00730065006e002000760061006c006d0069007300740065006c00750074007900f6006800f6006e00200073006f00700069007600690061002000410064006f0062006500200050004400460020002d0064006f006b0075006d0065006e007400740065006a0061002e0020004c0075006f0064007500740020005000440046002d0064006f006b0075006d0065006e00740069007400200076006f0069006400610061006e0020006100760061007400610020004100630072006f0062006100740069006c006c00610020006a0061002000410064006f00620065002000520065006100640065007200200035002e0030003a006c006c00610020006a006100200075007500640065006d006d0069006c006c0061002e>
/SVE <FEFF0041006e007600e4006e00640020006400650020006800e4007200200069006e0073007400e4006c006c006e0069006e006700610072006e00610020006f006d002000640075002000760069006c006c00200073006b006100700061002000410064006f006200650020005000440046002d0064006f006b0075006d0065006e007400200073006f006d002000e400720020006c00e4006d0070006c0069006700610020006600f60072002000700072006500700072006500730073002d007500740073006b00720069006600740020006d006500640020006800f600670020006b00760061006c0069007400650074002e002000200053006b006100700061006400650020005000440046002d0064006f006b0075006d0065006e00740020006b0061006e002000f600700070006e00610073002000690020004100630072006f0062006100740020006f00630068002000410064006f00620065002000520065006100640065007200200035002e00300020006f00630068002000730065006e006100720065002e>
/TUR <FEFF005900fc006b00730065006b0020006b0061006c006900740065006c0069002000f6006e002000790061007a006401310072006d00610020006200610073006b013100730131006e006100200065006e0020006900790069002000750079006100620069006c006500630065006b002000410064006f006200650020005000440046002000620065006c00670065006c0065007200690020006f006c0075015f007400750072006d0061006b0020006900e70069006e00200062007500200061007900610072006c0061007201310020006b0075006c006c0061006e0131006e002e00200020004f006c0075015f0074007500720075006c0061006e0020005000440046002000620065006c00670065006c0065007200690020004100630072006f006200610074002000760065002000410064006f00620065002000520065006100640065007200200035002e003000200076006500200073006f006e0072006100730131006e00640061006b00690020007300fc007200fc006d006c00650072006c00650020006100e70131006c006100620069006c00690072002e>
/UKR <FEFF04120438043a043e0440043804410442043e043204430439044204350020044604560020043f043004400430043c043504420440043800200434043b044f0020044104420432043e04400435043d043d044f00200434043e043a0443043c0435043d044204560432002000410064006f006200650020005000440046002c0020044f043a04560020043d04300439043a04400430044904350020043f045604340445043e0434044f0442044c00200434043b044f0020043204380441043e043a043e044f043a04560441043d043e0433043e0020043f0435044004350434043404400443043a043e0432043e0433043e0020043404400443043a0443002e00200020042104420432043e04400435043d045600200434043e043a0443043c0435043d0442043800200050004400460020043c043e0436043d04300020043204560434043a0440043804420438002004430020004100630072006f006200610074002004420430002000410064006f00620065002000520065006100640065007200200035002e0030002004300431043e0020043f04560437043d04560448043e04570020043204350440044104560457002e>
/ENU (Use these settings to create Adobe PDF documents best suited for high-quality prepress printing. Created PDF documents can be opened with Acrobat and Adobe Reader 5.0 and later.)
>>
/Namespace [
(Adobe)
(Common)
(1.0)
]
/OtherNamespaces [
<<
/AsReaderSpreads false
/CropImagesToFrames true
/ErrorControl /WarnAndContinue
/FlattenerIgnoreSpreadOverrides false
/IncludeGuidesGrids false
/IncludeNonPrinting false
/IncludeSlug false
/Namespace [
(Adobe)
(InDesign)
(4.0)
]
/OmitPlacedBitmaps false
/OmitPlacedEPS false
/OmitPlacedPDF false
/SimulateOverprint /Legacy
>>
<<
/AddBleedMarks false
/AddColorBars false
/AddCropMarks false
/AddPageInfo false
/AddRegMarks false
/ConvertColors /ConvertToCMYK
/DestinationProfileName ()
/DestinationProfileSelector /DocumentCMYK
/Downsample16BitImages true
/FlattenerPreset <<
/PresetSelector /MediumResolution
>>
/FormElements false
/GenerateStructure false
/IncludeBookmarks false
/IncludeHyperlinks false
/IncludeInteractive false
/IncludeLayers false
/IncludeProfiles false
/MultimediaHandling /UseObjectSettings
/Namespace [
(Adobe)
(CreativeSuite)
(2.0)
]
/PDFXOutputIntentProfileSelector /DocumentCMYK
/PreserveEditing true
/UntaggedCMYKHandling /LeaveUntagged
/UntaggedRGBHandling /UseDocumentProfile
/UseDocumentBleed false
>>
]
>> setdistillerparams
<<
/HWResolution [2400 2400]
/PageSize [612.000 792.000]
>> setpagedevice
|
| id | nasplib_isofts_kiev_ua-123456789-82919 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 0130-5395 |
| language | English |
| last_indexed | 2025-12-07T13:13:54Z |
| publishDate | 2011 |
| publisher | Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України |
| record_format | dspace |
| spelling | Favier, A. de Givry, S. Jégou, P. 2015-06-11T20:00:01Z 2015-06-11T20:00:01Z 2011 Solution Counting for CSP and SAT with Large Tree-Width / A. Favier, S. de Givry, Ph. Jégou // Управляющие системы и машины. — 2011. — № 2. — С. 4-13, 70. — Бібліогр.: 36 назв. — англ. 0130-5395 https://nasplib.isofts.kiev.ua/handle/123456789/82919 519.157 Рассмотрена проблема подсчета количества решений задачи совместимости ограничений (Constraint Satisfaction Problem). Для ее решения был адаптирован метод обратного прослеживания с ацикличным представлением графа ограничений (Backtracking with Tree-Decomposition). Предложен точный алгоритм, сложность которого экспоненциально зависит от ширины дерева, и приближенный алгоритм, экспоненциально зависящий от размера максимальной клики. The problem of counting the number of solutions of a CSP is considered. For solving the problem the Backtracking with a Tree-Decomposition method was adapted. The exact algorithm is suggested which has the worst-time complexity exponential in a tree width, as well as iterative algorithm that has computational complexity exponential in a maximum clique size. Розглянуто проблему підрахунку кількості розв’язків задачі сумісності обмежень (Constraint Satisfaction Problem). Для її розв’язку було адаптовано метод зворотного простеження з ациклічним поданням графа обмежень (Backtracking with Tree-Decomposition). Запропоновано точний алгоритм, складність якого експоненційно залежить від ширини дерева, і наближений алгоритм, експоненційно залежний від розміру максимальної кліки. en Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України Управляющие системы и машины Оптимизационные задачи структурного распознавания образов Solution Counting for CSP and SAT with Large Tree-Width Подсчет количества решений задач CSP и SAT на деревьях большой ширины Підрахунок кількості розв’язків задач CSP та SAT на деревах великої ширини Article published earlier |
| spellingShingle | Solution Counting for CSP and SAT with Large Tree-Width Favier, A. de Givry, S. Jégou, P. Оптимизационные задачи структурного распознавания образов |
| title | Solution Counting for CSP and SAT with Large Tree-Width |
| title_alt | Подсчет количества решений задач CSP и SAT на деревьях большой ширины Підрахунок кількості розв’язків задач CSP та SAT на деревах великої ширини |
| title_full | Solution Counting for CSP and SAT with Large Tree-Width |
| title_fullStr | Solution Counting for CSP and SAT with Large Tree-Width |
| title_full_unstemmed | Solution Counting for CSP and SAT with Large Tree-Width |
| title_short | Solution Counting for CSP and SAT with Large Tree-Width |
| title_sort | solution counting for csp and sat with large tree-width |
| topic | Оптимизационные задачи структурного распознавания образов |
| topic_facet | Оптимизационные задачи структурного распознавания образов |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/82919 |
| work_keys_str_mv | AT faviera solutioncountingforcspandsatwithlargetreewidth AT degivrys solutioncountingforcspandsatwithlargetreewidth AT jegoup solutioncountingforcspandsatwithlargetreewidth AT faviera podsčetkoličestvarešeniizadačcspisatnaderevʹâhbolʹšoiširiny AT degivrys podsčetkoličestvarešeniizadačcspisatnaderevʹâhbolʹšoiširiny AT jegoup podsčetkoličestvarešeniizadačcspisatnaderevʹâhbolʹšoiširiny AT faviera pídrahunokkílʹkostírozvâzkívzadačcsptasatnaderevahvelikoíširini AT degivrys pídrahunokkílʹkostírozvâzkívzadačcsptasatnaderevahvelikoíširini AT jegoup pídrahunokkílʹkostírozvâzkívzadačcsptasatnaderevahvelikoíširini |