🚀 go-pugleaf

In article <NAKASHIM.92Dec4111659@uranus.etl.go.jp> nakashim@etl.go.jp (Hideyuki Nakashima) writes:

  $@1JED!w(JATR$@$G$9!#;d$N<ALd$KBP$7$F!"AaB.!"8f2sEzD:$$$FM-Fq$&$4$6$$$^$9!#(J
$@;(;v$KJ6$l$F%U%)%m!<$,CY$/$J$C$F$7$^$$$^$7$?!#(J

> $@IaDL$OLZ$NJ#;($5$8$c$J$/$F!$LZ$NC5:w$N%3%9%H$rLdBj$K$7$^$9$M!%(J
> $@$D$^$j!JLZ!\%"%k%4%j%:%`!K$GJ#;($5$,7h$^$k$o$1$G$9!%(J

> $@DL>o$O(J $@J?6Q;^J,$+$l?t(Jm^$@J?6Q?<$5(Jn (O(M^n))$@$G$9$M!%(Jand$@$+(Jor$@$+$O7W;;(J
> $@%*!<%@!<$K$O4X78$J$$$H;W$$$^$9!%(J


  $@<B$O!";d$O(J propositional satisfiability $@$NLdBj$rG0F,$KCV$$$F$$$?$N$G(J
$@$9$,!"$=$N;~$b!"$d$O$j!"(Jand $@$H(J or $@$N6hJL$O=EMW$G$O$J$$$N$G$7$g$&(J? $@A02s!"(J
$@$&$^$/@bL@$G$-$J$+$C$?$N$G!">/$7D9$/$J$j$^$9$,!"$b$&0lEY@bL@$7$^$9!#(J


  CNF (Conjunctive Normal Form) $@$K$*$$$F!"<!$N$h$&$JCM$r%Q%i%a%?$H$7$F!"(J
propositional satisfiability $@$NFq$7$5$r%b%G%k2=$9$kO@J8$r8+$+$1$?$N$,!"(J
$@$=$b$=$b!";d$,$3$N<ALd$9$k$-$C$+$1$G$9!#(J

	N: $@JQ?t$N?t(J
	K: $@@a(J(clause)$@$NCf$N%j%F%i%k$N?t(J
	L: $@@a$N?t(J

  $@$=$NO@J8$G$O!"<!$N$h$&$J%U%i%C%H$J9=B$$rBP>]$K$7$F$$$^$9!#(J

	(:and
	  (:or x1 (:not x2) x3)
	  (:or x1 (:not x3) x4)
	  (:or x1 x2 x5))

  $@$3$l$K$O!"(Jpropositional satisfiability $@$NLdBj$O!":G0-$N>l9g(J O(K^L) 
$@$N7W;;NL$@$,!"J?6QE*$J?6Iq$$$O$=$s$J$K0-$/$J$/$F!"(J O(N^2) $@$0$i$$$H$$$&(J
$@$h$&$J$3$H$,=q$$$F$"$k$h$&$K8+$($^$7$?!#(J($@;d$O!"$3$NJ,Ln$O>\$7$/$J$$$N(J
$@$G!"Bg4V0c$$$@$C$?$i%4%a%s%J%5%$(J)$@!#(J

  $@$=$3$G!"Kd$a9~$_$,$"$k(J And-Or $@LZ$K$J$C$F$$$k;~$O!"$I$&%b%G%k2=$9$k$N(J
$@$@$m$&$H$$$&$N$,!";d$NA02s$N<ALd$N0U?^$G$9!#$^$?!"2f!9$N9=J82r@O%W%m%0(J
$@%i%`$NJ8K!!&<-=q%G!<%?$NFbIt7A<0$O!"$3$N$h$&$J(J And-Or $@LZ$K$J$C$F$$$k$N(J
$@$G!"$3$N7A<0$N$^$^$G!"7W;;NL$r8+@Q$kJ}K!$,$"$k$H(J ($@$=$7$F$=$l$,0lHLE*$K(J
$@G'CN$5$l$?$b$N$G$"$k$H(J)$@!"$H$F$b4r$7$$$N$G$9!#(J

(:and
  x0
  (:or x1 x2)
  (:or x3 x4 (:and
               x5
               (:or x6 x7))))

  $@$G!"$3$N>l9g!"!V@a$N?t(J L $@!W$KAjEv$9$k$N$,!"!V(Jor $@$N?t!W$G$O$J$$$+$HD>(J
$@4QE*$K;W$C$?$N$G!"<!$N$h$&$J0U8+$K;j$C$?$o$1$G$9!#(J

> 	     ($@Bh(J1$@0F(J) $@A*8@(J(or)$@$N?t$r?t$($k(J           ---> $@$3$N>l9g(J 3 $@8D(J
> 	     ($@Bh(J2$@0F(J) AND-OR$@LZ$NMU(J($@@)Ls(J)$@$N?t$r?t$($k(J ---> $@$3$N>l9g(J 8 $@8D(J
> 
>      $@A4$F$N2DG=@-$rAmEv$?$j$GD4$Y$k$h$&$J:G0-$N%1!<%9$N7W;;NL$O!"A*8@$N?t(J
>    $@$N;X?t$G8z$$$F$/$k$h$&$K;W$$$^$9$,!"(J

  $@$b$7!"$3$N$h$&$JOCBj$r07$C$?O@J8$J$I$"$j$^$7$?$i!"65$($F2<$5$$!#(J

  $@59$7$/$*4j$$$7$^$9!#(J

--
-----
$@1JED>;L@!w#A#T#R<+F0K]LuEEOC8&5f=j(J
Masaaki Nagata, ATR Interpreting Telephony Research Laboratories
  TEL:    07749-5-1325, (Messages) 07749-5-1311
  FAX:    07749-5-1308
  E-MAIL: nagata@atr-la.atr.co.jp