如何避免Clingo/Gringo中无意义变体的过度接地？

问题背景 #

使用Clingo 5.7.1处理时间依赖ASP问题：某项目可在2025、2026或2027年启动，每年价值规则为：未启动时价值0，启动当年价值30，启动次年价值31，启动后第二年价值32。最终需对每年价值求和，但接地后出现无意义的求和结果（如2026年求和为61），导致接地过程阶乘式膨胀，计算耗时剧增。

原代码 #

% Time horizon
horizon(2025..2027).

% q(value, years from start)
q(30, 0; 31, 1; 32, 2).  

% choice of start year
{ start(Year) : horizon(Year) } 1.

% possible values depending on the year of start
value(Value, Year) 
   :- q(Value, Year - YearStart), YearStart <= Year, start(YearStart), horizon(Year).

% summation of values (in a real program, summation is performed for different objects, but it doesn't matter here)
summation(Q, Year) 
   :- Q = #sum { Value : value(Value, Year) }, horizon(Year).

问题原因 #

接地阶段Clingo尚未应用{ start(Year) } 1的唯一性约束，因此会生成所有可能start假设下的value/2事实。例如，若同时假设start(2025)和start(2026)，2026年既会有start(2025)带来的value(31,2026)，又会有start(2026)带来的value(30,2026)，求和后得到无意义的61。这些多余的组合导致接地规模急剧膨胀。

解决方案 #

方案1：约束每个年份仅对应一个有效价值 #

通过添加约束，确保每个年份最多存在一个value/2事实，从源头避免多值求和：

% Time horizon
horizon(2025..2027).

% q(value, years from start)
q(30, 0; 31, 1; 32, 2).  

% choice of start year
{ start(Year) : horizon(Year) } 1.

% 每个年份最多对应一个价值，排除多值冲突
:- value(V1,Y), value(V2,Y), V1 != V2.

% possible values depending on the year of start
value(Value, Year) 
   :- q(Value, Year - YearStart), YearStart <= Year, start(YearStart), horizon(Year).

% 未启动的年份价值为0
value(0, Year) :- horizon(Year), not value(_, Year).

% summation of values
summation(Q, Year) 
   :- Q = #sum { Value : value(Value, Year) }, horizon(Year).

方案2：直接基于唯一启动年份计算价值 #

跳过value/2事实的生成，直接结合start的唯一性计算每年价值，彻底避免多余组合：

% Time horizon
horizon(2025..2027).

% q(value, years from start)
q(30, 0; 31, 1; 32, 2).  

% choice of start year
{ start(Year) : horizon(Year) } 1.

% 直接计算每年求和结果，无需中间value事实
summation(Q, Year) :-
    horizon(Year),
    (start(YS), YS <= Year, q(Q, Year - YS);
     not exists start(YS) where YS <= Year, Q=0).

方案说明 #

两种方案均围绕确保每个年份仅对应一个有效价值展开：

• 方案1通过约束过滤多值冲突，保留原代码结构的同时消除无意义组合；
• 方案2简化逻辑，直接绑定唯一启动年份计算求和结果，接地效率更高。

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