SCHEMA USERS GUIDE

Schema Documentation

kautz@cs.rochester.edu

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

Parse a list of schemas (see BNF syntax below) and return a list of clauses

in symbolic form.

(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

positive literals. The predicates that are used in observed

literals should only appear in test expressions in formulas in

"test.wff".

(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 literals

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. Suppose the file "test.soln" specifies a solution satisfying assignment, specified 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.)

(interpret "test.soln" "test.map" "test.out")

Reads in a DIMACS solution file "test.soln" of the format

specified above and a mapping file "test.map", and creates a

file "test.out" containing the positive literals in the

satisfying assignment in symbolic form.

Schema BNF

`<schema> = <option> | <type declaration> | <formula>
<option> = (option <option name> <integer expression>)
<option name> = compact | shadow
<type declaration> = (type <type name> <set expression>)
`

`<formula> =
<proposition> |
(not <formula>) |
(and <formula>*) |
(or <formula>*) |
(implies <formula> <formula>) |
(equiv <formula> <formula>) |
(all <variable> <set expression> <integer expression> <formula>) |
(exists <variable> <set expression> <integer expression> <formula>) |
(if <test> <formula>)
`

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

`<set expression> =
<type name> |
(set <term> <term>*) |
(range <integer expression> <integer expression>) |
(union <set expression> <set expression>) |
(intersection <set expression> <set expression>) |
(setdiff <set expression> <set expression>) |
(lisp <lisp list valued expression>)
`

`<term> =
<constant symbol> |
<integer expression> |
<variable> |
(<uninterpreted function symbol> <term>*)
<integer expression> =
<number> |
<variable> |
(<observed predicate symbol> <term>*)
(member <term> <set expression>) |
(not <integer expression>) |
(and <integer expression>*) |
(or <integer expression>*) |
(<operator> <integer expression> <integer expression>) |
(lisp <lisp integer valued expression>)
`

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

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 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. 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)".

Important note: nested quantifiers may not use the same variable name, unless the option SHADOW is set.

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 expressions. Expressions may include arithmetic functions (+, -, *, div, rem, mod), comparison functions (<, <=, =, >=, >, member), set composition functions (enumeration lists, union, intersection, setdiff), and logical functions (and, or, not). Note that logical functions in expressions are evaluated by the Schema interpreter and do not appear in the final CNF, unlike the logical operators that have the same names.

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.

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

; For example: (all x (set a b) 1 (implies (p x) (exists x (c d) 1 (q x))))

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 formula is linear in the size of the 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:

1. The output formula entails the input formula; and

2. Any model of the input formula can be extended to a model

of the output formula.

Condition 1 can also be expressed as:

1'. Any model of the output formula is also a model of the

input formula.

When no new propositions are introduced, the input and output formulas are equivalent.

Sanity Tests

After loading schema.cl run these to check that system

is working properly:

;;; Sanity tests:

;;;

;;; (parse '((exists y (range 3 5) t (p y (fun1 (* y y) (fun2 (+ y 1)))))) nil)

;;; ((OR (P 3 (FUN1 9 (FUN2 4))) (P 4 (FUN1 16 (FUN2 5))) (P 5 (FUN1 25 (FUN2 6)))))

;;;

;;; (parse '((type boys (set sam alex jon)) (all x boys t (equiv (lonely x) (not (exists y boys (neq x y) (friend x y)))))) nil)

;;; ((OR (NOT (LONELY SAM)) (NOT (FRIEND SAM ALEX)))

;;; (OR (NOT (LONELY SAM)) (NOT (FRIEND SAM JON)))

;;; (OR (FRIEND SAM ALEX) (FRIEND SAM JON) (LONELY SAM))

;;; (OR (NOT (LONELY ALEX)) (NOT (FRIEND ALEX SAM)))

;;; (OR (NOT (LONELY ALEX)) (NOT (FRIEND ALEX JON)))

;;; (OR (FRIEND ALEX SAM) (FRIEND ALEX JON) (LONELY ALEX))

;;; (OR (NOT (LONELY JON)) (NOT (FRIEND JON SAM)))

;;; (OR (NOT (LONELY JON)) (NOT (FRIEND JON ALEX)))

;;; (OR (FRIEND JON SAM) (FRIEND JON ALEX) (LONELY JON)))

;;;

;;; (parse '((all x (range 1 5) t (all y (range 1 5) t (if (neq x y) (different x y))))) nil)

;;; ((OR (DIFFERENT 1 2)) (OR (DIFFERENT 1 3)) (OR (DIFFERENT 1 4)) (OR (DIFFERENT 1 5))

;;; (OR (DIFFERENT 2 1)) (OR (DIFFERENT 2 3)) (OR (DIFFERENT 2 4)) (OR (DIFFERENT 2 5))

;;; (OR (DIFFERENT 3 1)) (OR (DIFFERENT 3 2)) (OR (DIFFERENT 3 4)) (OR (DIFFERENT 3 5))

;;; (OR (DIFFERENT 4 1)) (OR (DIFFERENT 4 2)) (OR (DIFFERENT 4 3)) (OR (DIFFERENT 4 5))

;;; (OR (DIFFERENT 5 1)) (OR (DIFFERENT 5 2)) (OR (DIFFERENT 5 3))

;;; (OR (DIFFERENT 5 4)))

;;;

;;; (parse '((all b (set sam alex) t (all g (set mary sue) (likes b g) (dates b g)))) '((likes sam sue) (likes alex mary) (likes alex sue)))

;;; ((OR (DATES ALEX SUE)) (OR (DATES ALEX MARY)) (OR (DATES SAM SUE)))