Докажи, что я неправ!

22

Введение

Ваша жизненная миссия проста: докажите, что люди не правы в Интернете!
Для этого вы обычно тщательно анализируете их высказывания и указываете на противоречие в них.
Пришло время автоматизировать это, но, поскольку мы ленивы, мы хотим доказать, что люди ошибаются с минимальными усилиями (читай: самый короткий код).

Спецификация

вход

Ваш вклад будет формулой в соединительной нормальной форме . Для этого формата вы можете использовать приведенный ниже формат или определить свой собственный, исходя из потребностей своего языка (хотя вы не можете кодировать больше в формате, чем чистый CNF). Тем не менее, тестовые случаи (здесь) представлены в следующем формате (хотя это не будет слишком сложно для создания собственного).

Ваш ввод будет представлять собой список из списка переменных (вы также можете читать его как строки / требовать строки). Входные данные представляют собой формулу в конъюнктивной нормальной форме (CNF), записанную в виде набора предложений, каждое из которых представляет собой список из двух списков. Первый список в предложении кодирует положительные литералы (переменные), второй список кодирует отрицательные (отрицательные) литералы (переменные). Каждая переменная в предложении объединяется в OR, а все предложения объединяются в AND.

Чтобы было понятнее: [[[A,B],[C]],[[C,A],[B]],[[B],[A]]]можно читать как:
(A OR B OR (NOT C)) AND (C OR A OR (NOT B)) AND (B OR (NOT A))

Выход

Вывод логический, например, какое-то истинное значение или некоторое ложное значение.

Что делать?

Все просто: проверьте, удовлетворяет ли приведенная формула, например, существует ли какое-либо присвоение true и false всем переменным, так что общая формула выдает «true». Ваш вывод будет "true", если формула satiesfiable, и "false", если это не так.
Интересный факт: это NP-полная задача в общем случае.
Примечание: создание таблицы истинности и проверка, является ли какая-либо результирующая запись истинной, разрешено.

Угловые чехлы

Если вы получите пустой список 3-го уровня, то в этом предложении нет такой (положительной / отрицательной) переменной - допустимого ввода.
Вы можете оставить другие угловые случаи неопределенными, если хотите.
Вы также можете вернуть true для пустой формулы (список 1-го уровня) и false для пустого предложения (список 2-го уровня).

Кто выигрывает?

Это код-гольф, поэтому выигрывает самый короткий ответ в байтах!
Стандартные правила применяются конечно.

Тест-кейсы

[[[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
источник
1
Можем ли мы принять вклад как (A OR B OR (NOT C)) AND (C OR A OR (NOT B)) AND (B OR (NOT A))?
Адам
1
@ Adám, как указано в задании, формат полностью зависит от вас, если он не кодирует больше информации, чем основанный на списке. (Например, формулировка, которую вы дали, полностью разрешена)
SEJPM
@SEJPM Если я правильно понимаю нотацию, я думаю, 3-й и 4-й тесты должны вернуть true. Я попытался заменить (P, Q) = (1,1) и (P, Q, R, S, T) = (0,0,0,0,0) и нашел оба значения true, поэтому должен быть хотя бы один случай, когда выражение верно.
busukxuan
@busukxuan, я на 100% уверен, что третий и четвертый являются ложными. Для 3): это {{P,Q},{P,!Q},{!P,Q},{!P,!Q}}(не в этом порядке), что легко показать, противоречие. Для 4): Это тривиально противоречие, потому что оно, P AND ... AND (NOT P)очевидно, никогда не может быть истинным ни для какого значения P.
SEJPM
2
Забавно, что более короткий код на самом деле требует больше усилий для написания.
user6245072

Ответы:

41

Mathematica, 12 байт

SatisfiableQ

Ну, есть встроенный ...

Формат ввода есть And[Or[a, b, Not[c], Not[d]], Or[...], ...]. Это делает работу правильно для пустого подвыражения, потому что Or[]это Falseи And[]есть True.

Для записи, решение, которое получает основанный на списке формат от запроса и выполняет само преобразование, составляет 44 байта, но ОП пояснил в комментарии, что любой формат хорош, если он не кодирует дополнительную информацию:

SatisfiableQ[Or@@Join[#,Not/@#2]&@@@And@@#]&
Мартин Эндер
источник
18
Потому что Mathematica ...
Дрянная Монахиня
11
У Mathematica действительно есть безумное количество встроенных ._.
TuxCrafting
3
@ TùxCräftîñg Действительно .
jpmc26
15
В течение доли секунды я думал, что этот ответ был написан в неясном, основанном на стопах esolang, где, по чистой случайности, последовательность команд S a t i s f i a b l e Qмогла решить проблему. Только тогда в дверь постучали по чтению ...
ojdo
3

Haskell, 203 200 байт

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)

Этот вызов заслуживает ответа без встроенных функций, так что вот и все. Попробуйте это на Ideone . Алгоритм просто пытается присвоить все переменные и проверяет, удовлетворяет ли одно из них формуле.

Ввод осуществляется в форме [([],["P","Q"]),(["Q","P"],[]),(["P"],["Q"]),(["Q"],["P"])], хотя вместо строк будет работать каждый тип с равенством.

Ungolfed код:

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
источник
1

JavaScript 6, 69B

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

Использование:

f('a|b')(['a','b'])
true
l4m2
источник