Skip to main content
OverflowAI is here! AI power for your Stack Overflow for Teams knowledge community. Learn more
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 ...
Kaveh's user avatar
  • 21.7k
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 ...
Jakob Nordstrom's user avatar
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 ...
Ryan O'Donnell's user avatar
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 ...
Magnus Wahlström's user avatar
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 ...
Jan Johannsen's user avatar
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 ...
David Eppstein's user avatar
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 ...
domotorp's user avatar
  • 14k
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 ...
Michael N. Rice's user avatar
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 ...
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. ...
D.W.'s user avatar
  • 12.1k
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 ...
D.W.'s user avatar
  • 12.1k
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 ...
Michael N. Rice's user avatar
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. ...
Peter Taylor's user avatar
  • 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 ...
Andras Farago's user avatar
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 ...
D.W.'s user avatar
  • 12.1k
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....
Peter Leupold's user avatar

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