# Tag Info

14

You are looking for an ALL-SAT or all solutions SAT solver. This is a different problem from #SAT. You do not have to enumerate all solutions to count them. I do not know of a tool that solves your problem because people add these algorithms on top of existing SAT solvers but rarely seem to release these extensions. Two papers that should help you in ...

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

Ashish Sabharwal lists some software (e.g., SampleCount, ApproxCount, and more) for this on his web page. I haven't tried any of these.

2

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

2

I recently discovered sharelatex.com and used it with my collaborator to coauthor a paper. I liked it so much my current plan is to use it for all my projects. Some notable features: Real-time in-browser TeXing (like Google Docs, but made for TeX, syntax-highlighting and all). In-browser compiling and PDF viewing Supports projects with multiple files Has a ...

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