solver

0열

1답변

Z3py를 처음 사용하면서 과제 (sat 및 unsat)에 대한 카운터 예제를 생성했습니다. unsat 솔루션에 대한 반례를 생성하는 함수가 있습니까?

0열

1답변

저는 17 개의 방정식, 총 변수의 최소 합을 계산할 수있는 506 개의 변수로 구성된 선형 시스템을 가지고 있습니다. 이것은 잘 작동하지만, 지금까지는 해결책이 19 가지 변수를 조합 한 결과입니다. 결국 결국 최적의 변수가 무엇인지 미리 알지 못하고 선택한 변수의 양을 10 개로 제한하고 싶습니다. (솔버가 나와 내포하는 비율과 비율). 값이 0보다 커

0열

2답변

PHP의 3 항의 방정식 솔버

a, b, c를 폼으로 주어진 간단한 다항식 (x^2 + b x + c)을 해결해야하는 실험실 프로젝트가 있습니다. 이 코드를 구현했지만 html 스크립트도 작동하지 않는 것 같습니다. 거의 하루 동안 실수를 찾으려고했기 때문에 당신의 도움이 필요합니다. 그러나 나는 잘못된 것을 발견 할 수 없습니다. <!DOCTYPE html> <html> <

-1열

1답변

Excel에서 구속 조건을 가진 객관적인 셀을 최적화하기 위해 루프에서 솔버를 실행하려면

저는 VBA, MACRO에 완전히 익숙합니다. 나는 그것이 제약 세포 (R10) 그런 다음이 목표와 제약 모두에 대해 다음 열로 이동해야와 목적 함수 세포 (N10)를 실행한다 먼저 을 최적화하기 위해 루프가 필요합니다. 즉 Cell O10 & 셀 S10에 대해서도 마찬가지로 2 회 더 반복합니다. 그런 다음 i + 9 번째 행으로 이동하고 동일한 단계 분

0열

1답변

Excel Solver 숫자 집합의 하위 집합에서 대상 합계 찾기

큰 집합의 하위 집합에서 대상 합계를 찾으려면 Solver를 사용하고 싶습니다. (16 개의 숫자 중 10 개의 숫자 하위 집합). 저는 Solver에 익숙하지 않아 제약 조건을 설정하는 가장 좋은 방법을 모릅니다. 내가 세트 내의 숫자의 5 종류를, A는 B가 C가 D는 E. 16의 세트는 이러한 종류의 상이한 조합을 포함 할 수 있지만, 대상의 서브 세

0열

3답변

카페에서 아담 솔버를위한 solver.prototxt

아담을 사용하는 solver.prototxt는 다음과 같습니다. 약관을 추가하거나 삭제해야합니까? 손실 나던, '스텝 사이즈는'고정 '되어'lr_policy '때문에 삭제 될 수 있습니다 caffe example on mnist과 비교하여 net: "/home/softwares/caffe-master/examples/hpm/hp.prototxt" test

0열

1답변

SAT 해 찾기 : SAT4J - 더 많은 예제가 있습니까?

SAT 해결사 전에 사용하지 않았기 때문에 SAT4J 사용법을 배우기 시작했습니다. 주로 API를 사용하고 있지만 때때로 클래스 또는 메서드의 몇 가지 인수 또는 형식/형식이 수용 할 수있는 것이 무엇인지 이해하기가 어렵습니다. 예 : public BinaryClause(IVecInt ps, ILits voc) SAT4j의 구현 된 기능을 이해하는 데

-2열

1답변

R 프로그래밍 - 제한된 변수를 사용하여 함수 (RMSE) 최소화

R에서 solver가 Excel에서하는 것처럼 함수 (rmse)를 최소화하고 싶습니다. 제한된 vaiables (i)를 사용하여 조절하기 **i >= 0 && i<=2** ac = c(85,95,79,88,90,99,111,99,100,110) ff = c(100,110,105,95,115,105,110,120,105,110) ff1 = ff[2:5

2열

1답변

Linear Programming Decision Variable> 0 then> = 3000

Excel에서 solver를 사용하여 뮤추얼 펀드 비용을 최소화하는 선형 프로그램을 만들려고합니다. 내 결정 변수는 각 펀드에 투자 한 금액입니다. 투자 된 것이 있다면 기금 최저액을 충족해야합니다. 어떻게 프로그램 할 수 있습니까? 금액 기금 1 투자> = 양 투자가> 0 기금 1 다음 양 펀드에 투자하는 경우 1> = 3000 다른 양 = 0 어떤 도움

1열

1답변

출력을 16 진수 형식으로 출력하는 방법

이 Boolector 프로그램 인쇄 출력을 2 진 형식으로 출력합니다. 하지만 16 진수 형식이 필요합니다. boolector에서 16 진수 형식을 인쇄하는 방법. (set-logic QF_BV) (set-info :smt-lib-version 2.0) (declare-const val1 (_ BitVec 16)) (declare-const val2