I strongly recommend the paper by Bixby, the "father" of CPLEX, that surveys not only on implementing aspects of the (revised) simplex algorithm: Robert E. Bixby, Solving Real-World Linear Programs: A Decade and More of Progress, Operations Research (50) 2002, 3-15.
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 ...
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)....
I think that Sage is the right thing for this task.
sage: G = digraphs.Circuit(40)
sage: G = G.lexicographic_product(G)
Other graph products and algorithms are available as well.
here is a new collaborative online Latex editor called WriteLatex that looks promising, as a near one-stop shop for many scientific writing needs/requirements.
works on mobile
has realtime preview
finds latex errors
allows add on latex libraries/styles
John Hammersley posted an announcement in tcs se meta ...
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 ...
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/ .
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 ...
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 ...
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/...
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 ...
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).