Minimal models for Propositional Formulas

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