创建随机 CNF 公式序言

Question

对于我的论文，我正在研究知识库的特定属性以及这如何影响论证树的大小。我需要一个我已经拥有的 prolog 中的 sat 求解器，但我还需要一个创建随机子句的算法。 k-SAT 表示恰好长度为 k 的子句。为简单起见，我将 k 设置为 3，最大 4。我想将 K（每个子句的文字量）作为程序的参数。因此，如果我想要一个 3-sat，包含 1000 个子句和 300 个文字，那么我的程序应该创建一个包含 100 个长度为 3 的子句的知识库，其中所有这些文字都必须以一定比例的负数（50 /50 为简单起见）。我希望输出看起来像这样， Output: a set of clauses randomly created:

V1 :- V2, V3.

V2 :- -V3, -V4.

有人可以帮我解决这个问题吗？

Answer 1

Logtalk 提供了 user-extensible arbitrary library and QuickCheck support in its lgtunit developer tool. You can use both with most Prolog systems.

Answer 2

尝试做这样的事情：

random_knowledge_base(NumberOfClauses,
                      LiteralsPerClause,
                      AmountOfLiterals,
                      Ratio,
                      KnowledgeBase) :-
    length(KnowledgeBase, NumberOfClauses),
    maplist(random_clause(LiteralsPerClause, AmountOfLiterals, Ratio), KnowledgeBase).

random_clause(LiteralsPerClause, AmountOfLiterals, Ratio, Head :- Body) :-
    randseq(LiteralsPerClause, AmountOfLiterals, [Number|Numbers]),
    atom_concat(p, Number, Head),
    maplist(literal(Ratio), Numbers, Literals),
    comma_list(Body, Literals).

literal(Ratio, Number, Literal) :-
    atom_concat(p, Number, Proposition),
    (   maybe(Ratio)
    ->  Literal = Proposition
    ;   Literal = -Proposition ).

示例：

?- random_knowledge_base(5, 3, 9, 0.7, B).
B = [(p2 :- p5, -p6),  (p8 :- p3, p6),  (p9 :- p7, p2),  (p4 :- -p1, p6),  (p8 :- p1, p9)].

代码详解

ISO 谓词 atom_concat/3 连接两个原子形成第三个原子：

?- atom_concat(p, 2, A).
A = p2.

谓词maybe/1成功的概率为P，失败的概率为1-P:

?- maybe(0.5).
true.

?- maybe(0.5).
false.

形式为 (Condition -> Then ; Else) 的目标用作条件语句：

?- (maybe(0.5) -> writeln(positive) ; writeln(negative)).
negative
true.

?- (maybe(0.5) -> writeln(positive) ; writeln(negative)).
positive
true.

因此，例如，目标 literal(0.5, 1, L) 随机生成文字 p1 或 -p1:

?- literal(0.5, 1, L).
L = -p1.

?- literal(0.5, 1, L).
L = p1.

要在 1..M 范围内选择 K 个唯一的随机整数，我们可以使用 randseq/3。对于 K = 3 和 M = 5，我们有：

?- randseq(3, 5, Ns).
Ns = [4, 5, 2].

?- randseq(3, 5, Ns).
Ns = [1, 3, 2].

要将 K 任意整数列表转换为 K 对应文字列表，我们可以使用 maplist/3：

?- randseq(3, 5, Ns), maplist(literal(0.5), Ns, Ls).
Ns = [1, 3, 5],
Ls = [p1, p3, p5].

谓词 comma_list/2 可用于将文字列表转换为连词：

?- randseq(3, 5, Ns), maplist(literal(0.5), Ns, Ls), comma_list(B, Ls).
Ns = [1, 5, 3],
Ls = [p1, p5, p3],
B =  (p1, p5, p3).

?- randseq(3, 5, Ns), maplist(literal(0.5), Ns, Ls), comma_list(B, Ls), C = (p3 :- B).
Ns = [1, 4, 2],
Ls = [-p1, p4, -p2],
B =  (-p1, p4, -p2),
C =  (p3 :- -p1, p4, -p2).

把它们放在一起，我们有谓词 random_clause/4:

?- random_clause(3, 4, 0.5, C).
C =  (p3 :- p4, -p2).

?- random_clause(3, 4, 0.5, C).
C =  (p1 :- -p5, p4).

要创建一个随机知识库，例如包含 4 个子句：

?- length(KB, 4).
KB = [_, _, _, _].

?- length(KB, 4), maplist(random_clause(3,5,0.5), KB).
KB = [(p2 :-p1, -p3),  (p5 :-p2, p3),  (p3 :- -p4, p5),  (p3 :- -p1, p4)].

或者，使用谓词 random_knwoledge_base/5:

?- random_knowledge_base(4, 3, 5, 0.5, KB).
KB = [(p1 :- -p4, -p5),  (p2 :- p3, p4),  (p2 :-p3, -p5),  (p3 :- -p1, -p4)].

创建随机 CNF 公式序言

Creating random CNF formulas prolog

logic

prolog

logic-programming

conjunctive-normal-form

swi-prolog