Rosette – A solver-aided programming language that extends Racket(emina.github.io)

    :- op(200, fy, ∧).
    :- op(200, fy, ∨).
    :- op(200, fy, ¬).

    sat(F) :- interpret(F, t).

    interpret(∧Ls0, T) :-
            maplist(interpret, Ls0, Ls),
            apply(and, Ls, T).
    interpret(∨Ls0, T) :-
            maplist(interpret, Ls0, Ls),
            apply(or, Ls, T).
    interpret(¬Expr, T) :-
            interpret(Expr, T0),
            not(T0, T).
    interpret(t, t).
    interpret(f, f).
    interpret(v(f), f).
    interpret(v(t), t).

    apply(and, Ls, T) :- foldl(and, Ls, t, T).
    apply(or, Ls, T) :- foldl(or, Ls, f, T).

    and(t, t, t). and(t, f, f). and(f, t, f). and(f, f, f).

    or(t, t, t). or(t, f, t). or(f, t, t). or(f, f, f).

    not(f, t). not(t, f).

    ?- sat(∧[v(R),v(O),∨[v(S),v(E),¬t], v(T), ¬v(E)]).
    R = O, O = S, S = T, T = t,
    E = f ;
    false.

    ?- sat(F).
    F = ∧[] ;
    F = ∧[∧[]] ;
    F = ∧[∧[], ∧[]] ;
    F = ∧[∧[], ∧[], ∧[]] .