New answers tagged sat
2
There exist first order (FO) logic systems that allow you to actually write FO constraints, and to reason with them in very intricate ways. E.g., see the IDP system.
For instance, I took a small variation of your example and coded it up in the online IDP editor:
vocabulary V{
type D
P(D)
}
theory T: V{
?x: P(x).
}
structure S:V{
D = {a;b}
}
...
-3
Solving a Sudoku puzzle is equivalent to deciding whether there is a valid graph vertex coloring using $k$ colors, where $k = 9$ in your $3 \times 3$ Sudoku instance. The graph coloring problem is known to be NP-complete for values of $k > 2$, so a non-trivial, non-backtracking algorithm for $3 \times 3$ Sudoku would be very surprising.
Top 50 recent answers are included
