NEWSLETTER

No. 49, October 2000

**Contents**

From the AAR President

The Design and Performance of CSato

CADE Elections

Model Computation -- Principles, Algorithms, Applications

Conference Call: RTA 2001

The most recent CADE has already led to an interesting outcome: a draft "Model Computation Manifesto". I expect to see more about this subfield of automated reasoning, and I especially look forward to learning about some interesting applications. One of the areas that caught my interest in the draft manifesto was educational software; I would like to hear from AAR members about efforts in using automated proof systems for teaching logic or geometry or the like.

In September,
new members were elected to the CADE board of trustees.
I join Maria Paola Bonacina in congratulating the new officers.
I am pleased to note that our membership is increasing;
I would like to encourage all AAR members to take
an active role in AAR and CADE.
Participating in next year's IJCAR conference,
sending articles to the AAR newsletter,
and submitting papers to
the *Journal of Automated Reasoning*
are all excellent ways of promoting the field.

The next CADE will, as most of you know, be part of IJCAR, the International Joint Conference on Automated Reasoning, combining CADE, FTP, and Tableaux conferences. Need I say that I am delighted to see that "automated reasoning" is highlighted in the title? For more information, see the Web site.

*Andrew E. Shaffer*

Cornell University, Ithaca, NY 14853-2801

jepigar@sunlink.net

*James J. Lu*

Bucknell University, Lewisburg, PA 17838

jameslu@bucknell.edu

This paper describes `CSato`^{1}
a C **++** object
for propositional reasoning. `CSato` is adapted from SATO
(version 3.2 at the time of writing), which is a state-of-the-art
implementation of the Davis-Putnam procedure that has been applied
effectively to solve a number of problems [2,3]. The
interface of `CSato` has been developed based on our experience in
writing a number of application programs for experimenting with search
strategies in propositional reasoning. It aims to provide easy
programming access to the underlying facilities of SATO through
standard C++
facilities, including the standard template library
(STL). Using `CSato`, application programs may instantiate
multiple SATO objects to perform different reasoning chores.
Resulting solutions are easily retrievable for examination and
analysis.

As a very simple example, a clause in SATO is represented as a list of
(positive and negative) integers. Each integer corresponds to a
propositional variable, and the sign indicates its polarity. Using
`CSato`, we can create and solve (i.e., find the models of) the
set of clauses

through the following program. In the program, propositions
*p, q, r,* and *s* are represented as integers
1, 2, 3, and 4, respectively.

#include "CSato.h" #include <iostream> #include <vector> int main() { CSato solver(3, 1); // instantiate a CSato object vector <int> aClause(2); // create the first clause aClause[0] = -1; aClause[1] = 3; solver.AddClause(aClause); // create the second clause aClause[0] = 1; aClause[1] = 2; solver.AddClause(aClause); // create the third clause aClause[0] = 4; aClause[1] = -2; solver.AddClause(aClause); // solve for all models of the clause set solver.Solve(0); solver.PrintClauses(); // show the clause set solver.PrintTrue(); // show all models cout << "Solving Time: " << solver.SolveTime() << endl; cout << "Build/Setup Time: " << solver.SetupTime() << endl; } |

( -1 3 ) ( 1 2 ) ( 4 -2 ) % 0 3 There are 2 solutions. Solution #0 2 4 Solution #1 1 3 Solving Time: 0 Build/Setup Time: 0.01 |

In this section, we describe the
various groups of member functions that form the interface for ` CSato`.

CSato::CSato(); CSato::CSato(int inData, int inTrace);The options to the second constructor allow modifications to the TRACE and DATA variables that SATO uses while performing its search. The default constructor uses values resulting from the SATO command line "-d3 -t1".

The simple way of inserting a clause is as a vector of signed integers. Each sign indicates the polarity of the corresponding literal. The prototype of the member function is

void CSato::AddClause(const vector <int> & inVars);Note that a call to

