Monotone $(3^+, 2^-)$ SAT can be defined as follows:
Given a monotone CNF formula $(+F^3, -F^2)$, each positive monotone clause of length 3 and each negative monotone clause of length 2.
Each variable appears exactly once (as a positive literal in clauses in $+F^3$), (on the same variables as in $+F^3$) and one or more times in $-F^2$, (where all variables are negated).
Is $(+F^3, -F^2)$ satisfiable?
The above problem is NP-Complete (ref: https://cs.stackexchange.com/questions/16634/complexity-of-monotone-2-sat-problem)
Can someone provide with a small non trivial instance of this problem that are unsatisfiable?
Does this work?
$(X \vee Y \vee Z) \land (A \vee B \vee C) \land $
$(\neg A \vee \neg X) \land (\neg A \vee \neg Y) \land (\neg A \vee \neg Z) \land$
$(\neg B \vee \neg X) \land (\neg B \vee \neg Y) \land (\neg B \vee \neg Z) \land$
$(\neg C \vee \neg X) \land (\neg C \vee \neg Y) \land (\neg C \vee \neg Z)$
It's supposed to say that at least one of $X, Y, Z$ is true, and that at least one of $A, B, C$ is true, but also that any pair of variables chosen from each triple cannot both be true.