부울 시스템의 고정 점을 찾기위한 솔버
소개 : 문제
내 문제 는 연구 된 부울 시스템 의 고정 점을 찾는 방정식 시스템 을 푸는 것과 관련이 있습니다 ($F(X)=X$).
간단한 예
허락하다 $\bar{x}=\{x_1,x_2,x_3\} \in \{0,1\}$관심있는 부울 변수가 있습니다. 허락하다$F=\{f_1,f_2,f_3\}$일 업데이트 기능 이 변수를 (즉,$x_i(t+1) = f_i(x(t))$), 다음 조건 함수로 정의됩니다 (해당 그래프 개념화의 노드 인 각 변수의 입력을 기반으로 함).
$f_1 = \begin{cases} 1, -x_2 \ge 0 \\ 0, \text{otherwise} \end{cases}$, $f_2 = \begin{cases} 1, x_1-x_3 \ge 0 \\ 0, \text{otherwise} \end{cases}$, $f_3 = \begin{cases} 1, x_1+x_3 \ge 0 \\ 0, \text{otherwise} \end{cases}$
이러한 기능은이 질문에서 영감을 얻었습니다 .
목표는 답변 세트 를 찾는 것입니다. $\bar{x}$ (그 자체로 0, 하나 또는 여러 개일 수 있음) $F(\bar{x})=\bar{x}$.
위의 예는 물론 매우 간단한 경우입니다. 결국 저는 수백 개의 변수로 이러한 연립 방정식을 풀고 싶습니다. 조건 함수 는 항상 각 변수의 입력 값의 선형 조합이고 변수는 항상 boolean 입니다.
질문
이런 종류의 문제에 대한 효율적인 솔버 가 필요합니다 ( NP-hard btw로 알려져 있습니다 !). 예를 들어이 문제를 제약 프로그래밍으로 공식화하고 응답 세트 프로그래밍 (ASP) 기술을 사용하여 해결할 수 있습니까?
답변
따라서 ASP를 사용하여이 문제를 해결할 수 있습니다! 여기에 다음과 같은 파일에서 문제의 가능한 인코딩을 제공합니다 fp.lp.
% variables
var(1..3).
% functions
% f(Function,Coefficient,Variable)
f(1,-1,2).
f(2,1,1).
f(2,-1,3).
f(3,1,1).
f(3,1,3).
% guess assignment to variables
{ init(V) : var(V) }.
% compute functions
next(F) :- var(F), #sum { C,V : f(F,C,V), init(V) } >= 0.
% check if fixed point
:- init(V), not next(V).
:- next(V), not init(V).
#show next/1.
#show init/1.
명령 줄에서 clingo(version 5.4.0) 사용 : 이 특정 인스턴스에 대해 UNSATISFIABLE 을 clingo fp.lp얻 습니다 .
사실에 주석을 달고 우리가 얻은 솔버를 %f(2,1,1).다시 실행하십시오 clingo.
Answer: 1
next(3) init(1) init(3) next(1)
SATISFIABLE
init/1및 next/1술어 모두에서 리턴 된 변수는 활성 부울 변수 (1) 및 누락 된 변수 (0)로 변환됩니다. 따라서 반환 된 결과는 부울 벡터입니다.$\bar{x}=\{x_1=1,x_2=0,x_3=1\}$.
이 답변에 대한 크레딧은 Roland Kaminski로 이동합니다. ASP potassco 커뮤니티의 여러 다른 회원들이 유용한 의견과 솔루션을 제공했습니다. ASP에 대한 자세한 내용은 다음을 확인하십시오.https://potassco.org/