Clauses can also be built an atom at a time. The `NewClause()`
method begins work on a new clause, and `AddLit()`
inserts the signed literal `lit` into the current clause.
`AddLit()` calls will continue to append to the current clause
until the next `NewClause()` or `AddClause()` call.

void CSato::NewClause(); void CSato::AddLit(int lit);

`Solve()`

will solve for
all solutions, while the second method will solve for at most
int CSato::Solve(); int CSato::Solve(int NumModels);

The member function `NumSolutions()` returns the number of
solutions found, and `GetSolution()` returns a constant
reference to solution number `s`. The format of the solution
is a vector of `SATOINT`s (`#define`d to be
`int`s) that corresponds to those atoms assigned true in the
solution. The related function `GetDontCare()` returns, for a
given solution number `s`, those atoms that are neither assigned
true nor false in the solution. Prototypes of these functions are as
follows.

int CSato::NumSolutions(); const vector <SATOINT> & GetSolution(int s); const vector <SATOINT> & GetDontCare(int s);

int CSato::NumClauses(); void CSato::PrintClauses(); void CSato::PrintClauses(ostream & OutStream);Solutions either can be retrieved, as described previously via

void CSato::PrintTrue();The function

const vector <int> & GetClause(int c);The functions

double CSato::SetupTime(); double CSato::SolveTime();Lastly,

int CSato::NumBranches();

void CSato::AddSolution(SATOINT Atoms[]);This function is used to communicate with the SATO code and does nothing outside of

A program that used the
`CSato` object and emulated SATO's behavior of reading clauses
in from a file was used to compare the performances of `CSato`
and SATO. Clauses attempted were instances of randomly generated Open
Crossword Puzzle Construction problems containing 100 to 180 words
[1]. The options "-f1 -d3 -t1" were passed to the
command-line version of SATO.

The following table compares the runtime using `CSato` and SATO
for each clause set size, where the clause set size and runtime
correspond to the average of 20 trials. Timings are gathered with the
*time* command. Results show that
the use of STL in `CSato` incurs a small performance overhead when
using `CSato`, in comparison to SATO. The performance of ` CSato` is otherwise comparable to SATO.

Average Clause Set Size | CSato |
SATO |
Difference |

5322 | 13.3675 | 12.429 | 0.9385 |

6082 | 16.8075 | 15.651 | 1.1565 |

6826 | 31.055 | 29.4645 | 1.5905 |

7594 | 27.8775 | 25.9985 | 1.879 |

8386 | 28.251 | 26.7355 | 1.5155 |

**Remark. **Stock SATO will not compile correctly with GNU
*g++*
as it uses older style C
prototypes and function declarations. GNU *gcc* was used to
compile SATO and GNU *g++* used to compile `CSato`
along with the modified SATO code that `CSato` uses.
Optimization was turned off when compiling.

The C++ interface described here provides a wrapper around SATO but
it does not fundamentally change the ways in which SATO behaves. In our
experience writing applications, a very desirable feature of ` CSato` (and of propositional reasoning systems in general) would be
the ability to interrupt and return the results of partial
computations. A related capability to resume
computation will also be useful. These features will enable
applications to decide, at various points, whether further searches
by `CSato` are necessary. It will also provide applications with
better abilities to direct the search of `CSato`, possibly as the
result of examining partial results. We aim to explore these and
other extensions to `CSato`.

1. `CSato` is available
from
a tarred file.

2. Details of compiling and linking `CSato` are included in the tar file.

3. A value of 0 for `NumModels` will solve for all solutions.

4. Specifically, *egcs* version "egcs-2.91.66 19990314/Linux (egcs-1.1.2 release)"

1. Lu, J.J.; Rosenthal, J.S.; and Shaffer,
A. E. *Crossword Puzzles: A Case Study in Compute-Intensive
Meta-Reasoning*. Proceedings of the Third International Workshop on
First-Order Theorem Proving (eds. Baumgartner and Zhang),
St. Andrews, Scotland, 2000.

