Implementing Coucelle‘s theorem It’s about implementing a…
0 reactions
Implementing Coucelle‘s theorem
It’s about implementing a prompt for asking something in monadic second order logic (given as ascii string) about a graph of bounded treewidth and decide a property in linear time .
It will take some months,perhaps a year to stick parts together.
We have to connect this chain. Many parts are already implemented:
\- Parser for queries in monadic second order logic given in ascii, say.
\- Computing a tree decomposition of a graph using Bodlaenders linear time algorithm. It’s known to be infeasible. Someone should check this once again as phd topic.
\- Actually, its better to use nonlinear algorithms here. Consider this solved and being practical.
\- a tree decomposition allows to decide properties of the underlying graph by deciding it on local, distance-related, smaller parts.
\-monadic second order logic (MSO) restricts SOL sets to be sets covering k-neighborhoods of vertices.
\- monadic second order logic can be defined by an automaton. I dont remember details, but its straighforward.
\- you can expand a tree decomposition (operating on the power set of a graph) to a hypertree decomposition used to having finite state monadic second order logic automatons as vertices and evaluate these automatons as usual.
Anyone interested ?
#technology
It’s about implementing a prompt for asking something in monadic second order logic (given as ascii string) about a graph of bounded treewidth and decide a property in linear time .
It will take some months,perhaps a year to stick parts together.
We have to connect this chain. Many parts are already implemented:
\- Parser for queries in monadic second order logic given in ascii, say.
\- Computing a tree decomposition of a graph using Bodlaenders linear time algorithm. It’s known to be infeasible. Someone should check this once again as phd topic.
\- Actually, its better to use nonlinear algorithms here. Consider this solved and being practical.
\- a tree decomposition allows to decide properties of the underlying graph by deciding it on local, distance-related, smaller parts.
\-monadic second order logic (MSO) restricts SOL sets to be sets covering k-neighborhoods of vertices.
\- monadic second order logic can be defined by an automaton. I dont remember details, but its straighforward.
\- you can expand a tree decomposition (operating on the power set of a graph) to a hypertree decomposition used to having finite state monadic second order logic automatons as vertices and evaluate these automatons as usual.
Anyone interested ?
#technology
| 3,000 mlx | |
| 3 | |
| 0 |