Université d’Artois - CRIL
Industrial and Systems Engineering Department, UW Madison
October 27, 2023
where is a polynomial.
Observation: may be assumed to be multilinear since over
Bad news: Solving BPO is NP-hard.
Intuition: a polynomial can encode many things:
BPO is a non-linear optimization problem.
Make it linear so that we can use LP solvers!
Integer Linear Program solvers can now solve it!
is a Boolean function on variables .
An assignment satisfies iff .
Example: Boolean function on :
Represented as a formula or by
For and consider:
where is a semi-ring
This is an optimization task!
For define: where
and on as:
We can use existing toolbox for AMC to solve BPO
How can we represent Boolean function:
So far we have seen: list every satisfying assignment of (aka Truth Table)
where is a literal or for some variable .
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.
Looking for tradeoffs between Truth Tables and CNFs!
Research has focused on factorized representation.
Data structure based on decision nodes to represent “ is even”.
Path for , and is accepting.
Previous data structure are Ordered Binary Decision Diagrams.
How many -matrices have a row full of ones?
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:
Exhaustive DPLL with Caching based on Shannon Expansion:
This scheme is parameterized by:
For many tasks, such as model counting, it is interesting to detect syntactic decomposable part of the formula, that is:
D4 is a top-down compiler as shown earlier:
|instance||d4 (s)||scip (s)|
is a hypergraph.
Exploit the structure of to solve BPO more efficiently.
Tree BPO: BPO problem where is a tree.
If has tree width then one can solve BPO in time .
If is -acyclic then one can solve BPO in time .
Dedicated algorithm for each class.
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 .
Is there a connection?
For define: where
can be encoded as the conjunction of:
is naturally encoded as a CNF that preserves tree width.
Every known tractability for BPO can be recovered in our framework as follows:
And we get new tractability results!
KC approach very versatile:
Connection between BPO and Boolean functions:
KC only exploits combinatorics of the underlying Boolean function. How could we mix existing more algebraic techniques?