27
votes
Theoretical explanations for practical success of SAT solvers?
I am assuming that you are referring to CDCL SAT solvers on benchmark data sets
like those used in the SAT Competition.
These programs are based on many heuristics and lots of optimization.
There were ...
- 21.5k
24
votes
Theoretical explanations for practical success of SAT solvers?
I am typing this quite quickly due to severe time constraints (and didn't even get to responding earlier for the same reason), but I thought I would try to at least chip in with my two cents.
I ...
- 504
19
votes
Theoretical explanations for practical success of SAT solvers?
I'm not an expert in this area, but I think the random SAT / phase transition stuff is more or less completely unrelated to the industrial/practical applications stuff.
E.g., the very good solvers ...
- 1,801
18
votes
Theoretical explanations for practical success of SAT solvers?
Let me add my two cents of understanding to this, even though I've never actually worked in the area.
You're asking one of two questions, "what are all the known approaches to proving theoretical ...
- 803
17
votes
Theoretical explanations for practical success of SAT solvers?
There is a paper "Relating Proof Complexity Measures and Practical Hardness of SAT" by Matti Järvisalo, Arie Matsliah, Jakob Nordström, and Stanislav Živný in CP '12 that attempts to link the hardness ...
- 4,631
16
votes
Accepted
Are there any heuristic-free NP complete problems?
See Josh Grochow's answer to Poly time superset of NP complete language with infinitely many strings excluded from it. According to that answer, under some natural cryptographic assumptions, for every ...
- 50.9k
9
votes
What is the maximum number of stable marriages for an instance of the Stable Marriage Problem?
An exponential upper bound has been given in Anna R. Karlin, Shayan Oveis Gharan, Robbie Weber: A Simply Exponential Upper Bound on the Maximum Number of Stable Matchings.
Later the base of the ...
- 13.9k
5
votes
List of NP-hard problems, where there is active research in practical heuristics
MaxSAT - people actually care about this because SAT solvers are so well-developed that often the best route for your favorite NP optimization problem in practice is to reduce it to MaxSAT and then ...
5
votes
Accepted
Are there any heuristics that works solely on graphs?
There are known pre-processing methods that rely solely on the graph representation itself (and not on any kind of geometric embedding) to establish good heuristics for A*. Perhaps the most well-known ...
- 131
4
votes
Good algorithms to solve ATSP
You can also transform the ATSP to TSP; the process requires doubling number of nodes (adding dummy cities).
http://www.sciencedirect.com/science/article/pii/0167637783900482
http://www.sciencedirect....
3
votes
Accepted
Understanding performance of QFBV SMT solvers
The short answer is no, we don't understand it. The long answer is yes, we have some bounds, but those bounds aren't very helpful. It's quite clear that the worst-case running time is exponential. ...
- 11.7k
3
votes
Finding smallest context free grammar that generates a set of sets
Define a language $L$ to be nicely-ordered if $L \subseteq a^*b^*c^*d^*\cdots$, i.e., in every word of $L$, the letters appear solely in lexicographic order.
Conjecture: the optimum is always ...
- 11.7k
2
votes
Accepted
Pathfinding search over a space with known changing costs
In general, finding least-cost paths with arbitrary time-dependent edge costs is NP-hard, assuming that either (a) waiting at nodes is forbidden and your costs are not FIFO-preserving (e.g., see here ...
- 131
2
votes
Accepted
Packing $n$ objects into $m$ bins whose size is variable
One simple "bad" input that needs to be considered for worst-case analysis of this problem is as follows.
Let $c=(\sqrt{17}-1)/2 \approx 1.56$.
There are three objects of size $c$, $1$, and $1$.
...
- 18.9k
2
votes
Practical/heuristic algorithm for multi set-cover
You'd have to tweak the limits (in particular max_level may be too low), but for at least some "real" problems this is within the bounds of Knuth's algorithm M.
...
- 1,235
2
votes
Theoretical explanations for practical success of SAT solvers?
Since the original question title asks for theoretical explanations, let me point to a paper that might provide a kind of non-standard theoretical explanation.
The main result of the paper is that one ...
- 11.3k
1
vote
Accepted
Is it possible to prove that a general purpose integer factorization algorithm must contain a loop?
It depends on the precise model of computation you work within. However, this doesn't seem to be a useful direction for proving lower bounds on the time to factor.
Uniform algorithms
Let's look at ...
- 11.7k
1
vote
List of NP-hard problems, where there is active research in practical heuristics
Operations research have a plenty of combinatorial optimization problems where the development of heuristics for minimization (or maximization) of resulting costs are an very active area.
For example,...
1
vote
Finding smallest context free grammar that generates a set of sets
Because the order of your symbols does not matter, you can always move the nonterminals to the very right of the productions. If there is no more than one in any rule, the resulting grammar is regular....
- 462
1
vote
Packing $n$ objects into $m$ bins whose size is variable
This seems similar to bin-packing problem.
I set $a=1$ and try to solve the bin-packing problem of putting objects of size $O_1$ to $O_n$. If I cannot find the solution then I increase $a$ with value $...
- 199
1
vote
Accepted
Approximations for the Stable Fixtures Problem
Your problem is called maximum weighted simple b-matching, and it's solvable in strongly polynomial time. See this paper for instance.
- 1,551
1
vote
A search problem and no algorithm for it
As observed in Aaron Roth's answer, what you're describing does indeed appear to be PLS.
In such cases, there are many, many alternative approaches under the heading of `metaheuristics'. A great ...
- 773
Only top scored, non community-wiki answers of a minimum length are eligible