Restricted boolean formulas for avoiding NP-completeness

Question

I have boolean formulas A and B and want to check if "A -> B" (A implies B) is true in polynomial time.

For fully general formulas A and B, this is NP-complete because ""A -> B" is true" is the same as "not (A -> B)" is not satisfiable.

My goal is to find useful restrictions such that polynomial time verification is possible. I would also be interested in finding O(n) or O(n log n) restrictions (n is some kind of length |A| or |B|). I would prefer to restrict B rather than A.

In general, I know of the following classes of "easier" boolean formulas:

• (renamable) Horn formulas can be solved in linear time (they are in CNF form with at most one positive variable).
• All formulas in DNF form are trivial to check
• 2-SAT are CNF formulas with at most 2 variables per clause, solvable in linear time.
• XOR-SAT are CNF formulas with XOR instead of OR. They can be solved via Gaussian elimination in O(n^3)

The main problem is that I have the formula "A -> B" aka "(not A) or B", which quickly becomes non-CNF and non-DNF for non-trivial A/B.

If I understand the Tseytin transformation correctly, then I can transform any formula X into CNF Y with O(|X|) = O(|Y|), thus I can assume - if I want - that I have my formula in CNF.

There is some low-hanging fruit:

• if |B| is constant and small, I could enumerate all solutions to B and check if they are produce a true A.
• similarly, if |A| is constant and small, I could enumerate all solutions to A and check if they produce a false B

More interestingly:

• if B is in DNF then I can convert A to CNF, which will make "(not A) or B" DNF which is solvable in linear time.
• For general B, if |B| is in O(log |A|), I could convert B to DNF and solve it that way

However, I'm not sure how I can use the other easier classes or if it is possible at all.

Due to distributivity, an A or B in CNF will almost certainly blow up exponentially when trying to bring "(not A) or B" back to CNF - if I'm not mistaken.

Note: my use case probably has more complex/longer A than B formulas.

So my questions boils down to: Are there useful classes of boolean formulas A and B such that "A -> B" can be proven in polynomial (preferably linear) time? - apart from the 4 cases that I already mentioned.

EDIT: A different take on this: Under what conditions of A and B is "A -> B" in one of the following classes:

• in DNF
• in CNF and a Horn formula (Horn-SAT)
• in CNF and a binary formula (2-SAT)
• in CNF and a arithmetic formula (CNF of XOR)

Answer 1

"For fully general formulas A and B, this is NP-complete because ""A -> B" is true" is the same as "not (A -> B)" is not satisfiable."

Not satisfiable means unsatisfiable. Thus the problem you adressed is co-NP-complete.