-
16-10-2019 - |
题
好吧,请原谅我对这件事的无知 ASP 最近几天。
考虑这个简单的例子
p.
s :- p.
以及在Clingo中运行程序后生成的相应输出:
$ ./clingo.exe ex.lp --number=0
Answer: 1
p s
SATISFIABLE
Models : 1
...
在可能的情况下生成的模型 p true
和公式 p -> s
.
但是,如果我想问一些需要绑架推理才能产生一些答案的查询;换句话说,我需要知道这一事实的可能解决方案 s true
. 。因此,“所谓的”示例应该如下:
s.
s :- p.
但不幸的是答案不包含 p
正如预期的。
$ ./clingo.exe ex.lp --number=0
% warning: p/0 is never defined
Answer: 1
s
SATISFIABLE
Models : 1
...
可以在ASP中以任何方式完成吗?
解决方案
我发现这不能在ASP(或至少在我使用的求解器中)本地进行。因此,绑架理论需要用问题建模,以得出预期的结果。
这是一个说明如何完成的示例。我没有时间彻底测试其效率,但它适用于一些基本示例。
资源: http://www.dbai.tuwien.ac.at/proj/arvis/#usage
% abduction.lp
%%%%%%%%%%%%% Preprocessing %%%%%%%%%%
% Remove tautological clauses
taut(C) :- pos(C,X), neg(C,X).
preprocessed_clause(C) :- clause(C), not taut(C).
% which variable is in which clause
var_in_clause(C,X) :- preprocessed_clause(C), pos(C,X).
var_in_clause(C,X) :- preprocessed_clause(C), neg(C,X).
%%%%%%%%%%%%% Guess a Candidate Solution %%%%%%%%%%
% S, a subset of hypotheses is a solution iff (1) and (2) hold
solution(S) :- hypothesis(S), not nosolution(S).
nosolution(S) :- hypothesis(S), not solution(S).
%%%%%%%%%%%%% (1) background theory is consistent with S %%%%%%%%%%
% guess an assignment for all variables
true_consistency(X) :- variable(X), not false_consistency(X).
false_consistency(X) :- variable(X), not true_consistency(X).
%% Solution must be true
true_consistency(S) :- solution(S).
%% Check for each clause in T whether it is satisfied
sat(C) :- preprocessed_clause(C), pos(C,V), true_consistency(V).
sat(C) :- preprocessed_clause(C), neg(C,V), false_consistency(V).
%% In case a clause is not satisfied, remove AS
notsat :- preprocessed_clause(C), not sat(C).
:- notsat.
%%%%%%%%%%%%%% (2) background theory and solution entail the manifestation%%%%%%%%%%
%% Find assignment, which is a counter-example to entailment
true_entail(X) | false_entail(X) :- variable(X).
% ordering over variables in preprocessed clauses
lowerThan(C,X,Y) :- var_in_clause(C,X), var_in_clause(C,Y), X<Y.
not_successor(C,X,Z) :- lowerThan(C,X,Y), lowerThan(C,Y,Z).
successor(C,X,Y) :- lowerThan(C,X,Y), not not_successor(C,X,Y).
not_infimum(C,X) :- lowerThan(C,Y,X).
not_supremum(C,X) :- lowerThan(C,X,Y).
infimum(C,X) :- not not_infimum(C,X), var_in_clause(C,X).
supremum(C,X) :- not not_supremum(C,X), var_in_clause(C,X).
% check if unsat
unsatupto(C,V) :- infimum(C,V), pos(C,V), false_entail(V).
unsatupto(C,V) :- infimum(C,V), neg(C,V), true_entail(V).
unsatupto(C,V) :- unsatupto(C,PreV), successor(C,PreV,V), pos(C,V), false_entail(V).
unsatupto(C,V) :- unsatupto(C,PreV), successor(C,PreV,V), neg(C,V), true_entail(V).
unsat(C) :- unsatupto(C,V), supremum(C,V).
unsat :- unsat(C).
% make sure that variables in manifestations and solution get the right truth value
false_entail(X) :- manifestation(X).
true_entail(X) :- solution(X).
% saturation
true_entail(X) :- variable(X), unsat.
false_entail(X) :- variable(X), unsat.
:- not unsat.
#show solution/1.
%#show manifestation/1.
%#show hypothesis/1.
%#show variable/1.
以及本文的问题中提供的示例:
% a_ex2.lp
% Variables V
variable("s";"p").
% Theory T over V
clause(1).
pos(1,"s").
neg(1,"p").
hypothesis("p").
manifestation("s").
输出:
$ ./gringo.exe abduction.lp a_ex2.lp | ./claspD.exe --number 0
claspD version 1.1. Reading...done
Answer: 1
solution("p")
Models : 1
Time : 0.002 (Parsing: 0.001)
不隶属于 cs.stackexchange