- Create graph in app
- Input desired EMSO formula
- Click 'Run' and observe output

During

During

During

A fast EMSO-solver for graphs of small treewidth.

Sequoia solves MSO-definable problems on graphs of small treewidth. It is based on a game-theoretic proof of Courcelle's Theorem described in this paper (PDF preprint). See also this paper for an experimental comparison to CPLEX.

You can try it out on this page below.

Sequoia is Open Source and licensed under the Apache License 2.0.

The source code is available from Github.

Click on the applet below to create a graph. Input a formula on the textfield below, then click on 'Run!'. Your output will be shown in the output frame at the bottom.

- Bipartiteness - Witness or None
- Connectedness - None only
- Vertex Cover - MinCardSet or MinCard
- Independent Set - MaxCardSet or MaxCard
- 3-Colorability - Witness or None
- Clique - MaxCardSet or MaxCard
- Dominating Set - MinCardSet or MinCard
- Connected Dominating Set - MinCardSet or MinCard
- Distance-2 Dominating Set - MinCardSet or MinCard