Prolog 中 SAT 求解器的否定谓词 not/2

Question

我正在用 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!

Answer 1

所以你的想法很好，但不可能嵌套你的条款。解决方案是在形式逻辑中使用像“解释”这样的谓词：将 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 求解器的否定谓词 not/2

Negation predicate not/2 for SAT Solver in Prolog

prolog

logic

sat

negation