I'm trying to generate some test problems for propositional satisfiability, in particular to generate some that are unsatisfiable, but according to a fixed pattern, so that for any N, an unsatisfiable problem of N variables can be generated.
An easy solution would be x1, x1=>x2, x2=>x3 ... !xN except this would be all unit clauses, which any SAT solver can handle instantly, so that's not a tough enough test.
What would be a pattern for unsatisfiable problems of N variables, that are not random and can be seen by inspection to be unsatisfiable, but are at least somewhat nontrivial for an SAT solver?
Pigeonhole problems are non-trivial for CDCL-based SAT solvers without preprocessing, i.e. see Detecting Cardinality Constraints in CNF. The paper Hard Examples for Resolution may be of interest for you.