THE INVERSE SATISFIABILITY PROBLEM

We study the complexity of telling whether a set of bit-vectors repres ents the set of all satisfying truth assignments of a Boolean expressi on of a certain type. We show that the problem is coNP-complete when t he expression is required to be in conjunctive normal form with three literals per clause (3CNF). We also prove a dichotomy theorem analogou s to the classical one by Schaefer, stating that, unless P=NP, the pro blem can be solved in polynomial time if and only if the clauses allow ed are all Horn, or all anti-Horn, or all 2CNF, or all equivalent to e quations modulo two.