11

数理解析研究所講究録
第1148巻 2000年 11-16

知的自動証明機の提案と実装
Noriko H. Arai

Ryuji Masukawa
Hiroshima City University

4‐3‐1 Ozuka‐higashi, Asaminami‐ku, Hiroshima 731‐31 JAPANnarai@cs.hiroshima‐cu.ac.jp,

masukawa@log05.1ogic.cs.hiroshima‐cu.ac.jp
Abstract

In Arai (1996) [1], we introduced a new syste\ln forpropositional calculus, which gives a natural frame‐
work for combinatorial reasoning using “without

loss of generality” a.rgunlellt and brute force induc‐tion. Ill this paper, we in_{\overline{1}}p^{]eI}11e11t this system, Sim‐
ple Combinatorial Reasoning as a ground theore\ln1)rover . We adopt tableau and DLL expressed as se‐quent calculi for the base svslenlS and i_{1}nplement a
symmetry rule on it. We show that our prover suc‐cessfully finds symlnetries in many elementary com‐binatorial problems, which are known to be exponen‐tially hard for resolution and tableau, and automat‐
ically produce polynomial‐size proofs. Furthermore,
our provel. distinguishes those formulas which con‐tain sy_{1}nnletries and those which do not with highpossibility without loosing much time. As a result,the performance of our prover on randomly generated
forlllulas is as good as that of existing resolution ortableau provers.

1

Introduction

Since Haken found the first llard example for resolu‐

tion [13], lnany others were added to the list of tau‐
tologies which require superpolynomially long proofs

for resolution and analytic tableau [8]. Actually mostof the interesting conlbinatorial problems were foundhard for these proof systems. It was a depressing

news for the society of aut_{0}nlated theorem proving
since many of aut_{0}nlated provers adopt either reso‐
1\iota ltion or analytic tableau as their engines. However,it was a quite natural consequence when we ponder
how we h_{U1}11i1J1 being reason. We use different rea‐sonil
for different types of problems; algebraic ap‐
proach to the problems related to counting or 1i_{1}1ear

algebra, combinatorial approach to those related tographs. If we always take only one approach, w1_{1}ich
is purely logical analysis in case we adopt resolution

and analytic tableau, it is very likely that we end up
with exponentially long proofs.

What we suggest in this paper is to give‐up “only‐one” approach and to adopt different approaches todifferent types of problems in ground theorem prov‐

ing. The prover we designed in this paper features

two theorem prover. One is a DLL‐like sequent cal‐features the sylnmetry rule which allows the exploita‐tion of symmetries present ill a problem. It poly‐

nomially I ) roves the pigeonhole pri11ci_{P}1e , the mod‐kP^{rinci}Ples_{\tau} Bondy’s theo\Gamma enl_{\backslash }(^{\tau}1ique ‐Coloring prob‐
lem and mally other combinatorial 1) roblems, aJ1 ofthe\ln are knoWll to be hald for both reSo1_{11}\dagger i_{011} andtableau.

quite number of researchers sl_{1}are
Slaney’s opinioll: “I collsider svlnlnet\iota\cdot y to be oneof the n\overline{l}ost important topics of current research inground theore\ln proving” [15], not lnuch effort wasdone to design a theorem prover exploiting symme‐
Alth_{oU}g11

tries. One reason why people were not so enthusias‐

tic in adopting symmetries in the real prover is thatfinding symmetries seemed to be as time consuming

as exhaustive search anyway. When a fornlula coll‐tains n variables, the most naive program to searchfor symnletries will check all the permutations on 7?
variables_{\backslash }. 7?! permutations all together. The second
reason is that symmetry rule does not seem to makeany progress to shorten proofs for landolnly gener‐

ated formulas, the i_{11)}pleme11tati_{on} of synln1etr\}' rule
does not see\ln to in\tau P^{\Gamma}oVetlle average ti_{lneCO1}nplex-it}’. To make the situation worse, it was proved t1_{1}atfinding a permutation of the longest orbit in a given

forlnula is NP ‐complete, and asking two given for‐mulas are symmetric is as hard as the graph isomor‐

phism problem, which is conjectured not in the class

P[11] . However, we should not mislead these evi‐
dences to conclude that symmetry rules is effective

