Quickly Prove Me Wrong!

Question

Introduction

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!

Specification

Input

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.

Example input:

[A -> B; B -> A]
[A,B,C -> D; B,C -> E; -> A; B -> ]

Output

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.

Who wins?

This is code-golf, thus the shortest solution in bytes wins! Standard rules apply.

Examples

with Explanation

[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.

without Explanation

[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

Answer 1

Alice, 45 bytes

/;;?dhE..';F>@.>F*.?oK
\'..zi;w!";-$"'!?n-$-/

Try it online!

Input is in the form A->B;B->A with no spaces. Output is Jabberwocky if the formula is satisfiable, and nothing otherwise.

Explanation

This follows a standard template for programs that run entirely in ordinal mode. Unwrapped, the program is:

';.diEw.";->".!Fn.$o;.?zh;.!';F$@'>?*-?-K

';.     Push a semicolon and duplicate it
d       Join these two semicolons into a single string and push it, without removing the originals
        This puts ";;" on top of the stack, with a ";" under it (and an irrelevant ";" under that)
i       Take input
E       Insert input between the only pair of characters in ";;"
w       Push return address (start main loop)
.       Duplicate current set of implications
";->"   Push this string
.!      Copy to tape (to get it again later with fewer bytes)
F       Check whether this string is in current set of implications
n       Negate result: "Jabberwocky" if no match, "" if match
.$o     Output this string if nonempty (no unit clauses remain)
;       Discard top of stack: if the previous command didn't output, this puts the implications back on the TOS
        If the previous command did output, this discards the implications and puts ";" on the TOS
.       Duplicate
?z      Remove everything up to and including the first ";->"
h;      Take first character of remaining string: this is the literal in the first unit clause,
        or ";" if the clause is simply "->" (or if "Jabberwocky" was output earlier)
.!      Copy to tape, since we will need it later
';F     Check whether this character contains (i.e., is) a semicolon
$@      If so, terminate
        (Replace "A" in the next two lines with the actual value of the literal in this unit clause)
'>?*-   Remove all instances of ">A"; this destroys all clauses that imply A
?-      Remove all instances of "A"
K       Return to start of main loop

Each command in the main loop takes polynomial time, and each iteration of the loop either terminates the program or destroys at least one clause. Hence, the entire program runs in polynomial time.

Answer 2

Python 2, 312 244, 243 bytes

from sympy import*;s=input()
l=' ||,|&|;->|;1>>|[->|[1>>|->;|>>0;|->]|>>0]|;|)&(|->|>>|[|(|]|)|(|((|>>|)>>'.split('|')
for i in zip(l[::2],l[1::2]):s=s.replace(*i)
for i in range(65,91):y=chr(i);vars()[y]=Symbol(y)
print satisfiable(eval(s))>0

Try it online!

Some explications The input is converted to the appropriate format of sympy module, then verifying satisfiability.

Is it time-polynomial?

I performed a set of experimental tests that shows that the algorithm is linear. Randomly, I took N implications, with N in [1..1000], over a number of variables between 1 and 26. After that I do one thousand of satisfiability test for each N. Finally I plot the average in millisecond.

Answer 3

APL, 49 bytes

{×∧/∨/¨≢¨¨{(2⊃¨⍵/⍨0=≢¨⊃¨⍵)∘{x y←⍵⋄(x~⍺)y}¨⍵}⍣≡⊢⍵} 

This function takes an array of implications, where each implication is a 2-element array, with the first element containing the variables before the arrow and the second containing the variable after the arrow if there is one.

E.g. [A,B,C -> D; B,C -> E; -> A; B -> ] is represented as:

('ABC' 'D')('BC' 'E')('' 'A')('B' '')

The elements need not be letters but could be anything as long as they can be compared.

Explanation:

• {...}⍣≡⊢⍵: run the following function on the input until a fixpoint is found

  • (...)∘: Find the current units:

    • ⊃¨⍵: For each implication in the input, take the first element
    • 0=≢¨: See which are empty
    • ⍵/⍨: Select those implications
    • 2⊃¨: Select the second element from each

  • {...}¨⍵: For each implication, given the units:

    • x y←⍵: unpack the implication into its first and second component
    • (x~⍺)y: remove the previous units from the first component and leave the second one alone
• ≢¨¨: find the length of each inner element. If the clause is unsatisfiable, there is at least one (0,0) element (i.e. [] -> [], True → False).
• ∨/¨: for each implication, find the GCD of the lengths of its parts. If unsatisfiable, this will be 0.
• ∧/: find the LCM of all the GCDs. If unsatisfiable, this will be 0.
• ×: return the sign, so a boolean value is returned (0 for unsatisfiable, 1 for satisfiable).

Polynomiality proof:

The main loop ({...}⍣≡) will run until there are no more reducible implications. Each step, all current known facts are removed from the left hand side of each implication. Because each implication can only have 0 or 1 variables on its right hand side, the size of the set of knowable facts is bounded by the amount of implications, meaning the loop will run at most n times.

The main loop further contains a number of maps over the list of implications, meaning the total running time is O(n^2).

Link to tests cases being run on tio.run.