The Glucose SAT Solver

단일 코어 솔버 (glucose)

단일 스레드에서 SAT 문제를 해결하는 버전입니다. 핵심 옵션, 클라우스 최소화, 축소, 재시작, 단순화 옵션 등 다양한 파라미터를 통해 해결 과정을 세밀하게 조정할 수 있습니다.

• 입력 파일은 일반 텍스트 또는 gzip으로 압축된 DIMACS 형식을 지원합니다.
• 실증 가능한 불만족(UNSAT) 옵션을 지원합니다.

다중 코어 솔버 (glucose-syrup)

여러 CPU 코어를 활용하여 SAT 문제를 병렬로 해결하는 버전입니다. 단일 코어 솔버의 모든 옵션에 더해 병렬 처리 관련 옵션이 제공됩니다.

• -nthreads: 사용할 스레드 수를 지정합니다 (기본값: 0).
• -maxnbthreads: 최대 스레드 수를 지정합니다 (기본값: 4).

다운로드·설치 방법

두 가지 방법으로 설치할 수 있습니다.

1. Chocolatey 설치: 관리자 권한으로 명령 프롬프트를 열고 다음 명령을 실행합니다.
   choco install glucose
2. 수동 설치: GitHub의 최신 릴리스 페이지에서 ZIP 파일을 다운로드한 후 원하는 폴더에 압축을 풉니다.

기본 사용법

설치 후 명령 프롬프트 또는 PowerShell에서 다음과 같이 실행합니다.

단일 코어 솔버 사용법:

• glucose --help: 사용 가능한 모든 옵션과 도움말을 표시합니다.
• glucose [options] <input-file> <result-output-file>: 지정된 DIMACS 입력 파일을 분석하여 결과를 출력 파일에 저장합니다.

다중 코어 솔버 사용법:

• glucose-syrup --help: 병렬 버전의 도움말을 표시합니다.
• glucose-syrup [options] <input-file> <result-output-file>: 여러 코어를 활용하여 문제를 해결합니다.

이런 경우에 유용합니다

컴퓨터 과학, 수학, 또는 관련 연구 분야에서 불리안 만족 가능성 문제를 해결해야 하는 연구자 및 개발자에게 유용합니다. 병렬 처리를 통해 대규모 또는 복잡한 SAT 문제의 해결 시간을 단축하는 데 적합합니다.

지원 환경·시스템 요구사항

이 빌드는 Windows 운영 체제를 지원합니다.

최신 버전·업데이트

현재 제공되는 최신 버전은 4.1입니다. 업데이트 및 릴리스 정보는 GitHub 릴리스 페이지를 통해 확인할 수 있습니다.

제한 사항·확인 사항

이 소프트웨어는 개발자, 연구자 등을 대상으로 하는 명령줄 도구입니다. 일반 사용자를 위한 그래픽 사용자 인터페이스(GUI)가 포함되어 있지 않습니다.