求解任一考卷上(decidable)是非題在polynomial time可reduce成SAT問題？

最近在想一個問題，

令問題X為，求取求解任一考卷上decidable的是非題的程序，

X 是否在polynomial time能reduce to SAT(satifiability) problem？

我假設，考卷上的是非題目其中一題，是有限個字的，為n個字。

且所用的字，可以在一本符號大全的書上找到，

而這本書有X'個符號，(包含空字元符號)，這我們把題目上的每一個字用logX'取上高斯的bit數來表示，

令bit數為K。則我們可以設計一SAT Algorithm把題目每一個字都輸入下去，看是否satisfy。

總共是輸入nk個bit看是否satisfy，若是satisfy 則 輸出為圈，否則輸出為叉.

所以求解任一考卷上的(decidable)是非題的問題應該是能在polynomial time reduce to SAT problem的!

再想想，若不是是非題的情況，

則假設答案是有限個字所能表示的情況，令最多可用i個字表示，

因為所選的符號書包含空字元符號，所以答案實際上為j個字<=i,

而答案是什麼，可想成答案中每一個字元的第y個bit是否為1 ，(y有i*k個)，

若satisfy則為1。所以要run SAT i*k次。

PS. any NP problem reduce to SAT is trivial, but SAT reduce to NP problem X, X is called NP-Complete.

後記：所以這結論是trivial的…