A symbolic solver that determines if a Boolean formula can be satisfied by finding true/false assignments.