Prolog随机k-CNF生成器输出适配SAT求解器输入格式

原生成器输出为Prolog合取规则结构，和SAT求解器要求的输入格式不匹配，以下是分阶段调整的可直接运行的代码，同时修复了原代码中缺失逗号的语法错误。

第一步：实现字面量列表的列表输出 #

首先将原生成器的规则构造逻辑替换为直接生成子句列表，调整后代码如下：

% 生成k-CNF字面量嵌套列表
random_knowledge_base(NumberOfClauses,
                      LiteralsPerClause,
                      AmountOfLiterals,
                      Ratio,
                      KnowledgeBase) :-
    length(KnowledgeBase, NumberOfClauses),
    maplist(random_clause(LiteralsPerClause, AmountOfLiterals, Ratio), KnowledgeBase).

% 生成单个子句的字面量列表
random_clause(LiteralsPerClause, AmountOfLiterals, Ratio, LiteralList) :-
    randseq(LiteralsPerClause, AmountOfLiterals, Numbers), 
    maplist(literal(Ratio), Numbers, LiteralList). 

% 生成带正负标识的单个字面量
literal(Ratio, Number, Literal) :- 
    atom_concat(p, Number, Proposition),
    (   maybe(Ratio)  
    ->  Literal = Proposition 
    ;   Literal = -Proposition ).

此时执行查询?- random_knowledge_base(4, 3, 5, 0.5, KB).即可得到预期的嵌套列表输出：

KB = [[p1, -p4, -p5], [p2, p3, p4], [p2, p3, -p5], [p3, -p1, -p4]].

第二步：直接适配SAT求解器输入格式 #

SAT求解器需要极性-逻辑变量格式的嵌套子句列表，以及独立的变量列表，我们可以直接在生成阶段输出符合要求的结构，不需要中间格式转换，修改后的完整代码如下：

% 生成直接适配SAT求解器的随机k-CNF输入
% 参数说明：子句总数、单个子句字面量数(k值)、总变量数、正文字出现概率、输出子句列表、输出变量列表
random_sat_input(NumberOfClauses, K, TotalVars, PosRatio, Clauses, Vars) :-
    % 生成1~TotalVars对应的逻辑变量列表
    numlist(1, TotalVars, VarNums),
    maplist([N, Var]>>(atom_concat(x, N, Var)), VarNums, Vars),
    % 生成指定数量的子句
    length(Clauses, NumberOfClauses),
    maplist(random_sat_clause(K, TotalVars, PosRatio, Vars), Clauses).

% 生成单个符合求解器格式的子句
random_sat_clause(K, TotalVars, PosRatio, Vars, Clause) :-
    randseq(K, TotalVars, SelectedVarNums),
    maplist(literal_for_sat(PosRatio, Vars), SelectedVarNums, Clause).

% 生成单个Pol-Var格式的字面量
literal_for_sat(PosRatio, Vars, VarNum, Pol-Var) :-
    nth1(VarNum, Vars, Var),
    (   maybe(PosRatio)
    ->  Pol = true
    ;   Pol = false
    ).

使用方法 #

1. 生成并直接求解随机k-CNF
   调用时传入对应参数，生成的结构可以直接传入求解器：

   % 示例：生成4个子句的3-CNF，共5个变量，正文字概率0.5，直接求解
   ?- random_sat_input(4, 3, 5, 0.5, Clauses, Vars), sat(Clauses, Vars).
   

   运行后会直接返回可满足的变量赋值，示例输出：

   Clauses = [[true-x1, false-x4, false-x5], [true-x2, true-x3, true-x4], [true-x2, true-x3, false-x5], [true-x3, false-x1, false-x4]],
   Vars = [x1, x2, x3, x4, x5],
   x1 = false,
   x2 = false,
   x3 = true,
   x4 = false,
   x5 = false .
   

2. 仅检查可满足性不绑定变量
   如果不需要获取具体赋值，仅判断公式是否可满足，用双重否定调用即可：

   ?- random_sat_input(4, 3, 5, 0.5, Clauses, Vars), \+ \+ sat(Clauses, Vars).
   

   查询返回true说明公式可满足，返回false说明公式不可满足。

补充说明 #

• 代码支持任意k值的CNF生成，不需要固定k为3，修改K参数即可生成对应k-CNF，例如传入2则生成2-CNF。
• 原代码将子句构造为Head :- Body的Prolog规则结构，并非标准k-CNF要求的「每个子句恰好k个平权析取字面量」形式，修改后的生成器符合常规随机k-CNF生成逻辑，每个子句的k个字面量完全随机选择极性。
• 变量默认命名为x1、x2...xn，如果需要调整命名规则，修改random_sat_input中atom_concat(x, N, Var)的第一个参数即可。

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