sat-solvers

4열

1답변

링크 : 나는 SAT 해결사로 Z3를 사용했습니다 Z3 theorem prover picosat with pyhton bindings . 더 큰 수식의 경우 성능 문제가있는 것 같아서 피코사스가 더 빠른 대안인지 확인하려고했습니다. from z3 import * import pycosat from pycosat import solve, itersolv

2열

1답변

Z3py : 144 개의 변수가있는 큰 수식을 인쇄하십시오.

저는 Z3 정리 프로 버를 사용하며 큰 수식 (114 개 변수)이 있습니다. 모든 절과 함께 큰 수식을 인쇄 할 수 있습니까? 보통 print str(f)은 출력을 절단하고 모든 절이 아닌 "..."만 끝에 인쇄됩니다. 나는 print f.sexpr()을 테스트했으며 항상 모든 절을 인쇄합니다. 그러나 sexpr 구문에서만. 수식의 모든 절을 인쇄 할 수

0열

1답변

/usr/bin/ld : -lcplex를 찾을 수 없습니다.

이 git repo에서 MaxHS SAT 솔버를 설정하려고합니다. - https://github.com/fbacchus/MaxHS입니다. '/ usr/bin/ld : -lcplex를 찾을 수 없습니다.'라는 오류 메시지가 나타납니다. 누구나 lcplex 라이브러리 란 무엇이며 어떻게 해결할 수 있습니까? 내 콘솔은 다음과 같습니다 .. install -d

2열

1답변

MiniSat의 비 결정 변수의 의미는 무엇입니까?

C++ 라이브러리로 MiniSat을 사용할 때, 모든 새로운 변수는 결정 변수 또는 비 결정 변수로 생성 될 수 있습니다. 솔직히 분기 할 때 어떤 변수를 사용할 지 결정할 때 비 결정 변수는 고려되지 않습니다. 그러나 솔라가 SAT를 반환 할 때 공식이 실제로 UNSAT 임에도 불구하고 내 프로젝트에서 솔리드가 동등한 관계에있는 대신 결정되지 않은 변수가

2열

1답변

SMT에서 더 나은 관행은 무엇입니까? 다중 어설 션 또는 단일 및?

, (assert (> x y)) (assert (< y 2)) 처럼 별도의 주장으로 추가하거나이 (assert (and (> x y) (< y 2) )) 처럼 함께하고 작업자 한 주장을 추가하는 것이 좋습니다 내가 SMT에서 모델링 할 두 개의 절을 가지고 말할 수 있습니다 SMT 솔버 성능 측면에서 큰 문제가되는지 여부 나는 Z3을 사용하

1열

1답변

자식 프로세스는 영원히

나는 다음과 같은 라인을 따라 정의 된 제한 시간 내에 종료해야 자식 프로세스를 시작하고 살고있다. 내 주요 프로그램은 C#로 작성되었으며 Visual Studio 2013 및 Windows 7 64 비트을 사용하여 개발했습니다. 대부분의 경우 위 코드가 작동하고 적절한 프로세스 시간 초과 종료가 수행됩니다. 그러나 약 5 %의 경우에 process.Kil

7열

1답변

(get-unsat-core)은 Z3에서 빈을 반환합니다.

Z3을 사용하여 충족되지 않는 공식의 unsat-core를 추출합니다. 나는 Z3를 사용하고 @ 인터페이스를 상승 (웹 기반)를 다음과 같은 코드를 작성, 체크인 토가 제대로 'unsat'반환하지만 (GET-unsat 코어)을 빈 반환 (set-logic QF_LIA) (set-option :produce-unsat-cores true) (declar

0열

1답변

Java 용 IP Solver를 쉽게 사용할 수 있습니까?

자바 프로그램에서 0-1 정수 프로그래밍 솔버를 도구로 사용하고 싶습니다. 웹에서 사용하기 쉬운 것을 찾을 수 없습니다. 내가 sat4j에서 의사 부울 라이브러리를 시도했지만 이것은 잘 설명되어 있지 않으며 일부 클래스는 API의 설명과 일치하지 않습니다 (일부 메소드 서명이 다릅니다). 의견이 있으십니까?

1열

1답변

DPLL 일관된 리터럴 집합이란 무엇입니까?

SAT 솔버를 작성 중이며 DPLL 알고리즘을 구현하기 시작했습니다. 나는 알고리즘을 이해하고 그것이 어떻게 작동하는지, 나는 또한 그것의 변형을 구현했다. 그러나 나를 귀찮게하는 것은 다음 것이다. function DPLL(Φ) if Φ is a consistent set of literals then return true;

1열

2답변

다중 가정으로 해결

변수가 (a,b,c,d,e,f,g) 인 CNF 표현식이 있다고 가정합니다. SAT 해결사를 사용하여 (d,e,f)에 대한 할당을 찾으려면 어떻게해야합니까? {a,b,c,g} = {1,0,0,1}과 {a,b,c,g} = {1,1,1,1}이 주어 졌습니까? 하나의 가정이라면, {d,e,f}에 대한 과제를 찾기 위해 일일 해결사를 호출하는 것은 간단합니다 (예