Another user created a very useful code for me, which i will be using to create random k-cnf formulas. I found a good sat-solver online which i want to use to check the satisfiability of the k-cnf formula. There is a problem though. The output is different from the sat-solver its input, i would like this to match, in order for me to feed the random generated k-cnf formulas to the sat solver.
Code for the k-cnf generator
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 ).
The predicate comma_list/2 can be used to transform a list of literals into a conjunction:
For example
?- 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).
when querying
?- random_knowledge_base(4, 3, 5, 0.5, KB).
The output
KB = [(p1, -p4, -p5), (p2, p3, p4), (p2, p3, -p5), (p3, -p1, -p4)].
But i want the output to stay int the "Ls" form, meaning that it would look like this
KB = [[p1, -p4, -p5], [p2, p3, p4], [p2, p3, -p5], [p3, -p1, -p4]].
Because eventually, i want the output to look like this, to match this input of the sat solver:
?- sat([[true-X,false-Y],[false-X,false-Y],[true-X,true-Z]],[X,Y,Z]).
where The solver is called with two arguments. The first represents a formula in CNF
as a list of lists, each constituent list representing a clause. The literals of a
clause are represented as pairs, Pol-Var, where Var is a logical variable and Pol
is true or false, indicating that the literal has positive or negative polarity. The
formula ¬x∨(y ∧ ¬z) would thus be represented in CNF as (¬x∨y)∧(¬x∨ ¬z)
and presented to the solver as the list
L = [[false-X, true-Y], [false-X,
false-Z]]
where X, Y and Z are logical variables. The second argument is a list
of the variables occurring in the problem. Thus the query sat(L, [X, Y, Z])
will succeed and bind the variables to a solution, for example,
X = false, Y
= true, Z = true.
As a by-product, L will be instantiated to
[[false-false,
true-true], [false-false, false-true]].
This illustrates that the interpretation of true and false in L depends on whether they are left or right of the - operator: to the left they denote polarity; to the right, they denote truth values. If L is unsatisfiable then sat(L, Vars) will fail. If necessary, the solver can be called under a double negation to check for satisfiability, whilst leaving the variables unbound.
Code for checking satisfiability
sat(Clauses, Vars) :-
problem_setup(Clauses), elim_var(Vars).
elim_var([]).
elim_var([Var | Vars]) :-
elim_var(Vars), (Var = true; Var = false).
problem_setup([]).
problem_setup([Clause | Clauses]) :-
clause_setup(Clause),
problem_setup(Clauses).
clause_setup([Pol-Var | Pairs]) :- set_watch(Pairs, Var, Pol).
set_watch([], Var, Pol) :- Var = Pol.
set_watch([Pol2-Var2 | Pairs], Var1, Pol1):-
watch(Var1, Pol1, Var2, Pol2, Pairs).
:- block watch(-, ?, -, ?, ?).
watch(Var1, Pol1, Var2, Pol2, Pairs) :-
nonvar(Var1) ->
update_watch(Var1, Pol1, Var2, Pol2, Pairs);
update_watch(Var2, Pol2, Var1, Pol1, Pairs).
update_watch(Var1, Pol1, Var2, Pol2, Pairs) :-
Var1 == Pol1 -> true; set_watch(Pairs, Var2, Pol2).
Anyone that could help would be my hero :) credits to @slago
ps if the output has to be restricted to a certain K, i.e. 3-cnf, to fit the sat solver, that would also be fine
The code must be altered as follows:
random_knowledge_base(NumberOfClauses,
LiteralsPerClause,
AmountOfLiterals,
Ratio,
KnowledgeBase,
Variables ) :- % <== Add output argument to get used variables
length(KnowledgeBase, NumberOfClauses),
length(Variables, AmountOfLiterals), % <== Generate a set of variables to be used
maplist(random_clause(LiteralsPerClause, AmountOfLiterals, Variables, Ratio), KnowledgeBase).
random_clause(LiteralsPerClause, AmountOfLiterals, Variables, Ratio, Literals) :-
randseq(LiteralsPerClause, AmountOfLiterals, Numbers),
maplist(literal(Ratio,Variables), Numbers, Literals).
literal(Ratio, Variables, Number, Literal) :-
nth1(Number, Variables, Proposition), % <== Map each number into a corresponding variable
( maybe(Ratio)
-> Literal = true-Proposition
; Literal = false-Proposition ).
Examples:
?- literal(0.5, [X,Y,Z], 1, Literal).
Literal = false-X.
?- literal(0.5, [X,Y,Z], 2, Literal).
Literal = true-Y.
?- random_clause(2, 3, [X,Y,Z], 0.5, C).
C = [false-X, true-Y].
?- random_clause(2, 3, [X,Y,Z], 0.5, C).
C = [true-Z, true-X].
?- random_knowledge_base(3, 2, 3, 0.5, K, V).
K = [[false-_A, false-_B], [false-_C, true-_A], [false-_B, false-_C]],
V = [_B, _A, _C].
?- random_knowledge_base(3, 2, 3, 0.5, K, V), sat(K, V).
K = [[false-true, true-true], [true-true, true-true], [true-true, true-true]],
V = [true, true, true] ;
K = [[false-false, true-true], [true-false, true-true], [true-true, true-false]],
V = [false, true, true] ;
K = [[false-true, true-true], [true-true, true-true], [true-false, true-true]],
V = [true, true, false] ;
false.
EDIT Use the following predicate to see the random knowledge base before the instatiations made by sat/2:
show(K, V) :-
copy_term(K-V, Kn-Vn),
numbervars(Kn-Vn),
format('Knowledge base: ~w\n', [Kn]),
format('Propositions..: ~w\n\n', [Vn]).
Example:
?- random_knowledge_base(3, 2, 3, 0.5, K, V), show(K, V), sat(K, V).
Knowledge base: [[false-A,true-B],[true-C,true-A],[false-A,false-C]]
Propositions..: [C,A,B]
K = [[false-true, true-true], [true-false, true-true], [false-true, false-false]],
V = [false, true, true] ;
K = [[false-false, true-true], [true-true, true-false], [false-false, false-true]],
V = [true, false, true] ;
K = [[false-false, true-false], [true-true, true-false], [false-false, false-true]],
V = [true, false, false] ;
false.