Implementations of clausal contraints.