only in theory, but not in practice. These evidel3Ces
only tell us tllat we cannot always find the symme‐

tries hidden in forlnulas, and synnnetries will not give
us mnch when we focus on the randolnly generated

forlnulaS.

In this paper, we set our goal to de\downarrow`,ign a groundtheorem prover so that

1. it finds sy_{lnmet}ries in a pro_{I^{)}}ositi_{0}nal forlnula aslong as h_{U1}nan being can fi_{11}d the symmetries in
the corresponding first order formula, and

2. it can quickly decide whether sylnllletry rule isworth trying; it distinguishes forlnulas witl] alotof symmetries fro\ln those without them.
Notice that our goal does not contradict to any of

the P^{essi}1ni_{Stic} evidences.

soning. Introduced by Arai (1996), Simple Combi‐

The symmetry rule can be added to resolution,
tableau or sequent calculus. Since Krishnalnurthy
first pointed out that the symlnetry rule is effec‐

designed exclusively for combinatorial problems. It

had focused 011 the sy_{ln1\gamma 1}et_{1}\}^{r} rule in resolution [6][7]culus and the other is Simple Combinatorial Rea‐

natorial Reasoning is a propositional proof system

tive to shorten resolution refutations, the researchers12[14]. It was Benhamou and Sais who first presented
an algorithm how to implement the symmetry ruleon resolution [6]. Their strategy was to find a per‐mutation of the largest orbit in the given formula
before the nlaChi_{11e} started resolution procedure. It
was pointed out in [11] that fi_{11}ding a perlnutati_{on}of the longest orbit is an NP ‐complete probleln , but

Benhanlou and Sais allowed machine to backtrack

only for fixed amount of tilne, therefore their algo‐rithm has polynomial‐time complexity. They demon‐
strated their SLDI resolution prover with symmetryrule can aut_{oma}tical1_{\}} produce polynomial‐size refu‐tations for the pigeonhole principle. Unfortunately,
Benhamou‐Sais algorithm did not overwhelnl othertechniques without the symmetry rule mainly be‐cause of the following two reasons.

1. B‐S algorithm heavily depends on the form of
the input clauses, and it does not work when
we disturb its s\}^{r}nlmetrieS by throwing in someunnecessary clauses or additional variables.
2. It does not feature any subroutine whether weshould run the subroutine to find symnletries , ittries to find symmetries always. 1 Consequently,

we end up with poor average time‐complexity
although it nlay run dralnati_{Ca}11y fast for a slnall
class of interesting formulas.
To overcome these deficiencies, we implemented
our prover as a sequent-cal\mathbb{C}uluS‐type backward

search prover, called Godzilla in [4]. Godzilla does

not try to find synmietries in the input formula,but it finds them while breaking down the forlnula.
Godzilla almost always finds symmetries and pro‐duces proofs of size linear to the size of inputs forthe pigeonhole principle, the mod‐k principle, theclique‐coloring proble\ln without increasing the time‐complexity much.
However, the perforlnance of original Godzilla
turned out to be much poorer than existing DLL
provers for randomly generated forlnulas. One rea‐son is that DLL is theoretically faster than tableau,
and another is that Godzilla did not use any heuris‐
tic favor for randomly generated 3‐CNF formulas.
Another criticism against Godzilla was that the per‐formance of Godzilla on the combinatorial formulas

seemed to rely on how nicely the input formulas were
formulated. In this paper, we adopt both tableau

and DLL as the basis for new Godzilla so that we

can choose either of them according to the condi‐
tions satisfied by the input formula. As a good by‐effect, new Godzilla proves some colnbinatorial prob‐
lems which old model was not able to produce shortproofs. We discuss the detail in section 4. As aresult, the performance of Godzilla is inlprovcd con‐siderably. We experimented whether or not Godzilla
can appropriately find symlnetries when we shuffle
the input clauses.
This paper is organized as follows. In section
2, we analyze proofs for elementary combinatorial
problems. In section 3, we define a deterllullis‐
tic algorithm to simulate elementary con) binatorial
proofs line by line, and implement it as a theore\lnprover, Godzilla. In section 4.1, we delnonstrate how
Godzilla produces proofs for the set of the clauses of
1A hard example for B‐S algorithm can be found in [5]size n on ,? variables, the pigeonhole principle andthe clique‐coloring probleln , which surprisingly re‐semble to hun_{\overline{1}}an proofs. In section 4.2, we shuffle
the input clauses of the pigeonhole principle and see
whether Godzilla can still find sy_{111m}etries .

In sec‐tion 4.3, we exanune the perforn\overline{l}ance of Godzilla on
randonly generated formulas. It is a key for the \backslash ^{\neg}uccess of Godzilla not to increase tinle‐complexitv when
it is attacking an tauto\log\backslash 1laving no colnbillatol ial\cdot

model.

2

Simple Combinatorial Proofs

Ill this section, we informally define what el\epsilon m\epsilon niary
combinatorial proofs are, and discuss how to find thesymmetries hiddell in problenms and how to exploit
the\ln to obtain short proofs.
I3y analyzing proofs
for simple colnbinatorial problenrs step by step, we
try to extract the reason w1_{1}y these problems are so
straightforward for us while they are \exp_{0}nential1y
hard for many automatic pro\backslash e\Gamma s .

The pigeonhole principle is one of the lnost elemen‐tary combinatorial princil\supset le . The pigeollhole princi‐
ple states that there is no one- 01le mapping fron] t1_{1}eset of ,? +1 objects into the set ot ’? objects. T1_{11^{\nwarrow}}
principle i_{b} known to be hard for tableau, resolution
and even for bounded depth Frege s\backslash l stelns ’ although
the truth of the principle is clear for \iota 1S . The bestthing we can do to prove tlle 1) rinCiP^{le}111 resolutionv

is to go over all the 1) oSSible cases, ’ l ! cases all to‐gether, that is sliglltly better thall tlte iruth table.

An elelnentar_{\mathcal{Y}} proof of the pigeo1lh_{0}1e principle
uses mathelnatical induction on the nulnber_{1}'? , ofobjects in the dolnain, we assume that the pigeonhole
principle holds for n . and show t1_{1}at it also holds for
7z+1.

(Informal proof of the pigeonhole principle)

Let f be a mapping from \{r). 7l+\underline{)}\} to \{\{), , n+1\} .
With_{0}\iota 1t loss of g_{C^{1}ne1}aJit.v , we can assllnlet1\iota at.t'(1?+2) =n+1 . If theie exi_{3}ts an i\neq n+\sim) snch thatf(i)=n+1 . we are don\epsilon . S_{tt}1 ) pobeot1_{1e}1WiSe . Thenthe function f lestricted to \{(), . n\perp 1|\} is a \ln apP^{i_{1}l}g
to \{0, n\} . By the induction 11vpo\{hesi_{S} . it is notone- t_{0}-one , and so is not f(c_{1}et\iota.) .

The novelty of the proof g,i\iota en\backslash \cdot above is the line,“Without loss of generalit}
Here, we ullderstand\ldotsthat the situation off(n+2)=i(i=0, , n) ismerely a variant of the sit uation of f(n+2)=n\perp 1| ’we save till\overline{l}e by represenli_{1}(ex_{1)}onential1\}^{r})1\overline{1}1a11Y
cases by just one case.
We give another exan1p1_{GW}1_{1}ic1111aS slightly differ‐
ent I) roof structure. We dc\cdot fi_{11}en(11) by the set of allclauses of length n in n\iota arial ) leb . 11(1\perp) is d11 tlllsat‐
isfiable set of clauses. DAgoStill0 proved t1_{1}a'. thisproblem is hard for analytic tableau [10]: it requires

the proof of size at least l? !. w1_{1}ich is superpolynomialof 2^{n} \square (n) is informally proved as follows.

(Informal proof of \Pi(n) )muandiLet\prod_{1as}^p(\Pi7otaln').\cdotpr_{ea}).|l^{1 -}\perat\io ta_{O}e.Ho1w\cdote1,bhofte)(p_{n}deo1the]i_{St} )fVarib]epn)str1ifan([o\ta_{Y.e}yif|)o1qu_{V}a1entI(-l)BVt1einduCpari_{1\tug}v1\prod_{}^sa(n)|p_{1}foOl=Ttir-|
hyp_{oth}esls , II(n‐1) is true. (qed.)13

In this proof, again, we understand that \Pi(n) withthe assulnption p1 being true and that with the as‐sulllption p1 being false are isomorphic in structure.
Consequently, we represent exponentially many casesby just one case.
The main structure of these proofs is summarized

as follows.

1. The statement to be proved is a big disjunctionof subcases,

1\leq i\leq hAi
w1_{1er}eA_{i} andeach other.

A_{j}(1\leq i, j\leq h) a.re isomorphic

2. The formula A_{1} is reducible (using pure logic)

to an induction hypothesis, or \lrcorner 4_{1} has a shortproof.

We define elementary combinatorial proofs by thosehaving the structures satisfying the conditions (1)and (2) given above. Many combinatorial principles

are known to have elelnentary combinatorial proofs;
the nlod-k principle, the non‐unique endnode princi‐
ple and Bondy’s theorenl are few examples.
Now we try to simulate elementary combinatorial
proo& in the propositional setting. We assume that
formulas are expressed as CNF; the i_{11}p_{U}t fornlula isexpressed as a set of clauses, A=C_{1}ノ\wedge\cdots A C_{-’n}ノ and

C_{i}=l_{1}^{i}\vee\cdots\vee l_{m}^{i}.\cdot The first task is to understand thegiven formula, A , as a big disjunction of subcases.
In the case of the pigeonhole principle, there exists

a clauseA

C_{i}(1\leq i\leq n) such that=\vee\cdots V(C_{ノ}1\wedge\cdots ci-1\wedge l^{i}\wedge C_{i+1}1\wedge\cdots\wedge cn)(C_{arrow 1^{\wedge\cdots c_{i-1} }"\wedge l_{m}^{i}, \wedge C_{i+1} '\wedge\cdots\wedge C_{n}')and each ( C_{1} A . . C_{i-1}'\wedge l_{j}^{i}\wedge C_{i+1}\wedge\cdots\wedge C_{n} ) is
i_{SOlnor}Phic to the induction hypothesis.
The proof structure for \Pi(n) i,s different; there ex‐
ists a variable p such that A with the assumption p
and that with the assumption \overline{p} are both isomorp1_{1}ic
to the induction hypothesis.
The first kind of reasoning is most naturally ex‐pressed as tableau‐like sequent calculus, on tlle other
hand DLL‐like sequent calculus is more suitable toexpress the second kind.

The old prover we designed in [4] to simulate e1\cdot-

ementary combinatorial proofs was equipped onlywith tableau.

He11Ce_{I} it failed to find second kindof symmetries discussed above. To overcome this de‐ficiency, we design our prover so that it can choose
either tableau or DLL according to the type of the
input formula.

3

Theorem prover: Godzilla

3.1

Algorithm

In this subsection, we implement a ground theorem
prover, Godzilla, to simulate elementary combinato‐rial proofs discussed in the previous section. The al‐
gorithm of Godzilla consists of three parts. The firstpart is a tableau‐like sequent calculus, the second isa DLL‐like sequent calculus, and the t1_{1}ird part takes
care of the restricted permutation rule.

F_{\lrcorner}ach of the first and the second I ) art consists of

two subparts: Simplification and Branching. Silnpli‐

fication consists of three subroutines. \prime rhe first sub‐routine checks whether or not a gil\cdot en set of clauses
contains an axiom. We delete un13e\langle eS_{\backslash }Qary clauses

as much as possible in the second subroutine. The
third subroutine is the unit propagation (unit resolu‐tion). During unit propagation, the set of clauses isreordered. Branching divides the given set of clauses
to several subsets. Obviously, Branching is the maincause to blow‐up the size of proofs.

The third part of the algorithm checks whether or

not gi.ven two form.\iota 11_{\partial S} are .i\nwarrow omQfphi(^{\backslash }-. T.hi.s proce‐dure 1S called Musical‐ c_{・}/| air. It is quite lmpoftallt
not to play Musical‐Chair when it is hopeless thattwo given formulas are isomorphic, otherwise the av‐
erage performance of our prover will be quite poor
comparing to the existing Davis‐Putnam based the‐ore\ln prover. For this purpose, we inserted a proce‐dure called Checker to examine whether we S' llotlld

try lnusical‐chair or not.
Now we explain the flow of the algoritllm.

For
a technical reason, we describe the algorithm sothat the machine produces proofs for several sets ofclauses stored in a database.

Each set of clau8\rho s isexpressed as a sequence of clauses. called a sequent.
Each sequent S is labeled wit1_{1} the number of clauses
in S , denoted by len(S) , and a sequence of integers
seq (s) of length l_{Cn(}6' ) such t_{c}1\iota at the ith elenlell lin seq (s) is the size of the ith clause in S . We callseq (s) the characteristic sequence of S . Suppose thata sequent S’ is of the form
p_{1}p_{2}p_{3}, p4p5,\overline{p}_{1}\overline{p}4_{)}\overline{p}s\overline{p}5.

Then, len(S)=4a11d.s\epsilon q('S) is 3, 2, 2, 2.
We first run the subroutine Simplification for all
the sequents in the database in pararell. Next, wesend the database to Musical‐Chair.
In Musical‐
Chair new databases are f_{or1}ned . At last, we send

the new databases to Branching, and back to Sim‐plifi cation.
1.

FirSt_{1} check if all the e\downarrow e } nell.tSiI1 the databaseare pro_{I}) er sets of clauses.

2. (Simplification) Si_{1}np^{]i}ficati_{0}n consists of t hreesubro\iota ltilles.

(a) (Subro?\iota tine1) For each sequent

S in

the

database, check whether or not S contains
an axiorn: for son ) e literal t , both \{l\} and\{\overline{l}\} . If S contains an axiom, write “ S is
unsatisfiable. If S is an empty sequeut,
stop the whole procedure immediately andoutput “(The input is) satisfiable”. lf nof_{7}go to next subroutine(b) (_{L^{\backslash _{t} }' lb_{\Gamma}outi,?e2) For eac1_{1}S ill the database,find a literai l_{S\iota 1},C\grave{\iota}_{1} that tlleYe exists a clausecontaining l but there is lloriecQntaini_{1l}giarrow.
Delete all the clauses containing i . If thereis 11O such l , go to the next subroutine.

(c) (Unit Propagatio 7\downarow ) E^{\urcorner}o1^{\cdot} each sequent S intlle database, fi_{11}d a unit clause {1}. Delete
the clauses containing 1
Move all theclauses containing \overline{l} to t1_{1}e head of S , delete14(a) (Tableau) Without loss og generality, we as‐

the occurrences .of\overline{l}, and .go back to Subrou‐tine 1. Otherwlse, this 1S the end of Si111^{-}

sume t1_{1}atS is of the f_{or}111

plification, and go to Checker.

(_{ノ}^{v_{i} , (_{\circ,\sim}^{t},

3. In Checker, we divide the given database into
disjoint subdatabases.

\{l\}, (_{2}'.
for each l\in C_{\rfloor} .

O(n^{2}).)

expressed as follows.

S_{1} and S_{2} arec_{1},
c_{n}(=^{s_{1}})D_{1)}\ldots, D_{n}(=S_{\sim},)\ldots,size (C_{k})=size(D_{k}) for every 1\leq k\leq 7l . Sup‐
pose that C_{1} is a clause of the form l_{1}\cdots l_{m} and
D_{1} is of the form t_{i} . . t_{m} . Without loss of gen‐erality, we can assume that C_{1} and D_{1} are dis‐joint sets of literals. Define a permutation ,\tau bya product of transpositions as follows.
\pi=

Extend\pi(l_{1} t_{1})\cdots(l_{m} t_{m})so that\pi(l)=

tif\backslash equellt\backslash \neg\{p\}\cup S and
I_{p^{1J\}}}\cup S , to tl\iota e database. Send the new\{\pi(C_{2}), . . , \pi(C_{n}^{t})\}=\{D_{2)}\ldots, D_{n}\}database back to `\searrow_{l \gamma\}}p^{[_{l} fi\Gamma at\dot{l}0\gamma\prime .

6. If every sequent in c\backslash !er } database is unsatisfi‐
able, output “(The input is) unsatisfiable”.
When we input a sset of unsatisfiablecla\iota lses_{t}\{(_{-}^{v}1, \ldots, c_{n}\} , Godzilla produces a elementary co\lnbinatorial proof expressed as a directed acyclic graphso that every leaf of P is labeled bv an axiom. When
we input a set of satisfiable clanses, \{C_{1}', . \tau , (_{\eta}'\} ,Godzilla stops in\overline{l}11lediatelyw1_{1}en it finds a satisfy‐
ing valuation.
Time‐Complexity All of the subroutines are ac‐

colnplished in time O(n^{4}) where n is tlle size of t1_{1}einput. Hence, if the size of tîlc obtained proof is poly‐
nonlially bounded, the tinle ( 0\neg 1111^{)}1eXic\iota to obtaill \dagger 11e
proof is also polynolnially \dagger Jo tlllded. \dot{H}ence , we callassess the eificiency of (lodzilla by the size of proofs
generated by Godzilla. The ob\iota^{r}i_{0}u^{q} upper bound forthe size of proof is k 2^{n}, wllere ’ is the nulnber ofvariables contained in a given f_{ormt1}]_{\dot{\mathfrak{c}}}1 , and k the \iota\backslash ize\pi(\overline{l})Rename literals in S_{1} according to

Selld the new databaseand add two new

database consists of a single sequent, send

ber of combination is

C_{n}rences in S . Delete ` S frol)] tlle database,

When acharacteristic sequences. Pick two sequents S_{1}and S_{2} in the database. (Note that the nu\ln-(',1(b) (DLL) Pick a variable 1) of lnost occur‐

database into databases consisting of se‐quents so that S and S' are in the sanle

4. (Musical Chair) Now we are looking at a
database consisting of sequents having the same,back to Simplification.

(b) (Checker 2) Next, partition the givell

it to Branching.

.

add new sequellts

database into databases consisting of thesanle length of sequents. When a databaseconsists of a single sequent, send it toBranching.

scq(s_{)}=seq(S') .

.

where no literals ill (_{1}^{t} appears \ln otherclauses. Delete Sf\cdot ro\ln the database, and(a) (Checker 1) First, partition the given

database iff

.

=

\pi

.

as

t.

If

sets

of clauses, then delete C_{1\cdot\cdot Cn},,., from thedatabase because it is reducible to D_{2} , .. , D_{n}of the forlnula.

Memory The nunlber of sets of clauses stored in thelnemory is bounded by (nla.x clause length ) \cross(llunll)er
of variables). The size of each sets of clauses is

by using a symmetry rule. Otherwise, move allbounded by that of the input set

its negation to the end of the sequent i_{11}S_{1} . On

4

Experimental results

4.1

How Godzilla simulates human

the clauses containing a literal in (C_{1}-7r(C1)) or

the other hand, move the clauses w1_{1}ich contains
a literal in (\pi(D_{1})-D_{1}) or its negation to theend of the sequent in S_{2} . Send the obtained two

sequents back to Musical‐ Chair. If we are stillplaying on the same two sequents after running
this procedure n times, pick different conlbina‐
tion of sequents. When we finish checking all

the combinations, it is the end of Musical‐Chair.
For each sequent left in the database, form a new
database consists of the sequent, and send themto Branching.

5. When we receive a database from Musical‐ Chair,it always consists of a single sequent S. Branch‐
ing has two subroutines called Tableau and DLL .
In this paper. we adopt the following conditionas our heuristic to decide which we should apply

Tableau or DLL . If there exists a clause C suchthat no literals in C’ appears in other clauses in
S , go to Tableau. Otherwise go to DLL .

reasoning
We first demonstrate how Godzilla acts on colllbina‐

torial problems; \Pi(n) , the pigeonhole principle, čmdthe clique‐coloring problem.

The clique‐colorin g problem, denoted by k‐Test(n),states that if a graph contaills a k ‐clique, the graphcannot be properly colored by (k‐1) different colors.
To express the clique‐coloring problem in the propo‐

sitional calculus, we introduce three types of vari‐ables; one to express the clique function, one to ex‐press whether there exists a edge between given two
vertices, and another to express the coloring func‐
tion. In this m,odel\backslash \cdot ’ how we sllould permute “col‐oringvariables 1S,) deterlmned by the permntationof “edge vaI^{\cdot}iables , which is determined by that of“clique variables ; finding an appropriate permuta‐tion for the clique‐coloring problenl is a lot 1_{1}arderthan that for the pigeonhole principle.

15

Figurel, 2 and 3 shows comparison of performanceof Godzilla with and without

perlnutati_{on}rule2

for\Pi(n) , PHP(n) and (11‐1)‐Test(n) in CPU time.

Table 1 shows the number of leaves of the proofs

generated by Godzilla for these problerns.

160

wKh_{-^{S}}vmmelwp\mathfrak{l}arrow

no‐symmetry pi —

140

t20

Godzilla almost always finds necessary permuta‐
tions for these elementary combinatorial problems.

100

Furthermore, Godzilla applied DLL for II(n) andTableau for PHP(n) and (n- 1)- Test(11) , which wereappropriate decisions. The number of nodes in proofs
for \square (n) produced by Godzilla is about square root

80

60

40

of that produced by its old model.

20

0_{3}

\epsilon

6

9

10

11

Figure 1: Godzilla w/vs . w/0 symlnetries on \Pi(n).-\llcorner\cdot r\mathfrak{n}m-,.W^{\cdot}..m_{-}\cdot\prime^{\mathfrak{n}m\cdot\nu m}-,i;^{\ota'}i\epsilon 0;
l,isymmetries is much worse than the results in the pre‐vious subsection. It should be worth noting that cven

;
j

:.
;

,\primet:

0_{4}./':\prime'i

Figure 2:
PHP(n)

6aGodzilla w/vs .

that Godzilla seemed to find symmetries only when

The result shows that the chance for Godzilla to find;20

One of the main criticism against Godzilla in [4] was

Godzilla on 20 shuffled PHP(n) and take the average
number of leaves in the proofs generated by Godzilla.

.

40

Can Godzilla find symmetries
when input clauses are shuffled?

the input were formulated nicely. Table 2 shows how
the size of proofs increases when we shuffle the orderof clauses in the pigeonhole principle. We varied thenumber of pigeons from 5 to 13. For each n , we ran

t20

t\infty

4.2

t0

12

14

w/0 symmetries on

if a prover fails to recognize two formulas are isomor‐
phic only 1 out of 100 cases, the size of proofs may
still blow‐up exponentially. We need more techniques
to improve the ability to find symnletries when the
input formula is not formulated nicely. Analyzing
the proof produced by Godzilla on a shuffled pigeon‐hole principle with 7 pigeons, we observed that when
the sequents become longer, it is hard for Godzillato recognize two given sequents are isomorphic after
shuffling; it is hard to find symmetries in the begin‐ning of the proof. However, reordering process in theunit propagation helped Godzilla to find the symme‐
tries, and the possibility to find symmetries increases
towards the end of the proof.

When we extend Godzilla so that it can simulate

course‐of‐values induction, we obtain better perfor‐

Figure 3: Godzilla w/vs . w/0 symmetries on (n- 1)Test (n)As n) entioned in the previous section, the cost ofmusical‐chair has time complexity O(n^{4}) .

2Run times are in seconds and are for C version of Godzilla-ng on a AMD‐K6‐2 300MH_{Z} processor with 128 MB ram.

mance in finding symmetries for shuffled formulas ormore complicated problems. However, in return, theperformance for randomly generated 3‐CNF drops
severely because of the search‐space blow‐up.

4.3

How Godzilla acts on randomly

generated formulas

It is important for Godzilla bei_{1l}g succes,sful as a the‐orem prover that it does not loose much time when

16

it is attacking a problem which has little hope tocontain any symmetries, such as randomly generated
formulas. As described in section 3, Godzilla is en‐
dowed with a subroutine called Checker so that itstops immediately when the given sequent seems tobe asymmetric. Our preliminary experimellts showedthat when randomly generated 3‐CNF formulas arebroken into several sequents by Branching, only 3

References[1] N.H. Arai, “ \prime r_{r}actabi\grave{1}it_{v}v of cut‐freec_{JentZe}ntype propositional calculus wit1_{1} perrnutation
inference, Theoretical Computer Science, Vol.
170 (1996) 129‐144.

[2] N.H. Arai, “Tractability of cut‐free Gentzen

type propositional calculus with permutation in‐ference II”, to appear in Th eoretical Comput\epsilon r

cases out of 1000 passed Checker; Checker seems tobe quite effective to detect which sequents containsymmetries and which do not.

Scien ce.

[3] N.H. Arai, No feasible lnonotone i1lterp_{0}1ati_{on}for simple combinatorial reasolling”, to appear
in Theoretical Computer Science.

[4] N.H. Arai alld R. Masukawa, “How to find sy\lnmetries hidden in combinatorial ploblelns”, submitted.

[5] N.H. Arai and A. Urquhart, (‘Local symmetries
in propositional logic”, lnantlscript.

[6] B. Bellhamou and L. Sais, ‘Tractability throughsy_{lnmet}ries in propositional calculus”, Journalof Automated Reasonin g. Vol. 12 (1994) 89,102.

[7] W. Bibel, “Short proofs of the 1^{)}igeonholef_{0}r\ln\iota 1las based on the co11nPcti_{0}nlnt^{3}thod',Figure 4: Godzilla w/vs .

dom 3‐CNF

Jour' jalt^{)}j
Automated Reasoning, Vol. 6 (i990) 287‐297.

w/0 symmetries on ran‐[8] V. Chvátal and E. Szemerédi. 44Many Hard Ex‐

amples for Resolution”, J_{otr},lol (′f the Associa‐
tion for Co'?puting\Lambda I_{0}chine|^{\sim}y Vol. 35 (1988)

Figure 4 shows a comparison of Godzilla with andwithout symmetry rule on 50 variable randomly gen‐erated 3‐CNF in CPU time. We varied the numberof clauses from 170 to 300. Godzilla only lost 16\Psi e) oftime by having the symmetry rule. 35Conclusion

759‐768.

[9] J. Crawford, L. Auton, tExperilllental results on
the crossover point in sati_{S}fiaI )ility problenls”
Proc. of the 11th AAAI (1993) 21‐27.

[10] M. D’Agostino, ‘4Are tableaux an improvernellt

on truth‐tables?”, Journal of Logic, Language
and Information, Vol.1 (199^{\underline{l}}) 235‐252.

Our theoretical results show that permutation rule(or symmetry rule) has dramatic impact on reducing
the lengths of proofs for many combinatorial prob‐lems, which are hard for both resolution and tableau.
Moreover, our experimental results show that finding
symmetries in a given formula is not as hard as it was
believed when we adopt the sequent calculus for thebase system.

It is a key for the intellectual theorem proving how
accurately and how easily the machine can recognize
which field of mathematics a given problem falls in.
Then, we can apply algebraic technique, for exanlple
the cutting planes, for algebraic problems, symme‐
try rules for elementary combinatorial problems, andcommon resolution for randomly generated 3CNF' s .
In this paper, we used naive heuristics to distinguishwhether we should apply the symmetry rule or not,that worked quite successfully in the restricted set‐ting. We will need more delicate heuristic functions
when we extend our technique to prove problems
which have various types of lnathematical models.
3Godzilla is about 60 times faster than its old model [4] on

randomly generated 3CNF_{S}' .

[11]\Gamma . De la Tour and S. Delnli,

On f he conlI)lexit}

or extending ground resolutiol1 witl] \sim yl\Pi lnetryrules”, Proc. of the 1.,/ th IJCA I (199^{\ulcorner}.)) 289‐295.

[12] J. H. Gallier. Logic for Compu ‘l er S_{C\dot{l} c\gamma? ce, Jolm
Wiley&Sons, New York (1987).
[13] A.

Haken_{t}‘The intractability of resolutioni’,

Theoretical c_{0mpu}f\epsilon r

308.

Lb^{l}cle\prime lc\epsilon .

3^{t}J(1985) 297‐

[14] B. Krishnamurthy, “Short proofs for tricky for‐mulas, Acta Informatica, Vol22 (1985) 253‐275.

[1.\ulcorner)] J. Slaney, “The crisis in finite\Pi lathen_{\overline{1}}a\{ics :autonlated reasoning as cau\backslash e alld cure” ill
CADL^{1},- 1_{\sim}^{o}\rangle Nancy. ed. A I3ilnt^{\iota_{\dagger} |.\cdot.\backslash pringer Ver‐lag, LNAI 814 (1994) 113.