CODEWITHSUNDEEP
language-agnosticboolean-logicsatpropositional-calculus
rwallace
rwallace

Reputation: 33405

Generating unsatisfiable test problems

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?

Upvotes: 2

Views: 289

Answers (2)

tphilipp
tphilipp

Reputation: 466

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.

Upvotes: 3

Davislor
Davislor

Reputation: 15144

First example that comes to mind is to take the conjunction of all possible disjunctions containing every variable once. For example, if your variables are p1, p2, and p3:

(¬p1 ∨ ¬p2 ∨ ¬p3) ∧ (¬p1 ∨ ¬p2 ∨ p3) ∧ (¬p1 ∨ p2 ∨ ¬p3) ∧ (¬p1 ∨ p2 ∨ p3) ∧ (p1 ∨ ¬p2 ∨ ¬p3) ∧ (p1 ∨ ¬p2 ∨ p3) ∧ (p1 ∨ p2 ∨ ¬p3) ∧ (p1 ∨ p2 ∨ p3)

Another way to describe this is: the conjunction of negations of every possible assignment. For example, ¬(p1 ∧ p2 ∧ p3) = (¬p1 ∨ ¬p2 ∨ ¬p3) is a clause of the formula. So, every possible assignment fails to satisfy exactly one clause. We only know this, however, because we verified that the clauses are exhaustive.

If we try to convert to canonical disjunctive normal form, we can’t do it any faster regardless of what order we try the variables in, and we eventually get:

(p1 ∧ ¬p1 ∧ p2 ∧ p3) ∨ (p1 ∧ p2 ∧ ¬p2 ∧ p3) ∨ (p1 ∧ p2 ∧ p3 ∧ ¬p3)

Where every clause we generate turns out to be unsatisfiable, but we only see this when we expand out all of them. If we try to search for a satisfying assignment, regardless of what order we try the variables in, we can only test every possible assignment exhaustively in exponential time.

There might be a SAT-solver out there that tests for this special case, although testing that every possible clause is in the input would itself take exponential time, and putting arbitrary input into a canonical form where you could efficiently say, there are only eight possible clauses of three variables and we’ve already checked that there are no duplicates, would take a while too.

Upvotes: 1

Related Questions