7

If $n \sim 10$ and $k$ is fixed, then you can even afford to go with an XP algorithm like the one we implemented for our Android app. The source code is here: TreewidthInspector, and for instance with $n \leq 13$ and $k \leq 4$ it terminates in less than a second. It's approximately 170 lines of code and it's GPL (or MIT or BSD or whatever you should need)....


5

LibTW can still be found. It's at http://www.treewidth.com/treewidth/ .


5

For $n\le150$ you can use the webservice over at http://treedecompositions.com/ to directly obtain and visualize a quick and reasonable decomposition, without having to compile or install anything.


5

The original algorithm of Lenstra (from 1983) has not been implemented AFAIK. Certainly, no open-source code is known to be available. Lovasz and Scarf proposed (in 1992) a generalized basis reduction algo that also solves IP in fixed dimensions, but avoids the ellipsoidal approximations required by Lenstra's algorithm. An implementation of this algo was ...


4

Yes, an example of a system that performs this task is T2. It does not solve the halting problem but instead it only attempts to solve certain special cases. A overview is at https://en.wikipedia.org/wiki/Microsoft_Terminator . The newest version of this system is at https://mmjb.github.io/T2/ .


4

Is there a tool which solves parametric games? Not that I am aware of (I am a co-author of GTE and help with Gambit). The best suggestion I have if you don't find such a tool (and I doubt one exists) is to do a parameter sweep and solve a bunch of individual instantiations and see what the resulting sets of equilibria say about $EQ()$. Gambit is very ...


4

A slow brute-force implementation of the graph crossing number was added to Sage in Sage Trac ticket 24216: Add crossing number of a graph which was closed 2018-01-05, and merged in Sage 8.2.beta3.


3

This kind of "laws" are usually labelled as Pareto principle, or 80–20 rule: Answering specifically your question(s) 1) This law is true in the real sense, or is just an observation, a presumption? This law is just an observation, and was explained more formally as a property of exponential distributions or power law. Then the observation is just the ...


2

You can get a square-root speed-up with a time-space tradeoff if you are working in $\mathbb{F}_2$. The matrix $M$ is a no-instance iff there exists a non-zero vector $v$ of Hamming weight $\le k$ (i.e., with at most $k$ non-zero coordinates) such that $Mv=0$. This is equivalent to saying that there exist $t,u$ of Hamming weight $\le k/2$ such that $Mt=Mu$ (...


2

I found a more recent (2014) paper on All-SAT at a VLSI conference, so it is definitely geared toward the practical side (which seems in tune with the OP's question here, albeit less so with cstheory.SE in general): "All-SAT using Minimal Blocking Clauses" by Yinlei Yu, Pramod Subramanyan, Nestan Tsiskaridze, Sharad Malik, VLSI Design 2014. doi:10.1109/...


2

You may also be interested in the more modern algorithms FlowCutter (GitHub) and the algorithms by Tamaki et al. (GitHub)


2

The website BeyondNP contains a good inventory of the existing tools to solve #SAT (and other related hard problems on CNF formulas). You may also find a list of tools for approximate model counting and knowledge compilation (the task of transforming the CNF into a hopefully succinct data structure that often supports polynomial time model counting). You ...


1

Here is one called tensorCSP and based on a tool called tensor networks. It is explained in this paper.


Only top voted, non community-wiki answers of a minimum length are eligible