Rosette – A solver-aided programming language that extends Racket

Nice! For constraint solving, I can also highly recommend to look into Prolog for some useful ideas.

For example, consider the use case of Rosetta that is shown on the page. In Prolog, we can express it as follows: First, let us define suitable operators, so that we do not need so many parentheses:

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

With these definitions in place, we can implement the SAT solver that is shown on the page as follows:

    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).

Thus, we can post:

    ?- 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.

On backtracking, all satisfying assignments of variables to truth values are reported. In this concrete case, there is only a single solution.

Interestingly, the Prolog version can not only be used to find satisfying assignments, but also to generate whole formulas that evaluate to true:

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

However, this particular enumeration is called unfair, since there are true formulas that will never be generated.