We look at metaprogramming in Julia. We illustrate parse
and eval
using the problem of determining a minimal model
for a given propositional formula. The computation of minimal models is of interest in answer set programming, as they
are used to define stable models 1. The problem of finding a minimal model is NP-complete,
whereas the problem of finding a stable model for a given set of propositional statements is $\Sigma_{2}^{P}$ complete.
A propositional variable takes only one of the two values, true or false. A variable that is assigned a value is called
a ground variable. A ground variable that takes on the value true is said to be valid. Variables can be connected using the
logical connectives, and (&), or (||), not (!), giving us propositional formulas. A model for a propositional formula
are the the ground propositional variables such that the propositional formula evaluates to true. We
represent the propositional statement as a string in Julia. The string can be parsed into an abstract syntax tree using
the function parse.
If all the variables in the string are grounded (a value is assigned), then the propositional
statement can be evaluated using the function eval.
wff = "(!a || b) &&(!b || c) &&(!c || a)"
a,b,c = false,false,false
eval(parse(wff))
The parse tree can also be visualized.
julia> wff = "(!1 || 2) &&(!2 || 3) &&(!3 || 1)"
julia> dump(parse(wff))
Expr
head: Symbol &&
args: Array(Any,(2,))
1: Expr
head: Symbol ||
args: Array(Any,(2,))
1: Expr
head: Symbol call
args: Array(Any,(2,))
typ: Any
2: Symbol b
typ: Any
2: Expr
head: Symbol &&
args: Array(Any,(2,))
1: Expr
head: Symbol ||
args: Array(Any,(2,))
typ: Any
2: Expr
head: Symbol ||
args: Array(Any,(2,))
typ: Any
typ: Any
typ: Any
Given a model M, we denote by T(M), the set of variables which are true. Model M is minimal if there is no model M’ such that T(M’) is a subset of T(M). Minimal models have a variety of uses. For instance, they are used to define “stable models” in answer set programming. Minimal models are unique for specific subclasses of propositional statements (logic programs without negation). Here, we write a procedure to find a minimal model M with the least cardinality of T(M) for a general propositional statement. The only way we know to solve such problems is to generate and test the potential models. This is precisely what we do.
If all the propositional variables are grounded, it is easy to check if the propositional formula is satisfied; evaluate it. So, we enumerate possible values for all the variables and check whether the propositional statement is satisfied for each possible grounding of the variables. We also take care not to explore the part of the tree which cannot lead to a smaller sized model.
The recursive function solve
below implements the strategy. It uses a global variable ub
to fathom the search.
Variable ub
is an upper bound on the cardinality of a minimal model discovered as of yet. Variable vars
is the list
of variables. Each variable in vars
is assigned a true/false value. Once all the variables are grounded, the
propositional statement is evaluated using the eval(parse()).
In case the formula evaluates to true, we update the
upper bound. The third argument is used to track the number of literals that are valid in the current model. The
recursive call occurs if the number of valid literals is less than the upper bound.
function solve(vars, cnf, val)
println(" ub=" , ub, " value=", val, " ", cnf)
global ub
if (ub > val)
if (vars == [])
if ((eval(parse(cnf)) == true))
ub = val
return true
end
return false
end
v = vars[1]
p1 = solve(vars[2:end], replace(cnf, v , "true"), val+1)
if (p1 == true)
return true
end
p2 = solve(vars[2:end], replace(cnf, v , "false"), val)
return p2
end
end
We can now find a minimal model as shown below.
global cnf = "(!1 || 2) &&(!2 || 3) &&(!3 || 4) &&(!4 || 5) &&(!5 || 1)"
global vars = ["1","2","3","4","5"]
global ub = 5
solve(vars, cnf, 0)
We can also perform the search starting with an upper bound of 1 and increase it by one til a minimal model is located. This strategy is called iterative deepening. The propositional statement “(!1 || 2) &&(!2 || 3) &&(!3 || 4) &&(!4 || 5) &&(!5 || 1)” has a minimal model in which all the variables are false. Check it out at the Julia prompt.
function model()
global cnf = "(!1 || 2) &&(!2 || 3) &&(!3 || 4) &&(!4 || 5) &&(!5 || 1)"
global vars = ["1","2","3","4","5"]
global ub = 1
ans = false
while (ub < length(vars))
ans=solve(vars, cnf, 0)
if (ans == true)
return true
end
ub = ub+1
end
return false
end
We can think of the propositional string as a program. The program is evaluated once all the variables in the program are
ground. The search function above writes and executes a large number of programs at runtime, without any recompilation
of the code. The code above treats the data in the string cnf
as code, at the time of evaluation. The code in the
string is treated as data when we replace the variables with the ground values. Such duality between code and data is
more natural to express and work with, in a particular style of dynamic languages such as LISP, Clojure, Julia.
The code is available here.
- Michael Gelfond, Vladimir Lifschitz: The Stable Model Semantics for Logic Programming. ICLP/SLP 1988: 1070–1080. ^