ASSOCIATION FOR AUTOMATED REASONING

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

From the AAR President, Larry Wos...

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.

The Design and Performance of CSato: A Propositional Reasoning Object

Andrew E. Shaffer
Cornell University, Ithaca, NY 14853-2801
jepigar@sunlink.net

James J. Lu
Bucknell University, Lewisburg, PA 17838
jameslu@bucknell.edu

1. Introduction

This paper describes CSato1 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

{ p V q, ~ p V r, s V ~ q }

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;
  }
The result of compiling and executing the program is displayed below.2
( -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

2. CSato

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

CSato Object Constructors

There are two constructors:
    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".

Inserting and Creating Clauses

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 AddClause() starts a new clause with the given literals, but it does not restrict the clause to just those literals. More literals may be added via the method AddLit(), described next.

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

Solving

The following functions are used to solve the clause set and generate solutions. The argumentless function Solve() will solve for all solutions, while the second method will solve for at most NumModels. The return value of the function is the number of solutions found. A return value of 0 indicates that the given clause set is unsatisfiable.
    int CSato::Solve();
    int CSato::Solve(int NumModels);

Retrieving Solutions

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 SATOINTs (#defined to be ints) 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);

Other Functions

The NumClauses() member function returns the number of clauses in the clause vector. PrintClauses() prints the clauses to cout in "LISP" format, which the command line version of SATO can read when passed the command line argument "-f1". The second form simply allows an alternate output stream to be specified rather than cout. Prototypes of these functions are as follows.
    int CSato::NumClauses();
    void CSato::PrintClauses();
    void CSato::PrintClauses(ostream & OutStream);
Solutions either can be retrieved, as described previously via GetSolution() or GetDontCare(), or they can be printed directly via PrintTrue(). The output format can be seen from the example in the introduction section.
    void CSato::PrintTrue();
The function GetClause() returns a constant reference to a specified clause number.
    const vector <int> & GetClause(int c);
The functions SetupTime() and SolveTime() can be used to examine the time required by CSato to solve a given clause set.
    double CSato::SetupTime();
    double CSato::SolveTime();
Lastly, NumBranches() returns the number of branches explored in solving a given clause set.
    int CSato::NumBranches();

Internal Public Functions

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

3. Performance

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.

Lessons Learned and Future Work

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.

Acknowledgments

Work supported by the National Science Foundation under Grant No. CCR9731893.

Notes

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

References

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.

Results of the CADE Trustee Elections

Maria Paola Bonacina
(Secretary of AAR and CADE) E-mail: bonacina@cs.uiowa.edu

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.

Model Computation - Principles, Algorithms, Applications:
Report from a CADE-17 Workshop

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 Talks

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.

Toward a "Model Computation Manifesto"

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:

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

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.

Conference Calls

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