This repository has been archived on 2023-08-20. You can view files and clone it, but cannot push or open issues or pull requests.
yap-6.3/packages/swi-minisat2/examples/pearl_examples.pl

55 lines
1.2 KiB
Perl
Raw Normal View History

2009-11-11 10:56:37 +00:00
:- use_module(library(cnf)).
:- use_module(library(minisat)).
:- use_module(adder).
%% Example, pg3
%%
%% ?- cnf(X==Y,Cnf).
%% Cnf = [[T], [-X, Y, -T], [X, -Y, -T]]
%% ?- cnf((X*Y)+(-X*Z),Cnf).
%% Cnf = [[T], [-T, T1, T2], [-T2, -X],
%% [-T2, Z], [-T1, X], [-T1, Y]]
%% Example, pg4
%%
%% ?- sum([X+Y,X*Y,X==Y,X xor Y],[S1,S2,S3],Psi).
%% Psi = (T1==X+Y)*(T2==(X==Y))*(T3==T1 xor T2)*(T4==T1*T2)*(T5==X*Y)*
%% (T6==X xor Y)*(T7==T5 xor T6)* (T8==T5*T6)*(S1==T3 xor T7)*
%% (S2==T4 xor T8 xor (T3*T7))* (S3==(T3*T7->T4+T8;T4*T8))
%% Examples, pg6
%%
%% ?- cnf(X==Y,Cnf), solve(Cnf).
%% X=0, Y=0
%%
%% ?- cnf(X==Y,Cnf), sat(Cnf).
%% Yes
%%
%% ?- sum([X+Y,X*Y,X==Y,X xor Y],Sum,F), cnf(F,Cnf), solve(Cnf).
%% X = 0, Y = 0
%% Sum = [1, 0, 0]
%%
%% ?- sum([X+Y,X*Y,X==Y,X xor Y],[0,1,0],F), cnf(F,Cnf), solve(Cnf).
%% X = 0, Y = 1
%%
%% ?- sum([X+Y,X*Y,X==Y,X xor Y],Sum,F), cnf(F,Cnf),
%% maximize(Sum,Cnf), solve(Cnf).
%% Sum=[1,1,0]
%% X=1, Y=1
%% Figure 3, pg 6
%%
%% partialMaxSat(+,+).
partialMaxSat(Phi,Psi) :-
sum(Psi,Max,SumPsi), cnf(Phi*SumPsi,Cnf),
maximize(Max,Cnf), solve(Cnf).
%% Example, pg 7
%%
%% ?- partialMaxSat(X+Y,[X*Y,X==Y,X xor Y,-X+Y, -X, -Y, X]).
%% X = 1, Y = 1