Computing finite models using free Boolean generators