2. Zhang, H.; and Stickel, M. Implementing the
Davis-Putnam Method. *J. of Automated Reasoning*,
24(1-2): 277-296, 2000.

3. Zhang, H. SATO:
An Efficient Propositional
Prover. *Proceedings of CADE*, 272-275. Springer-Verlag, 1997.

An election was held from the 1st through the 30th of September to fill three positions on the board of trustees of CADE Inc. Two positions were left vacant by Ulrich Furbach and William McCune, whose terms expired, and a third one was created to begin the implementation of the recently approved amendment on increasing the number of trustees. Ulrich Furbach, Michael Kohlhase, David McAllester, Andrei Voronkov and Dongming Wang were nominated for these positions.

Ballots were sent by electronic mail to all members of AAR as of the 31st of August, for a total of 445 ballots (up from 396 in 1999). Of these, 109 were returned with a vote, representing a participation level of 24.5% (down from 30% in 1999). The majority is 50% of the votes plus 1, hence 55.

The following table reports the initial distribution of preferences among the five candidates:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
Total |

U. Furbach | 41 | 24 | 11 | 9 | 24 | 109 |

M. Kohlhase | 23 | 22 | 14 | 8 | 42 | 109 |

D. McAllester | 23 | 22 | 21 | 5 | 38 | 109 |

A. Voronkov | 11 | 26 | 18 | 5 | 49 | 109 |

D. Wang | 11 | 8 | 18 | 2 | 70 | 109 |

No candidate reaches a majority right away, and since Dongming Wang turns out to be the weakest candidate (the tie with Andrei Voronkov in first preferences is broken by comparing second preferences), his votes are redistributed, yielding the following new distribution:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
Total |

U. Furbach | 44 | 25 | 14 | 12 | 14 | 109 |

M. Kohlhase | 25 | 23 | 13 | 29 | 19 | 109 |

D. McAllester | 24 | 27 | 17 | 21 | 20 | 109 |

A. Voronkov | 15 | 25 | 16 | 22 | 31 | 109 |

Again, no candidate reaches a majority, and Andrei Voronkov turns out to be the second weakest candidate. The redistribution of his votes yields the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
Total |

U. Furbach | 50 | 29 | 12 | 13 | 5 | 109 |

M. Kohlhase | 29 | 25 | 30 | 18 | 7 | 109 |

D. McAllester | 28 | 28 | 26 | 17 | 10 | 109 |

Again, no candidate reaches a majority, and David McAllester turns out to be the third weakest candidate by one vote. His votes are redistributed, producing the following table:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
Total |

U. Furbach | 66 | 23 | 11 | 8 | 1 | 109 |

M. Kohlhase | 32 | 45 | 21 | 9 | 2 | 109 |

Thus, Ulrich Furbach, current President of CADE Inc., is reelected for a second term on the board of trustees. At this point, his votes are redistributed, with the following result:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
Total |

M. Kohlhase | 39 | 17 | 11 | 31 | 11 | 109 |

D. McAllester | 35 | 26 | 9 | 32 | 7 | 109 |

A. Voronkov | 17 | 36 | 7 | 40 | 9 | 109 |

D. Wang | 16 | 11 | 12 | 56 | 14 | 109 |

None of the candidates has a majority to be elected, so that the votes need to be redistributed again. The weakest candidate is Dongming Wang by one vote, and his votes are redistributed as follows:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
Total |

M. Kohlhase | 43 | 16 | 27 | 17 | 6 | 109 |

D. McAllester | 38 | 28 | 20 | 19 | 4 | 109 |

A. Voronkov | 24 | 30 | 19 | 31 | 5 | 109 |

The weakest candidate is now Andrei Voronkov, and redistributing his votes gives the following situation:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
Total |

