This is the evolution of this previous challenge which was about checking satisfieability of normal formulae in conjunctive normal form (CNF). However, this problem is NP-complete and watching algorithms finish is just boring, so we're gonna simplify the problem!
You may tune the following input specification to optimally match your language as long as you don't encode additional information.
Your input will be a list of implications. Each implication has a list of variables on the left and a single variable on the right. Variables may be represented using your favorite representation (integer, strings, whatever), for the sake of this specification, characters will be used. The list on the left side may be empty and there may not be a variable on the right. The variable on the right side will not appear on the left side of the same implication.
[A -> B; B -> A] [A,B,C -> D; B,C -> E; -> A; B -> ]
Your output will be a truthy or a falsy value.
What to do?
You need to determine whether the given formula is satisfieable and output truthy if it is satisfieable and falsy if not.
A,B -> C means that if A and B need to hold then C needs to hold as well.
-> C means that C always needs to hold (this is short-hand for
True -> C).
A,B -> means that if A and B need to hold, so does falsum and thus there is a contradiction, thus if you find such an implication where A and B hold, you can immediately output falsy (this is short-hand for
A,B -> False).
The list of implications all need to hold at the same time.
Because this problem is also known as HORNSAT, it is P-complete and to avoid trivial solutions to this, your solution must run in polynomial time and you must provide reasoning why your solution does so.
This is code-golf, thus the shortest solution in bytes wins! Standard rules apply.
[A,B -> C; C ->; -> A; A -> B] A needs to hold, thus B needs to hold, thus C needs to hold and thus you found a contradiction.
[A,B -> D; C ->; -> A; A -> B] A needs to hold, thus B needs to hold, thus D needs to hold, however C doesn't need to hold and thus this formula is satisfieable.
[A -> B; B -> A] => 1 [A,B,C -> D; B,C -> E; -> A; B -> ] => 1 [A,B -> C; C ->; -> A; A -> B] => 0 [A,B -> D; C ->; -> A; A -> B] => 1 [P -> ; -> S ; P -> R; Q -> U; R -> X; S -> Q; P,U -> ; Q,U -> W] => 1 [-> P; Q -> ; T -> R; P -> S; S -> T; T,P -> Q ] => 0