A Knowledge Compilation Take on Binary Polynomial
Optimization
Florent Capelli joint work
with Alberto Del Pia and Silvia di Gregorio
Université d’Artois - CRIL
September 12, 2024
Binary Polynomial Optimization
Problem definition
Binary Polynomial Optimization problem:
where
is a polynomial.
Observation:
may be assumed to be multilinear since
over
where
Example
0
0
0
0
0
0
1
0
0
1
0
0
0
1
1
0
1
0
0
3
1
0
1
1
1
1
0
3
1
1
1
2
are maximal
Complexity of BPO
Bad news: Solving BPO is NP-hard.
Intuition: a polynomial can encode many things:
encodes
on
For a graph
,
with
vertices and
edges
iff
encodes a vertex cover of
is maximal at
iff
encodes a minimal vertex cover!
Solving BPO as ILP
BPO is a non-linear optimization problem.
Make it linear so that we can use LP solvers!
rewrites as:
such that
and
for
and
for
and
Integer Linear Program solvers can now solve
it!
They may stall on known-to-be easy
instances. Is there an alternative way?
BPO as a Boolean Function Problem
Boolean Function
is a Boolean function on variables
.
An assignmentsatisfies
iff
.
Example
x
y
z
0
0
0
0
0
1
0
1
0
0
1
1
1
1
1
Represented as a formula
or by
Weighted Boolean Function
For
and
consider:
Example
,
,
,
,
,
x
y
z
0
0
0
0
0
1
0
1
0
0
1
1
1
1
1
30
Algebraic Model Counting
where
is a semi-ring
That is:
commutative, associative
,
distributes over
:
.
Examples
Any fields, e.g.,
Arctic semi-ring:
AMC over
-semiring
This is an optimization task!
Example
,
,
,
,
,
x
y
z
0
0
0
0
0
1
0
1
0
0
1
1
1
1
1
9
Encoding BPO as Boolean function
Example:
,
and .
for every other values.
For every
we have
and
Example
For
:
if
then
hence
!
Formal encoding
For
define:
where
encodes
!
and
on
as:
and
for
.
BPO as a Boolean Function
over the
-semiring.
The underlying algorithmic toolbox is very different from ILP solvers
providing new insights.
We can use existing toolbox for AMC to solve BPO
theoretical results
AND practical results
Knowledge Compilation how to solve
AMC
Representing Boolean functions
How can we represent Boolean function:
So far we have seen: list every satisfying assignment of
(aka Truth Table)
Easy to manipulate since the representation is explicit
Not compact
CNF Formulas
where
is a literal
or
for some variable
.
Examples
The SAT Problem
CNF formulas are extremely simple yet can encode many interesting
problems.
Cook, Levin, 1971: The problem SAT of deciding
whether a CNF formula is satisfiable is
NP-complete.
Valiant 1979: The problem #SAT of counting the
satisfying assignment of a CNF formula is
#P-complete.
Very unlikely that efficient algorithms exists for solving SAT /
#SAT
Thriving community nevertheless addresses these problems in
practice
SAT Solver very efficient in many applications
Relevance of CNF formulas
Natural encoding: succinctly encodes many problems,
witnessed by the many existing industrial benchmarks.
Intractable for algebraic model counting
Looking for tradeoffs between Truth Tables and CNFs!
Circuit Based Representations
Research has focused on factorized representation.
An example
Data structure based on decision nodes to represent
“
is even”.
Path for
,
and
is accepting.
OBDDs
Previous data structure are Ordered Binary Decision
Diagrams.
Directed Acyclic graphs with one source
Sinks are labeled by
or
Internal nodes are decision nodes on a variable in
Variables tested in order.
Counting with OBDDs
How many
-matrices
have a row full of ones?
Tractability of OBDDs
This idea can be generalized to any OBDDs:
Let
be a function computed by an OBDD having
edges. We can compute
with
arithmetic operations.
Generalises to many tasks:
Evaluate
if probabilities
are given for each
Enumerate
Algebraic Model Counting on any semi-ring.
Back to BPO
where
and
otherwise
Solving BPO:
transform
into an OBDD
compute
via dynamic programming on the OBDD itself
A Knowledge Compiler for OBDD
Exhaustive DPLL with Caching based on Shannon
Expansion:
This scheme is parameterized by:
caching policy
branching heuristics
Exploiting decomposition
For many tasks, such as model counting, it is interesting to detect
syntactic decomposable part of the formula, that
is:
and
decDNNF: OBDD +
-gates
decomposable
Still allows for algebraic model counting via the identity
Compilers can be adapted to detect this rule.
The D4 compiler
D4 is a top-down compiler as shown earlier:
Use oracle calls to a SAT solver with clause
learning to cut branches and speed up later computation
Use heuristics to decompose the formula so that it
breaks into smaller connected components.
instance
d4 (s)
scip (s)
bernasconi.20.3
0.002
0.01
bernasconi.20.5
0.04
8.91
bernasconi.20.10
1.21
119.20
bernasconi.20.15
14.92
479.15
bernasconi.25.3
0.00
0.01
bernasconi.25.6
0.19
151.65
bernasconi.25.13
12.59
1 698.18
bernasconi.25.19
442.26
TIMEOUT
bernasconi.25.25
TIMEOUT
TIMEOUT
This only illustrates that the underlying structure
of Bernasconi instances is better addressed using heuristics from model
counting than the ILP approach.
Tractability results
Tractable classes of BPO
is a hypergraph.
Exploit the structure of
to solve BPO more efficiently.
A toy example
Tree BPO: BPO problem where
is a tree.
Example:
Many Known Tractable Classes
has tree width
:
BPO can be solved in time
.
is
-acyclic:
BPO can be solved in time
.
Dedicated algorithm for each class.
A strange symmetry
Very similar results from Boolean function literature:
If a CNF
has tree width
then one can construct a DNNF for
of size
.
If a CNF
is
-acyclic
then one can construct a DNNF for
of size
.
Is there a connection?
Encoding BPO as a CNF
For
define:
where
can be encoded as the conjunction of:
for every
is naturally encoded as a CNF
that preserves tree width.
Tractability of BPO via KC
Every known tractability for BPO can be recovered in our framework as
follows:
Encode
as a CNF formula
Transform
into a polynomial size tractable representation
using known results
Solve AMC on
And we get new tractability results for structure that where not
known to make BPO tractable.
Beyond BPO
KC approach very versatile:
Solve top-k BPO: find the
best solutions of
by finding the
best in the circuit
Solve BPO + Cardinality constraints:
where
by transforming the circuit
Solve pseudo BPO:
can contains monomial of the form
Conclusion
Connection between BPO and Boolean functions:
Recover known results and generalize them using the existing rich
literature
Seems to have practical relevance
Perspective:
KC only exploits combinatorics of the underlying
Boolean function. How could we mix existing more
algebraic techniques?