M. Kohlhase | 51 | 31 | 14 | 11 | 2 | 109 |

D. McAllester | 45 | 35 | 16 | 12 | 1 | 109 |

Technically, it is still necessary to redistribute McAllester's votes:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
Total |

M. Kohlhase | 75 | 19 | 9 | 6 | 0 | 109 |

thus, Michael Kohlhase has a majority and is elected. Returning to the table after Ulrich Furbach's votes were redistributed, and redistributing those of Michael Kohlhase also, one obtains the following matrix:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
Total |

D. McAllester | 54 | 13 | 24 | 16 | 2 | 109 |

A. Voronkov | 25 | 36 | 30 | 14 | 4 | 109 |

D. Wang | 20 | 12 | 50 | 21 | 6 | 109 |

After one more redistribution step, David McAllester, the Program Chair of CADE-17, is elected:

Candidate |
1st pref. |
2nd pref. |
3rd pref. |
4th pref. |
5th pref. |
Total |

D. McAllester | 59 | 19 | 23 | 7 | 1 | 109 |

A. Voronkov | 34 | 35 | 28 | 10 | 2 | 109 |

After this election, the following people (in alphabetical order) are serving on the board of trustees of CADE Inc.:

Maria Paola Bonacina (Secretary)

Ulrich Furbach (President, elected 8/1997 and reelected 10/2000)

Harald Ganzinger (Past program chair, elected 10/1999)

Claude Kirchner (Past program cochair, elected 10/1998)

Michael Kohlhase (Elected 10/2000)

David McAllester (Past program chair, elected 10/2000)

Neil V. Murray (Treasurer)

Tobias Nipkow (IJCAR 2001 program cochair)

Frank Pfenning (Vice-President, elected 10/1998)

David A. Plaisted (Elected 10/1999)

On behalf of AAR and CADE Inc., I thank Bill McCune, for his service as trustee during the past three years; Andrei Voronkov and Dongming Wang, for running in the election; and all the members who voted, for their participation; and I offer the warmest congratulations to Ulrich Furbach, Michael Kohlhase, and David McAllester on being elected.

*Peter Baumgartner*, Universität
Koblenz-Landau, Germany

Email: peter@uni-koblenz.de

*Chris Fermüller*, University of Technology Vienna, Austria

Email: chrisf@logic.tuwien.ac.at

In the following, we report on a workshop titled "Model Computation -
Principles, Algorithms, Applications" held during CADE-17, the *17th
Conference on Automated Deduction*, June 16, Pittsburgh, PA, USA. The
organizers were Peter Baumgartner, Chris Fermüller, Nicolas Peltier and Hantao
Zhang. The papers are collected at the
Web site.

We summarize the contents of the eight talks (2 invited, 6 contributed) of the workshop, which was attended by about twenty researchers. The final item of the workshop program was a panel discussion on the scope, importance, and future research issues in the rather diverse and broad field of model computation. We therefore conclude this report by outlining the main topics and challenges that became visible in this lively discussion.

The workshop started with an invited talk by *Alexander Leitsch* (TU Wien,
Austria), titled "Syntactic Model Building by Calculi". The starting point
was a broad classification of model building methods for first-order logics as
*semantic* vs. *syntactic* ones. The former category comprises mainly
finite domain search methods, where it is attempted to find a finite domain and
an interpretation of the elements of the signature so that a model for the given
clause set results. In Leitsch's group, research concentrates on the
syntactic method, however, and the talk gave an overview of the activities. The
idea behind the syntactic method is to compute model representations as the
result of derivations of accordingly equipped calculi. Typical questions
that arise when following this line concern how models are actually represented and
which formula classes can be decided by which calculi (and to push the
frontiers, of course). For instance, reasonable resolution methods to decide the
Gödel-Class and compute models are still not known.

