Buktikan bahwa aku salah!

22

pengantar

Misi Anda dalam hidup itu sederhana: Buktikan orang salah di internet!
Untuk melakukan ini, Anda biasanya hati-hati menganalisis pernyataan mereka dan menunjukkan kontradiksi di dalamnya.
Sudah waktunya untuk mengotomatisasi ini, tetapi karena kita malas, kami ingin membuktikan orang salah dengan upaya yang paling sedikit (baca: kode terpendek) yang mungkin.

Spesifikasi

Memasukkan

Masukan Anda akan menjadi rumus dalam bentuk normal konjungtif . Untuk format, Anda dapat menggunakan format di bawah ini atau menentukan sendiri, berdasarkan kebutuhan bahasa Anda (Anda tidak dapat menyandikan lebih banyak dalam format daripada CNF murni sekalipun). Kasing uji (di sini) disediakan dalam format di bawah ini (meskipun tidak akan terlalu sulit membuat sendiri).

Input Anda akan berupa daftar daftar variabel (Anda juga dapat membacanya sebagai string / memerlukan string). Input adalah rumus dalam bentuk normal konjungtif (CNF) yang ditulis sebagai satu set klausa, masing-masing menjadi daftar dua daftar. Daftar pertama dalam klausa mengkodekan literal positif (variabel), daftar kedua mengkodekan literal negatif (dinegasikan) (variabel). Setiap variabel dalam klausa adalah OR'ed bersama dan semua klausa adalah AND'ed bersama.

Untuk membuatnya lebih jelas: [[[A,B],[C]],[[C,A],[B]],[[B],[A]]]dapat dibaca sebagai:
(A OR B OR (NOT C)) AND (C OR A OR (NOT B)) AND (B OR (NOT A))

Keluaran

Outputnya adalah boolean, misalnya nilai kebenaran atau nilai palsu.

Melakukan apa?

Sederhana: Periksa apakah rumus yang diberikan sudah memuaskan, misalnya apakah ada beberapa penugasan benar dan salah untuk semua variabel sehingga keseluruhan rumus menghasilkan "benar". Output Anda akan "benar" jika rumusnya memuaskan dan "salah" jika tidak.
Fun-Fact: Ini adalah masalah NP-complete dalam kasus umum.
Catatan: Membuat tabel kebenaran dan memeriksa apakah entri yang dihasilkan benar, diizinkan.

Kasus sudut

Jika Anda mendapatkan daftar level 3 kosong, maka tidak ada variabel (positif / negatif) dalam klausa itu - input yang valid.
Anda dapat membiarkan case sudut lainnya tidak terdefinisi jika Anda mau.
Anda juga dapat mengembalikan true pada formula kosong (daftar level 1) dan false pada klausa kosong (daftar level 2).

Yang menang?

Ini adalah kode-golf sehingga jawaban tersingkat dalam byte menang!
Aturan standar berlaku tentu saja.

Kasus uji

[[[P],[Q,R]],[[Q,R],[P]],[[Q],[P,R]]] -> true
[[[],[P]],[[S],[]],[[R],[P]],[[U],[Q]],[[X],[R]],[[Q],[S]],[[],[P,U]],[[W],[Q,U]]] -> true
[[[],[P,Q]],[[Q,P],[]],[[P],[Q]],[[Q],[P]]] -> false
[[[P],[]],[[],[P,S]],[[P,T],[]],[[Q],[R]],[[],[R,S]],[[],[P,Q,R]],[[],[P]]] -> false
optional behavior (not mandatory, may be left undefined):
[] -> true (empty formula)
[[]] -> false (empty clause)
[[[],[]]] -> false (empty clause)
SEJPM
sumber
1
Bolehkah kita mengambil input sebagai (A OR B OR (NOT C)) AND (C OR A OR (NOT B)) AND (B OR (NOT A))?
Adám
1
@ Adám, sebagaimana ditentukan dalam tantangan, format sepenuhnya terserah Anda, asalkan tidak menyandikan lebih banyak informasi daripada yang berbasis daftar. (Misalnya, formulasi yang Anda berikan sepenuhnya diizinkan)
SEJPM
@ SEJPM Jika saya memahami notasi dengan benar, saya pikir test case ke-3 dan ke-4 harus benar Saya mencoba mengganti (P, Q) = (1,1) dan (P, Q, R, S, T) = (0,0,0,0,0) dan menemukan keduanya benar, sehingga setidaknya harus ada satu kasus di mana ungkapan itu benar.
busukxuan
@busukxuan, saya 100% yakin yang ketiga dan keempat salah. Untuk 3): ini {{P,Q},{P,!Q},{!P,Q},{!P,!Q}}(tidak dalam urutan ini) yang dapat dengan mudah ditampilkan adalah sebuah kontradiksi. Untuk 4): Ini adalah kontradiksi sepele karena itu P AND ... AND (NOT P)jelas tidak pernah benar untuk nilai P.
SEJPM
2
Lucu betapa pendeknya kode sebenarnya membutuhkan lebih banyak upaya untuk ditulis.
user6245072

