비선형 관계를 표현하기
실수 연산과 다양한 비선형 함수를 포함하는 제약을 논리식으로 나타낸다. 이를 통해 단순 선형 관계보다 복잡한 계산 조건을 조사할 수 있다. 변수의 범위와 함수의 정의역을 문제에 맞게 정한다. 프로그램의 실제 정밀도나 자료 형식이 수학적 실수와 다른 경우 그 차이도 모델에서 검토해야 한다.
두 결과의 의미
unsat은 입력 논리식을 만족하는 값이 없다는 결과다. delta sat은 지정한 델타만큼 완화한 형태를 만족하는 해를 제공한다. 후자를 원래 등식이나 부등식의 정확한 해가 존재한다는 뜻으로 받아들이면 안 된다. 델타의 크기와 실제 요구 정확도를 연결해 결과를 해석한다.
설정과 연동 환경
명령행과 라이브러리 및 일부 기능의 Python 바인딩을 제공한다. Python 패키지 외에도 필요한 수치 라이브러리의 설치 조건을 확인해야 한다. 정밀도와 실행 제한 및 입력 형식을 함께 기록하고 도구가 반환한 구간을 원래 문제의 단위와 범위로 살펴본다. 시간 안에 계산을 끝내지 못한 상황은 두 판정 결과와 별도로 처리한다.