Misc

3-SAT solution V1

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

3-SAT v2

%%logica Literal, SatV

BoolHash(x) = (Abs(Fingerprint("a-" ++ ToString(x))) % 1000000 < 500000);

#Literal, SatV

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

Maybe() :- Random() > 0.5;

#RandomBool() = t :- t = (Random() > 0.5), t ~ Bool;

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

@Ground(Sat);
Sat() = List{{clause: List{{v:, p:} :- v in Range(3), p = BoolHash(i * 1000 + v)}} :- i in Range(5)};

@Ground(Literal);
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;

Variable(v) distinct :- Literal(c, v);

@Ground(V);
V(x) = SatV(x);
V(x) = (Random() > 0.5) :- ~SatV(), Variable(x);

ClauseSatisfied(c) distinct :-
    Literal(c, v, p),
    p = V(v);

SatSatisfied() :- Sum{1 :- ClauseSatisfied()} = Count{c :- Literal(c)};

@Recursive(SatV, 8);
@OrderBy(SatV, "col0");
SatV(x) = V(x) :- SatSatisfied();