Boolean Satisfiability with Transitivity Constraints

摘要

We consider a variant of the Boolean satisfiability problem where a subset E of the propositional variables appearing in formula Fsat encode a symmetric, transitive, binary relation over N elements. Each of these relational variables, Ei,j for 1