Hacker News new | ask | show | jobs
by secant 4034 days ago
I'm a bit of a math novice, but is the term "decidable" analogous with satisfiability (SAT), or is this a completely different set of modelling?
1 comments

Nope, decidable is a much higher level. A problem is decidable if it can ever be solved by any computer, given as much time as it wants.

The classic undecidable problem is "the halting problem". In short, given a computer program (and some input for it), decide if that program will ever stop, or continue forever. It turns out there is NO WAY to write a program which will, for any input program, check if it will halt in finite time.

This stuff is a little mind-blowing at first -- the wikipedia article isn't bad.

EDIT: Fixed typo from wolfgke

> The classic decidable problem is "the halting problem".

The classic undecidable problem ...

A simple summary is: a problem domain is decidable if there exists an algorithm that will always be able to tell you true or false if any problem in that domain is solvable.

Some examples of this are propositional logic and linear logic are decidable, whereas the halting problem and nonlinear logic are not.

For instance, the halting problem isn't decidable because although you can answer true or false for some specific programs, there exists programs where you do not know if they halt or not. Arbitrary mathematical problems in general are undecidable (see Gödel's incompleteness theorems) but we can still carve out domains within this that are decidable.

To be pedantic: the Halting Problem for Turing Machines is undecidable. There are simpler computing models for which we can decide halting.