In his talk "Topological Completeness of Propositional Int", *Gregori Mints*
(Stanford, USA) addressed a topic that, at first glance, does not seem to match
the main theme of the workshop: completeness of propositional intuitionistic
logic with respect to topological models. However, the suggested completeness
proof builds on an interesting model construction technique; and thus certainly
contributes to an often neglected topic in model computation: "nonstandard"
models for nonclassical logics.

*Chris Fermüller* (Technische Universität Wien, Austria) took a broad view in
his talk "Model Building for Non-Classical Logics" by proposing new research
aims for the development of model building techniques in intuitionistic and
modal logics, finite-valued logics, and fuzzy logics, thus going beyond the
"traditional" classical first-order logic.

*Wolfgang Ahrendt* (Universität Karlsruhe, Germany) addressed a core theme of
the workshop in his talk "A Basis for Model Computation in Free Data Types".
Free data types are of particular importance in the context of software
specification and verification - a setting where typically lots of unprovable
proof obligations arise. Being able to compute counterexamples - by means of
constructing models - is therefore of great significance. Although some open
issues remain, this contribution certainly provides some promising initial
thoughts.

The Davis-Putnam (DP) method still is a first-choice method for propositional
reasoning (and computing models). In his talk "Lemma Generation in the
Davis-Putnam Method", *Hantao Zhang* (University of Iowa, USA) presented a
new way to derive lemma clauses, which can dramatically improve the performance
of DP, in particular of Zhang's own implementation, SATO.

The next three talks reported upon have a clearly identifiable common theme: the
use of models to *guide the search* of refutational theorem provers.

The central idea in *Manfred Kerber*'s and *Seungyeob Choi*'s (both from the
University of Birmingham, England) talk "The Semantic Clause Graph Procedure"
is to select resolution steps based on the proportion of models that a newly
generated clause satisfies compared to all models given in an initially
determined reference class. (The talk was presented by Manfred Kerber.)

The Model Elimination (ME) procedure by *Marianne Brown* and *Geoff
Sutcliffe* (both from James Cook University, Australia) receives as
input
(besides the input clause set) a small model for a subset of the input clause set. This
model is used during ME derivations mainly to initiate backtracking earlier,
thus cutting the search space (often considerably). It was demonstrated
experimentally that the method works well in many cases, and, so far, possible
incompleteness was not an issue. The title of the talk (presented by Geoff
Sutcliffe) was "PTTP+GLiDeS: Using Models to Guide Linear Deductions".

The concluding talk was again an invited one: "Elements of
Theorem Proving Intelligence" by *David Plaisted* (University of North
Carolina, USA). Plaisted may look back to a great variety of theorem
proving methods developed by him and his coworkers over the years. The talk
summarized important elements for the construction of successful and
nevertheless general techniques used in his theorem provers. They are combined
in the "Ordered Semantic Hyper Linking" (OSHL) method. In particular, OSHL
makes use of models to guide the search for a refutation by explicitly modifying
an initially given model for the domain under consideration (e.g., set theory).

**Conclusions.**
An important conclusion that the organizers drew from the workshop is the
following: The surprisingly broad scope of the submissions (all, however, clearly
focusing on the topic of the workshop) suggests that "model computation" is a
much more general topic than initially envisaged by individual researches
contributing to particular problems in the field. In particular, many talks
presented challenges for model computation that go beyond finite model building
for classical first-order logic.

As a result of the panel discussion concluding the workshop, it was generally agreed that a "model computation manifesto" would help to clarify the nature, main challenges, and goals of this rather diverse field, and also would be useful for coordinating and promoting further activities. We hope that the interest in this field as demonstrated in the discussion by many participants with different research background remains active and thus will lead to the formulation of such a "manifesto" soon. In the following we kick off this process by summarizing some topics and trends that were mentioned at the workshop.

