Flawed problem generation!
Propositional satisfiability
- may generate unit clauses, x and -x
- just as 2 people here are likely to have same birthday
Quantified satisfiability
- may generate clause with single existential, x and another with -x
- no satisfying assignment
- simple argument gives l µÖn
Model A, discard clauses with one or fewer existentials
Model B, fix number of existentials in each clause