Prolog 中 SAT 求解器的否定谓词 not/2
Negation predicate not/2 for SAT Solver in Prolog
我正在用 Prolog 编写 SAT 求解器。到目前为止,这是我能想到的:
cst(true).
cst(false).
is_true(cst(true)).
is_false(cst(false)).
and(A,B) :-
is_true(A),
is_true(B).
or(A,B) :-
is_true(A),
is_false(B).
or(A,B) :-
is_false(A),
is_true(B).
or(A,B) :-
and(A,B).
% not(A) :-
我卡在 not/1 上了。谁能给我一个线索?
请注意,我没有使用 Prolog 的否定来解释逻辑否定。所以我改为实现了第二个谓词 is_false(+F),如果公式 F 为假,则为真。
编辑:我的意思是标题中的 not/1,而不是 not/2!
所以你的想法很好,但不可能嵌套你的条款。解决方案是在形式逻辑中使用像“解释”这样的谓词:将 is_true
或 is_false
拖到整个术语中:
is_true(cst(true)).
is_true(and(A,B)) :-
is_true(A),
is_true(B).
is_true(or(A,B)) :-
is_true(A),
is_false(B).
is_true(or(A,B)) :-
is_false(A),
is_true(B).
is_true(or(A,B)) :-
is_true(A),
is_true(B).
is_true(not(A)) :-
is_false(A).
is_false(cst(false)).
is_false(and(A,B)) :-
is_true(A),
is_false(B).
is_false(and(A,B)) :-
is_false(A),
is_true(B).
is_false(and(A,B)) :-
is_false(A),
is_false(B).
is_false(or(A,B)):-
is_false(A),
is_false(B).
is_false(not(A)) :-
is_true(A).
?- is_true( or(not(and(cst(true), cst(false))), cst(false)) ).
true.
?- is_true( or(not(and(cst(true), cst(true))), cst(false)) ).
false.
?- is_false( or(not(and(cst(true), cst(true))), cst(false)) ).
true.
?- is_false( or(not(and(cst(true), cst(false))), cst(false)) ).
false.
我正在用 Prolog 编写 SAT 求解器。到目前为止,这是我能想到的:
cst(true).
cst(false).
is_true(cst(true)).
is_false(cst(false)).
and(A,B) :-
is_true(A),
is_true(B).
or(A,B) :-
is_true(A),
is_false(B).
or(A,B) :-
is_false(A),
is_true(B).
or(A,B) :-
and(A,B).
% not(A) :-
我卡在 not/1 上了。谁能给我一个线索?
请注意,我没有使用 Prolog 的否定来解释逻辑否定。所以我改为实现了第二个谓词 is_false(+F),如果公式 F 为假,则为真。
编辑:我的意思是标题中的 not/1,而不是 not/2!
所以你的想法很好,但不可能嵌套你的条款。解决方案是在形式逻辑中使用像“解释”这样的谓词:将 is_true
或 is_false
拖到整个术语中:
is_true(cst(true)).
is_true(and(A,B)) :-
is_true(A),
is_true(B).
is_true(or(A,B)) :-
is_true(A),
is_false(B).
is_true(or(A,B)) :-
is_false(A),
is_true(B).
is_true(or(A,B)) :-
is_true(A),
is_true(B).
is_true(not(A)) :-
is_false(A).
is_false(cst(false)).
is_false(and(A,B)) :-
is_true(A),
is_false(B).
is_false(and(A,B)) :-
is_false(A),
is_true(B).
is_false(and(A,B)) :-
is_false(A),
is_false(B).
is_false(or(A,B)):-
is_false(A),
is_false(B).
is_false(not(A)) :-
is_true(A).
?- is_true( or(not(and(cst(true), cst(false))), cst(false)) ).
true.
?- is_true( or(not(and(cst(true), cst(true))), cst(false)) ).
false.
?- is_false( or(not(and(cst(true), cst(true))), cst(false)) ).
true.
?- is_false( or(not(and(cst(true), cst(false))), cst(false)) ).
false.