Creating random CNF formulas prolog

Question

For my thesis, I am looking at specific properties of knowledge bases and how this affects argumentation tree sizes. I need a sat solver in prolog which I already have, but I also need an algorithm that creates random clauses. k-SAT means clauses of precisely length k. For simplicity, I will set k to 3, max 4. I want to give K (amount of literals per clause) as a parameter to the program. So if I want a 3-sat, with 1000 clauses and 300 literals, then my program should create a knowledge base with 100 clauses of length 3 where all of those literals randomly have to be spread out with a certain ratio of negative ones (50/50 for simplicity). I want the output to look like this, Output: a set of clauses randomly created:

V1 :- V2, V3.

V2 :- -V3, -V4.

could somebody help me with this?

Answer 1

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

Answer 2

Try doing something like this:

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 ).

Example:

?- 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)].

Detailed explanation of the code

• The ISO predicate atom_concat/3 concatenates two atoms to form a third one:

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

• The predicate maybe/1 succeeds with probability P and fails with probability 1-P:

?- maybe(0.5).
true.

?- maybe(0.5).
false.

• A goal of the form (Condition -> Then ; Else) works as a conditional statement:

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

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

• Thus, for example, the goal literal(0.5, 1, L) randomly generates a literal p1 or -p1:

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

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

• To choose K unique random integers in the range 1..M, we can use randseq/3. For K = 3 and M = 5, we have:

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

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

• To transform a list of K arbitrary integers into a list of K corresponding literals, we can use maplist/3:

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

• The predicate comma_list/2 can be used to transform a list of literals into a conjunction:

?- 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).

• Putting it all together, we have predicate 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).

To create a random knowledge base with, for example, 4 clauses:

?- 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)].

Or, using predicate 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)].