**What Exactly Is Model Computation?**
Already the different names that are sometimes attached to the field--model computation, (automated) model building, model construction,
model finding--indicate that there are many aspects to cover. The topics range
from deduction systems that (implicitly or explicitly) construct
models of input formulas to using (finite as well as term) models
for proof search pruning;
but also computational aspects of focusing on "preferred" models
(minimal models, circumscription, abduction, etc.)
and using model based deduction mechanisms for diagnosing
specification errors and similar applications are in the scope
of the field.
Considering classical
first-order logic, but also on various nonclassical logics, it should be
clear that already the investigation of suitable formalisms for the
(computationally adequate) *representations* of models is an
important issue, too.

Probably there is no point in trying to find a final and all-embracing definition of "model computation"; rather, the task here is to assist better awareness of the various topics and the connections between them.

**Aims and Challenges:**
In accordance with the many facets of model computation, its aims are
manifold.
However, we think that an important methodological and
foundational issue concerns the whole field and should receive
more attention:
Namely, to bring out more clearly that constructing and using models is not just
another subfield of automated deduction but rather a complementary and complex
task, which is rich in practical and theoretical challenges itself.
In particular, a lot of
already existing work in automated deduction and related fields
can and should
be viewed as contributions (also) to model construction.

**Applications:**
In attracting more attention to the field, convincing and feasible applications
will play a key role. We present an incomplete list of actual and potential
applications as emerging from the panel discussion, but also from work in
progress:

- Disproving conjectures (e.g., in algebra, geometry combinatorial logic, theory of calculi) by presenting counterexamples.
- Supplementing educational software (e.g., for teaching logics or elementary geometry) by model construction features.
- Assisting first-order model checking.
- Using models for proof search pruning (also for nonclassical logics), both in automated and interactive proof systems.
- Systems where "preferred" models play a rôle (e.g., minimal models in model-based diagnosis and configuration management tools).

**
Possible Research Topics/Open Issues:**
Many theoretical, methodological, and implementational issues
are still (largely) unexplored. We mention just a few relevant questions:

- What are the best strategies for combining proof search with model checking and/or model building?
- Which calculi and proof search strategies allow to extract efficiently the information needed for model construction?
- How complex are the tasks of clause/formula evaluation or testing equivalence of the represented models for various types model representations and classes of formulas?
- Which (additional) model computation features would users of existing proof systems (at different levels) appreciate?
- Which types of models for various non-classical logics should be used for model computation?

We hope that not only the workshop participants but also other members of the community will contribute to a more complete and organized formulation of the scope, aims and major challenges of model computation. The organizers certainly appreciate all kinds of contributions towards this goal.

To this end, we started a "model computation"; see the Web page, which is intended to reflect the actual state of developments.

**RTA 2001**

*Papers*

The 12th International Conference on Rewriting Techniques and Applications will take place at the Sea of Galilee, Israel, May 22-24, 2001.

Papers are solicited on all aspects of rewriting, including applications, foundations, frameworks, implementation, and semantics. Submissions should fall into one of the following categories: (1) regular research papers describing new results (up to 15 pages), judged on correctness and significance; (2) papers describing the experience of applying rewriting techniques in other areas (up to 15 pages), judged on relevance and comparison with other approaches; (3) problem sets (up to 15 pages) providing realistic and interesting challenges in the field of rewriting; and (4) system descriptions (up to 4 pages, with a link to a working system), judged on usefulness and design. Submissions must arrive no later than December 4, 2000. For further information, see the Web page.

**Note:**
A prize of 2001 NIS will be given to the best paper as judged by the
program committee.

*Workshops*

Anyone wishing to organize an RTA workshop should send by e-mail a proposal in postscript format to rta2001@score.is.tsukuba.ac.jp by November 20, 2000. Proposals should be no longer than two pages and should contain the following information: a short scientific justification of the proposed topic, its relevance to RTA 2001, the proposed format and agenda, the procedures for selecting papers and participants, duration and preferred period, and contact information for the organizers.

Gail W. Pieper 2000-10-03