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

2. CSato

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

CSato Object Constructors

    CSato::CSato();
    CSato::CSato(int inData, int inTrace);

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

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

    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

    int CSato::NumClauses();
    void CSato::PrintClauses();
    void CSato::PrintClauses(ostream & OutStream);

    void CSato::PrintTrue();

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

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

    int CSato::NumBranches();

Internal Public Functions

    void CSato::AddSolution(SATOINT Atoms[]);

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.

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

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.

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:

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

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.