by zero_k on 2/10/25, 10:32 AM with 12 comments
by oinweo on 2/14/25, 7:12 AM
The highlighted lines are what’s call the Tseitin transformation, which basically means that when H1 is FALSE, (NOT X or NOT y) must be TRUE"
Forgive me if I'm wrong, but I think it should be "when H1 is TRUE, (NOT X or NOT y) must be TRUE" since this is equivalent to "H1 -> NOT (X & Y)"
by zero_k on 2/10/25, 10:32 AM