Jawaban:

41

Mathematica, 12 byte

SatisfiableQ

Nah, ada built-in ...

Format input adalah And[Or[a, b, Not[c], Not[d]], Or[...], ...]. Ini tidak bekerja dengan benar untuk sub-ekspresi kosong, karena Or[]ini Falsedan And[]adalah True.

Sebagai catatan, solusi yang menerima format berbasis daftar dari tantangan dan melakukan konversi itu sendiri adalah 44 byte, tetapi OP mengklarifikasi dalam komentar bahwa format apa pun baik-baik saja asalkan tidak menyandikan informasi tambahan:

SatisfiableQ[Or@@Join[#,Not/@#2]&@@@And@@#]&
Martin Ender
sumber
18
Karena Mathematica ...
Leaky Nun
11
Mathematica benar-benar memiliki sejumlah builtin ._.
TuxCrafting
3
@ TùxCräftîñg Memang .
jpmc26
15
Untuk sepersekian detik, saya pikir jawaban ini ditulis dalam esolang yang tidak jelas dan bertumpuk di mana, secara kebetulan, urutan perintah S a t i s f i a b l e Qakan menyelesaikan masalah. Baru kemudian, pemahaman membaca mengetuk pintu ...
ojdo
3

Haskell, 203 200 byte

t=1<3
e%((t,f):r)=or((e<$>t)++map(not.e)f)&&e%r
e%_=t
u v b e s|s==v=b|t=e s
s e[]c=1<0
s e(v:w)c=e%c||s(u v t e)w c||s(u v(1<0)e)w c
g v[]=v
g v((t,f):r)=g(v++[x|x<-t++f,notElem x v])r
g[]>>=s(\x->t)

Tantangan ini layak mendapat jawaban tidak-built-in, jadi begini saja. Cobalah di ideone . Algoritma hanya mencoba semua tugas variabel dan memeriksa apakah salah satu dari mereka memenuhi formula.

Input dalam bentuk [([],["P","Q"]),(["Q","P"],[]),(["P"],["Q"]),(["Q"],["P"])], meskipun alih-alih string, setiap tipe dengan kesetaraan akan berfungsi.

Kode tidak dikunci:

type Variable   = String
type CNF        = [([Variable], [Variable])]
type Evaluation = (Variable -> Bool)

satisfies :: Evaluation -> CNF -> Bool
satisfies eval [] = True
satisfies eval ((t,f):r) = or(map eval t ++ map (not.eval) f) && satisfies eval r

update :: Evaluation -> Variable -> Bool -> Evaluation
update eval s b var = if var == s then b else eval var

search :: Evaluation -> [Variable] -> CNF -> Bool
search eval [] cnf = False
search eval (v:vars) cnf = satisfies eval cnf || search (update eval v True) vars cnf || search (update eval v False) vars cnf 

getVars :: CNF -> [Variable] -> [Variable]
getVars [] vars = vars
getVars ((t,f):cnf) vars = getVars cnf (vars ++ [v |v<-(t++f), notElem v vars])

isSat :: CNF -> Bool
isSat cnf = search (\x->True) (getVars cnf []) cnf
Laikoni
sumber
1

JavaScript 6, 69B

x=>f=(v,e)=>(e=v.pop())?[0,1].some(t=>f([...v],eval(e+'=t'))):eval(x)

Pemakaian:

f('a|b')(['a','b'])
true
l4m2
sumber