SWI-Prolog中调用findnsols出现不符合预期的行为求助

你的问题出在子目标的执行顺序以及forall/2处理自由变量的行为上。

当前goal/1的定义中，forall子目标先执行，此时V_1是自由变量，Prolog会通过predneg_on_obj(O,V_1)绑定V_1——但forall/2的设计是验证“所有满足条件的实例都能让动作成立”，而非生成变量绑定。当V_1未绑定的时候，forall内部的匹配逻辑会优先绑定V_1到第一个满足predneg_on_obj(block1,V_1)的值（即block1），后续检查block2的情况也成立，因此得到第一个解。但回溯时，变量未绑定的执行路径会意外枚举istypeobj/1的所有实例，即使forall条件不满足，这就导致block2被错误纳入结果。

调整子目标顺序 #

调换goal/1中子目标的顺序，先通过istypeobj(V_1)枚举所有可能的对象，再用forall验证条件：

goal(V_1) :- 
    istypeobj(V_1),
    forall(member(O, [block1,block2]), predneg_on_obj(O,V_1)).

这样修改后，V_1会先被实例化为block1或block2，再逐个检查是否满足条件：

• 对于block1：predneg_on_obj(block1,block1)和predneg_on_obj(block2,block1)都存在，条件成立。
• 对于block2：predneg_on_obj(block1,block2)不存在，条件不成立，因此不会被纳入结果。

替代否定式写法 #

如果你想避免forall/2处理自由变量的潜在问题，也可以用否定式实现相同逻辑（语义与forall完全一致）：

goal(V_1) :-
    istypeobj(V_1),
    \+ (member(O, [block1,block2]), \+ predneg_on_obj(O,V_1)).

这个写法的逻辑是：不存在任何O属于[block1,block2]使得predneg_on_obj(O,V_1)不成立，先绑定变量再验证，行为更直观。

内容的提问来源于stack exchange，提问作者hamster