Misc

3-SAT solution

Random() = x :- x = SqlExpr("Random()", {}), x ~ Num;

Maybe() :- Random() > 0.5;

Sat() = [{clause: List{{v:, p: true} :- v in Range(3)}},
         {clause: List{{v:, p: false} :- v in Range(3)}}];

Literal(clause_index, variable_index, positivity) :-
    clauses = Sat(),
    clause_index in Range(Size(clauses)),
    clause = clauses[clause_index],
    literal_index in Range(Size(clause.clause)),
    the_clause = clause.clause,
    literal = the_clause[literal_index],
    variable_index = literal.v,
    positivity = literal.p;

    
Satisfier(clause) = ArgMax{made_by -> Random() :- ClauseIsTrue(clause, made_by:)} :-
    ClauseIsTrue(clause) = 1;

Satisfier(clause) = ArgMax{v -> Random() :- Literal(clause, v)}:-
    ClauseIsTrue(clause) = 0;


@Recursive(V);
@Ground(V);
@Ground(ClauseIsTrue);

V(Satisfier(clause)) = positivity :-
    Literal(clause, Satisfier(clause), positivity);
V(null) = false :- V = nil, 0 = 1;
    
ClauseIsTrue(c, made_by? ArgMax= v -> okay) Max= okay :-
    Literal(c, v, p),
    satisfies = (p == V(v)),
    ~(V(v) = true, V(v) = false),
    okay = (if satisfies then 1 else 0);

ClauseIsTrue(c, made_by? ArgMax= -1 -> 0) Max= 0 :-
    Literal(c, v, p);