SCHEMA USERS GUIDE

henry.kautz@gmail.com

Schema is a language for specifying propositional logic theories using a first-order logic-like syntax. The Schema interpreter produces propositional CNF (conjunctive normal form) which can be input to any satisfiability testing program.

The Schema interpreter is written in Common Lisp, but it is not necessary to know how to program in Lisp in order to use Schema.

Using Schema

Invoke any implementation of Common Lisp, and load the file "schema.el". The following Lisp functions are available:

(parse '(SCHEMA ...) '(OBSERVATION ...))
Parse a list of schemas (see BNF syntax below) and return a list of clauses in symbolic form. Each OBSERVATION is a ground atom that is asserted to be true. When the schemas are expanded, they are simplified by replacing observed atoms by 1 (true) and all non-observed atoms that employ the same predicates by 0 (false).

(instantiate "test.wff" "test.scnf" &optional "test.obs")
Reads the Schema file "test.wff", instantiates it, and saves the result in symbolic conjunctive normal form in the file "test.scnf". The optional file "test.obs" contains a sequence of observed ground atoms.

(propositionalize "test.scnf" "test.cnf" "test.map")
Reads the symbolic conjunctive normal form file "test.scnf" and creates a DIMACS format CNF file3 "test.cnf". In DIMACS format (the standard input language for all modern SAT solvers), propositions are represented by positive and negative integers. The mapping from symbolic ground atoms to integers is written to the file "test.map". The file "test.cnf" may then be sent to a SAT solver, such as Minisat or walksat.

(interpret "test.soln" "test.map" "test.out") Reads in a DIMACS solution file "test.soln" and a mapping file "test.map", and creates a file "test.out" containing the positive literals in the satisfying assignment in symbolic form. Tbe file "test.soln" specifies a solution by a sequence of positive and negative integers. If for some integer, neither the integer nor its complement appears, then it is assumed to be false (negative) for the assignment.

Examples

    ;; Define set types boy and girl
    (type boy (set jon alex max))
    (type girl (set mary sue ann))
    
    ;; A lonely boy is one with no male friends
    (all x boy t 
        (equiv (lonely x) 
                (not (exists y boy (neq x y) (friend x y)))))

    ;; if a boy likes a girl they are both happy
    (all x boy t 
        (all y girl (likes x y) 
            (and (happy x) (happy y))))

    ;; all boys know each other
    (all x boy t 
        (forall y boy t 
            (if (neq x y) (knows x y))))

    ;; Define range type time
    (type time (range 1 100))
    ;; Define set type block
    (type block (A B C))
    
    ;; Preconditions and effects of move
    
    (all t time t
        (all (x y z) block (alldiff x y z)
             (implies (move x y z t)
                      (and
                          (clear x t)
                          (on x y t)
                          (clear z t)
                          (on y z (+ t 1))
                          (clear y (+ t 1))
                          ((not (clear z (+ t 1))))))))

Language

A Schema program consists of a sequence of options, type declarations, and formulas. Options control certain details of the intrepreter. Type declarations bind type names to sets of Herbrand terms. Formulas are composed, as in first-order logic, of predicates, variables, constants, function symbols, logical connections, and quantifiers. The basic function of the Schema interpreter is to instantiate the variables in each formula and convert the result to CNF.

Formulas are specified in prefix (LISP) notation. The quantifiers, all and exists, iterate over sets of Herbrand terms. Terms are integers, constants, or complex terms built using uninterpreted function symbols. A quantified formula is represented by a list containing the quantifier, a variable, a set of terms, a test (integer) expression, and the subformula to which the quantification is applied. The subformula is instantiated only for bindings of the variable for which the test is true (not equal to 0). For example,

(all x (range 1 10) (= 0 (mod x 2)) (p x))

can be read, "for all x in the range 1 through 10, such that x is even, assert (p x)".

Propositions are expressed in Schema as either atomic symbols or complex propositions specified by a list beginning with a predicate followed by zero or more terms. Terms can be built from interpreted functions such as + and uninterpreted function symbols. For example, the literal expression (winner john (round (* 3 8))) is instantiated as

(winner john (round 24))

where "winner" is a predicate, "john" is a simple term, "round" is an uninterpreted function symbol, and "(round 24)" is a complex term.

The integer values 0 and 1 are used to represent false and true respectively in intger expressions. Integer expressions may include arithmetic functions (+, -, *, div, rem, mod), comparison functions (<, <=, =, >=, >, member, eq, neq, alldiff), set composition functions (enumeration lists, union, intersection, setdiff), logical functions (and, or, not), and observed predicates. Non-observed predicates may not appear in an integer expression. Note that logical functions in integer expressions are evaluated by the Schema interpreter and do not appear in the final CNF, unlike the logical operators that have the same names.

Observed predicates are useful for describing fixed relationships in a problem instance. For example, consider representing problems about a robot that can move between rooms that are connected. The schema file would contain general rules movement. The observation file would specify the way the rooms are connected, for example:

(connected R1 R2)
(connected R3 R4)
(connected R3 R5)

Making "connected" an observed predicate instead of an uninterpred predicate has several advantages:

The closed world assumption is automatically applied. In the example above, (not (connected R1 R5)) is implicitly asserted.
The predicate may be used inside test expressions.
The instantiated formula is smaller.

Comments begin with ;; (double semicolon) and extend to the end of the line.

Schema BNF

<option> = (option <option name> <integer expression>)

<option name> = compact | shadow

<type declaration> = (type <type name> <set expression>)

<proposition> = <predicate symbol> | (<predicate symbol> <term>*)

<term> = <constant symbol> | <integer expression> | <variable> | (<uninterpreted function symbol> <term>*)

<operator> = + | - | * | div | rem | mod | < | <= | > | >= | = | eq | neq | ** | bit

Options

(option compact-encoding 1) ; Allow new propositions to be created to reduce the size of the instantiated formula, as described below (default).

(option compact-encoding 0) ; Do not create new propositions.

(option shadow 0) ; Do not allow the same variable name to be used in nested subformulas (default).

(option shadow 1) ; Allow an inner quantified variable to shadow an outer variable of the same name.

Compact Encodings

The input formulas need not be in conjunctive normal form. Converting a formula to CNF using only the user-defined propositions can cause its size to increase exponentially. By creating new propositions, the Schema interpreter can guarantee the output CNF formula is linear in the size of the non-CNF instantiated input formula. Where

M = number of input formulas
L = length of the longest input formula
D = size of the largest set appearing in a quantification statement
N = deepest nesting of quantifiers in a formula

the size of the output CNF is O(M*L*D^N)

When new propositions are introduced in this manner, the relationship between the input and output formulas is that the output formula entails the input formula and any model of the input formula can be extended to a model of the output formula.