Ubuntu Online, Fedora Online, Windows 온라인 에뮬레이터 또는 MAC OS 온라인 에뮬레이터와 같은 여러 무료 온라인 워크스테이션 중 하나를 사용하여 OnWorks 무료 호스팅 제공업체에서 실행할 수 있는 depqbf 명령입니다.
프로그램:
이름
depqbf - 정량화된 부울 공식을 위한 솔버
개요
depqbf [옵션 ...] [NUM] [FILE]
기술
depqbf prenex의 QBF(정량화된 부울 공식)에 대한 검색 기반 솔버입니다.
결합 정규형. 충돌 중심의 QBF에 대한 DPLL 알고리즘을 기반으로 합니다.
조항과 솔루션 중심의 큐브 학습. DepQBF는 수식의 구조를 분석하여
독립변수를 식별하려고 시도합니다. 다른 이점 외에도 종종
의사결정의 자유도가 높아집니다. DepQBF 0.1의 JSAT 시스템 설명도 참조하세요.
참고 자료와 아이디어에 대한 간략한 개요는 QBFEVAL'10에서 확인하세요.
depqbf QDIMACS 형식의 QBF 수식을 읽습니다. 만약에 FILE 주어지지 않으면 다음에서 입력을 읽습니다.
표준입력. QBFEVAL'10에서 요구하는 입력/출력 표준을 준수합니다.
옵션
depqbf 다음 옵션을 허용합니다.
-시간, --도움
사용 정보를 인쇄합니다.
--번역
인쇄 버전.
--예쁜 인쇄
수식만 구문 분석하고 인쇄합니다.
-v 자세한 내용을 점진적으로 늘립니다.
NUM 선택사항: NUM초 후에 시간 초과됩니다.
FILE 선택 사항: FILE에서 입력을 읽습니다.
EXIT 지위
입력으로 주어진 QBF 공식이 만족되면 종료 상태는 10이고, 만족하면 20입니다.
불만족스럽다; 다른 종료 코드는 수식이 해결되지 않았음을 나타냅니다.
onworks.net 서비스를 사용하여 온라인으로 depqbf를 사용하세요.
