数理解析研究所講究録
918 巻 1995 年 277-291

277

Gr\"obner Bases for Set Constraints
Yosuke Sato
Dept.of Computer Science Ritsumeikan University
1916,Kusatu,Siga,525-77, Japan-mail:$\mathrm{h}^{-}\mathrm{o}\mathrm{j}\mathrm{i}_{\mathrm{C}}\mathrm{h}\mathrm{o}$)$\mathrm{E}$$\mathrm{t}’\backslash$\mathrm{y}\mathrm{s}\mathrm{a}\mathrm{t}\mathrm{o}^{\mathrm{i}_{\backslash }}\subseteq\mathrm{J},$\mathrm{h}e\mathrm{o}\mathrm{r}\mathrm{y}_{\mathrm{C}\mathrm{s}.\mathrm{r}}.\mathrm{i}\mathrm{t}\mathrm{S}\mathrm{u}\mathrm{m}\mathrm{e}\mathrm{i}.\mathrm{a}\mathrm{c}.\mathrm{j}\mathrm{p}$Abstract))
Tliis
proposes theofbases to solve set constraints
given in terms ofsuchand . Set constraints can be represented
tlle form of polynomial equations of a certain Boolean ring,
we canapply Boolean Gr\"obner ses we introduced in order to handle )ideals ofBooleanrings. In tllis
we study Boolean Gr\"obner bases in Inore
detail and sllow
several nice ) )which do not necessarily
for standard. Using these
we describe
weapply
Boolean Gr\"obIler b&ses to solve set constraints.
$1\mathrm{i}_{\mathrm{C}}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{I}1$$\mathrm{p}\mathrm{a}_{1}$$\mathrm{G}\mathrm{r}\ddot{\mathrm{o}}\mathrm{b}_{\mathrm{I}}1\mathrm{e}\mathrm{r}$$\mathrm{e}\Gamma$$\mathrm{a}\mathrm{p}\mathrm{I}$$\mathrm{s}\mathrm{y}_{\mathrm{I}\mathrm{n}\mathrm{b}\mathrm{o}1}\mathrm{s}$$\dot{\mathrm{c}}\mathrm{L}\mathrm{S}\cap.\cup.\subseteq.\in$$\not\in$$\mathrm{i}\mathrm{I}\mathrm{l}$$1_{1}\mathrm{e}\mathrm{n}\mathrm{c}\mathrm{e}$$\mathrm{b}\mathrm{A}$$\mathrm{o}\mathrm{l}\mathrm{y}\mathrm{I}\mathrm{l}\mathrm{o}\mathrm{I}\mathrm{f}\mathrm{l}\mathrm{i}\mathrm{a}\mathrm{l}$$1$)$\mathrm{o}\mathrm{l}\mathrm{y}_{\mathrm{I}1}\mathrm{o}\mathrm{I}\mathrm{I}\mathrm{l}\mathrm{i}\mathrm{a}1$$\mathrm{r}$$\iota y\mathrm{a}_{\mathrm{I}^{)}}\mathrm{e}\mathrm{r}$$\mathrm{e}\mathrm{r}\mathrm{t}\mathrm{i}\mathrm{e}\mathrm{s}$$\mathrm{t}1_{1}\mathrm{e}\mathrm{y}\iota_{1\mathrm{a}}\mathrm{V}\mathrm{e}$$\mathrm{I}$$\mathrm{G}\mathrm{r}\ddot{\mathrm{o}}\iota$1)$1_{1\mathrm{O}}1\mathrm{d}$$\mathrm{r}\mathrm{o}_{\mathrm{I}}$$\mathrm{n}\mathrm{e}\mathrm{r}\mathrm{b}\dot{C}\mathrm{k}9\mathrm{e}\mathrm{S}$$1_{1}\mathrm{o}\mathrm{w}$$1^{\mathrm{J}\mathrm{r}\mathrm{o}}\mathrm{P}^{\mathrm{e}}\mathrm{r}\mathrm{t}\mathrm{i}\mathrm{e}\mathrm{s}$$\mathrm{C}\mathrm{A}1$

Introduction

In constraint programlning, there are often applications in which we want to solve constraints written in terms of melnbership or inclusion of sets such as and . Since a)family of sets is naturally interprete, as a Boolean ring,of such constraints, calledt,his
set constraints inpaper, can be represented bv polynomial equations over Booleallrings of sets. For example, the constraints $a\in X,$ $b\not\in Y$ and $X\subseteq Y$ , whereareconstant, symbols of elements and X,
are variables for sets, are represented by the equa,tions $\{a\}X=\{a\},$ $\{b\}Y=0$ and $X\mathrm{J}’’=X$ respectively. Hence there arises an interest if
we can apply Gr\"obner bases to solve them.
Gr\"obner bases introduced in [Buchberger 65] are extremely useful tools to decide
problems of polynomial ideals. When a coefficient domain is not a field, however, itge,nerally is not so simple to define or calculate Gr\"obner bases since we can not induce a, reduction from a polynomial straightforwardly. General framework of constructing Gr\"obnerbases of polynomial rings over commutative Noetherian rings with some conditions about
computability
first introduc.ed inand [Zacharias 78]. It, however, is notvery efficient since the reductions are not defined so simple that calculation of Gr\"obnerbases is very
. For more limited coefficient domain,] introduced
Gr\"obner bases forrings over commutative regular rings based on special reductions. The same notion of Gr\"obner bases for Boolean polynomial rings was independently
introduced by us and called Boolean Gr\"obner bases in [Sakai 88], and more detailed study
was given in [Sakai 90].
In this paper, we prove two nice properties of Boolean Gr\"obner bases. One is about theextendability of special solutions presented in Theorem 2.5. When we use an admissible
power products of variables
total order,and,such thatfor each variableand power
Boolean Gr\"obner bases in general have the form {
,
,
$\in$

$\subseteq$$\mathrm{d}$$\mathrm{n}\mathrm{u}\mathrm{a}1$$\}^{r}\vee$$a,$ $b$’$1’$$\mathrm{m}\mathrm{a}111’\vee$$\mathrm{i}\mathrm{t}^{2}\mathrm{e}\mathrm{r}e$$[\mathrm{n}\cdot \mathrm{i}\mathrm{n}\mathrm{k}\mathrm{S}\overline{i}8]$$\mathrm{h}\mathrm{e}\mathrm{a}\backslash \gamma_{\vee}’$$1^{\mathrm{t}\backslash ^{-}}\prime\prime \mathrm{e}\mathrm{i}\prime \mathrm{s}\mathrm{p}\mathrm{f}e\mathrm{n}\mathrm{n}\mathrm{i}\mathrm{n}\mathrm{g}89$$\mathrm{P}^{\mathrm{o}1}\mathrm{y}\mathrm{n}\mathrm{o}\mathrm{n}\mathrm{l}\mathrm{i}\mathrm{a}1$$>\mathrm{o}\mathrm{f}$$-\overline{\mathrm{Y}}=.\mathrm{Y}_{1,-}\mathrm{v}_{\mathit{2}}.,$$z\mathrm{Y}_{n}$$1^{-}/’=\mathrm{I}_{1}’’,$$\ldots$’$Y_{i}>X_{1^{1}}^{\delta}z\mathrm{Y}_{2^{2}}‘ s\ldots\lrcorner \mathrm{Y}_{n}^{S_{l}}$$\mathrm{I}_{2}’’|,$$\mathrm{Y}_{m}$$\ldots$’$\mathrm{J}_{i}’$$\mathrm{p}_{-}\mathrm{r}\mathrm{o}\mathrm{d}\mathrm{u}\mathrm{C}\mathrm{t}\mathrm{x}_{1}^{s_{1}}\lrcorner \mathrm{v}^{s_{2}}2\ldots X^{S,\iota}n$’$g_{1}(d\overline{\mathrm{Y}}, \iota/)\prime g_{2}(\overline{X}, Y)-,,$$\ldots$$g_{l}(\overline{x},\overline{Y}),$$h_{1()}\overline{X}$278$h_{2}‘(\overline{X}),$$\ldots$

equations,$h_{k}(,\overline{\mathrm{Y}})\}$. Theorem 2.5 ensures us that we can extend each solution of theto a solution of the whole equations$\{h_{1}(\lrcorner\overline{\mathrm{Y}})=0, h_{2}‘(\overline{X})=0, \ldots , h_{k}(\overline{X})=0\}$.
The another one presented in Theorem 2.6 shows the existence of paralnetric Boolean
Gr\"obner bases. For a given set of polynomials, we canconstruct a parametric Boolean Gr\"obner base,tha,t isbecomes a Boolean Gr\"obner basis offor ach instantiation for the variables .
These properties play especially important rolls in our application of Boolean Gr\"obnerbases to solve set constraints.
give brief review of Boolean Gr\"obner bases
In section 2, weseveralclassical results of polynomial ideals of Boolean rings, then we show our nuain results
concerning Boolean Gr\"obner bases. In section 3, we describe several
to solve
Boolean Gr\"obner bas es. In section 4, we give. some examples of ourset constraints
fronl our
. We also conlpare ourwith other solvers ofin the last section.
Boolean$\{g_{1}(\overline{X}, 1/)-’=0, g_{2}‘(_{z}\overline{\mathrm{Y}}, 1^{-}/’)=0, \ldots , g_{l}(\overline{x},1^{-}/^{r})=0_{!}h_{1}(_{z}\overline{\mathrm{Y}})=0, h_{2}‘(\overline{X})=0, \ldots , h_{k}(_{z}\overline{\mathrm{Y}})=0\}$$\{f_{1}(z\overline{\mathrm{Y}},]^{-}/’), f‘ 2(d\overline{\mathrm{Y}}, 1/)’\underline{f}-, \ldots.k(d\overline{\mathrm{Y}}, 1/’)-\}$$C\tau(_{z}\overline{\mathrm{Y}})=\{g1(_{z}\overline{\mathrm{Y}}, 1^{\prime’}), g\underline{‘’}(_{-\overline{\mathrm{Y}}}-, 1’’), \ldots , g_{l}(d\overline{\mathrm{v}}.1’’)\}-$$C_{7}(\overline{a})=\{g_{1}(\overline{a}, \mathrm{y}/-)_{!}g_{2(\overline{a}}, 1^{-}/’),:.

$\{f_{1}(\overline{a}, \mathrm{I}^{-}/’), f‘ 2(\overline{a}, 1^{-}/’), \ldots , f_{k}(\overline{a}, 1’)-\}$.

, g_{l}(\overline{a}_{!}l/’)\}-$$d\overline{\mathrm{Y}}$$e$$\overline{a}$$\mathrm{f}\mathrm{i}\mathrm{r}\mathrm{s}\mathrm{t}_{1}$$\mathrm{t}\mathrm{o}\mathrm{g}\mathrm{e}\mathrm{t}|\mathrm{h}e\mathrm{r}\mathrm{W}\mathrm{i}\mathrm{t}_{\mathrm{t}}\mathrm{h}$$1\mathrm{n}\mathrm{e}\mathrm{t}\mathrm{h}_{0}\mathrm{d}_{\mathrm{S}}$$\mathrm{u}\mathrm{s}\mathrm{i}\mathrm{l}$$1\mathrm{n}\mathrm{e}\mathrm{t}\mathrm{h}_{0}\mathrm{d}_{\mathrm{S}}$$1\mathrm{n}\mathrm{e}\mathrm{t}\mathrm{h}_{0}\mathrm{d}_{\mathrm{S}}$$\mathrm{i}\mathrm{m}\mathrm{p}\mathrm{l}\mathrm{e}\mathrm{n}\mathrm{l}\mathrm{e}\mathrm{n}\mathrm{t}\mathrm{a}\mathrm{t}\mathrm{i}_{0}\mathrm{n}$$\mathrm{e}\mathrm{q}\iota \mathrm{l}\mathrm{a}\uparrow|\mathrm{i}\mathrm{o}\mathrm{n}\mathrm{s}$2Boolean Gr\"obner bases

A Boolean ring
idempotent, i.e.

$B$

is a

ring wit, identity such$\mathrm{c}\mathrm{o}\mathrm{m}\mathrm{l}\mathrm{n}\mathrm{u}\mathrm{t}\mathrm{a}\mathrm{t}\mathrm{i}\backslash r\mathrm{e}$$\mathrm{h}$$\mathrm{i}111\mathrm{p}_{0\Gamma \mathrm{t}}\mathrm{a}\mathrm{n}\mathrm{t}$

$B$

is

for all $a\in B$ .

$a^{2}=a$

It has the following

every element of$\mathrm{t}\mathrm{h}\mathrm{a}\mathrm{t}_{\mathrm{y}}$propert,y:$a+a=0$ for all $a\in B$ .

In this section we fix snch a computablering $B$ , and describe our Gr\"obner bases
method to solve polynomial equations over $B$ . Since each element of a Boolean ring is
idenlpotent, a quotient ringis lnore convenient to work on, rather‘, . . .
than a polynomial ring] itself, where is the ideal generated by the setof. This quotient ring is called a Boolean
polynomial ring and denoted by.
also call it, elelnent a Boolean
polyn.omial. The inlportant property of this quotient ring is that it also becolnes a Boolean$\mathrm{B}\mathrm{o}\mathrm{o}\mathrm{l}\mathrm{e}\mathrm{a}\mathrm{l}\mathrm{l}$$B[_{\lrcorner}\mathrm{Y}_{1},d\mathrm{Y}\underline{‘’}, \ldots , z\mathrm{Y}_{n}]/I$$B1^{\mathrm{x}_{1},d}\mathrm{Y}_{2}$$I$$-\mathrm{Y}_{n}$$,$$\mathrm{p}\mathrm{o}\mathrm{l}\mathrm{y}\mathrm{n}\mathrm{o}\mathrm{n}\mathrm{u}\mathrm{i}\mathrm{a}1_{\mathrm{S}}\{X_{1}^{2}’+X_{1}, X_{2}^{\mathit{2}}"+_{d}\mathrm{Y}_{2}‘, , .

.

, d\mathrm{Y}_{n}^{2}+_{d}\mathrm{Y}_{n}\}$$B(X_{1},- \mathrm{Y}_{2}, \ldots , .\mathrm{Y}_{n})$$\iota\iota^{\overline{J}}\prime e$$\mathrm{s}$ring.
A power prodnct. of variables
is a ternu‘, . . . ,for some non,. When every
negative integers
is it is denoted by 1. The set of power)a commutative monoid.
products,urally
express element, of by lowercase, power products by lowerc.ase Greek lettersletters(possibly with
suffix). A power productis called a Boolean power product ifforeach . Note that each equivalent class of the quotient ringis uniquely, whererepresented by a forni. , . , are different Boolean power products.
In this section we regard Boolean
as such representation forms. Using this)representation the Boolean
ring ecomes computable using the rewriting rules$.\mathrm{v}_{1,-}\mathrm{Y}_{2}$$s_{1},$$s_{2},$$z\mathrm{Y}_{n}$$s_{n}$$\ldots$$d\mathrm{v}^{s_{1}}1d\mathrm{Y}^{s}‘ 2\ldots X^{s,}2n\iota$$0$$s_{i}$’$\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{l}$$\mathrm{n}\mathrm{a}\mathrm{t}$

$a,$

$b,$

$c,$

$B$

$1^{f}\backslash ^{-}\prime \mathrm{e}$$\mathrm{l}\mathrm{s}$$\mathrm{s}$$\alpha,$$\ldots$$\beta,$$\wedge f,$$\ldots$$s_{i}\leq 1$$x^{S}\lrcorner \mathrm{Y}^{s_{2}}\cdots x^{\epsilon}1^{1}2nn$$i$$B(d\mathrm{Y}_{1},p\mathrm{Y}_{2}‘, \ldots, \lrcorner \mathrm{Y}_{n})$$\Sigma_{i=1i}^{l}a_{i}\alpha$$\alpha_{1},$$\alpha_{l}$$\mathrm{P}^{\mathrm{o}1}\mathrm{y}\mathrm{n}\mathrm{o}111\mathrm{i}\mathrm{a}\mathrm{l}\mathrm{s}$$\mathrm{p}\mathrm{o}1_{\mathrm{Y}^{r}\mathrm{n}\mathrm{o}}1$$\{-\mathrm{Y}_{1}^{2}‘arrow\lrcorner \mathrm{Y}_{1,-}\mathrm{Y}_{\mathit{2}}^{2}"arrow\lrcorner \mathrm{Y}_{\mathit{2}}‘, , .

.

$1\mathrm{i}\mathrm{a}1$, .\mathrm{Y}_{n}^{2}‘arrow-\mathrm{Y}_{n}\}$$\mathrm{b}$.

Let us first present the following classical result of Boolean polynolnial rings. It enables
deal with selllantic properties of equations concerningus
solutions by halldling
ideals only$\mathrm{t},\mathrm{h}\mathrm{e}\mathrm{i}\mathrm{r}$$\mathrm{t}_{\mathrm{t}}\mathrm{o}$$\mathrm{s}_{arrow}\}^{r}\mathrm{n}\mathrm{t}\mathrm{a}\mathrm{C}\mathrm{t}\mathrm{i}\mathrm{C}\mathrm{a}\mathrm{l}1\}’\vee\cdot$

279

Theorem 2.1
ringgenerated ideal in a Boolean
Let be an finit,of elements of is called a solution of-tuple$f\in I$ .
is valid under if
say a Boolean polynomial
properties.
we
have
the
followingof . Then$I$$e1\mathrm{y}$$n$$\overline{a}=a_{1},$ $a_{2},$$B$$a_{n}$$\ldots$$\backslash 4^{-}\prime e$$I$$h(\lrcorner\overline{\mathrm{Y}})$. Any
for every
for any solution$B(-\mathrm{Y}_{1,.2}\mathrm{Y}‘, \ldots , z\mathrm{Y}_{n})$$\mathrm{p}\mathrm{o}\mathrm{l}\mathrm{y}\mathrm{n}\mathrm{o}\mathrm{m}\mathrm{i}\mathrm{a}\iota$

$I$

if

$J(\overline{a})=0$$h.(\overline{a})=0$$\overline{a}$$I$(1) A finitely generated ideal
element of $B$ in .

$I$

has a solution if and only if there is not any non-zero$I$is valid under
has a solution,.
for each Boolean polynomial(2)$\mathrm{t}’\backslash ^{-}\prime \mathrm{h}\prime \mathrm{e}\mathrm{n}$$I$$h(_{z}\overline{\mathrm{Y}})$$I$

if and only if$h(-\overline{\mathrm{Y}})\in I$,$\square$$h(_{z}\overline{\mathrm{Y}})$

monoid of power products is called $adm.\dot{i}ssible$ if it

theA total ordersatisfies the following properties.

$\mathrm{c}\mathrm{o}\mathrm{m}\mathrm{m}\mathrm{u}\mathrm{t}\mathrm{a}\mathrm{t}_{1}\mathrm{i}\mathrm{b}^{7}\mathrm{e}$$>\mathrm{o}\mathrm{n}$1. If$\alpha>\beta$, then$\alpha_{J}^{\wedge}|>\beta^{\wedge},$}for$\mathrm{a}1^{-}1\mathrm{Y}^{r\wedge},$}$\vee\cdot$

2. $\alpha>1$ , for any power product $a(\neq 1)$ .
Let us fix such a total admissible order . Not the trivial fact that the restriction of
on the set of Boolean power products is also a total order. For a Boolean,, the greatest Boolean power product amongis called the leading$lpp(f)$.(denoted
coefficientisitscalledthe leading coefby),
Boolean power product ofby $res(f)$ . The notation.(denoted by $lc(f)$ ). The rest part, of is also
anddenotes a Boolean polynomial but also indicates
led a rule if $lc(f)reS(f)=res(f)$ .
. A Boolean polynomial is
$>$

$e$

$>$

$\mathrm{P}^{\mathrm{o}1}\mathrm{y}\mathrm{n}\mathrm{o}\mathrm{n}\mathrm{l}\mathrm{i}\mathrm{a}1$$f=\Sigma_{i1}^{l}=\alpha a_{i\mathrm{i}}$$\alpha_{1},$$\ldots$$\alpha_{l}$$f$$ficien\dagger$$\mathrm{d}\mathrm{e}\mathrm{n}\mathrm{o}\mathrm{t}_{}\mathrm{e}\mathrm{d}$$J$$lc(a\alpha\triangleright h)=a,$$a\alpha\triangleright h$$f$$res(\mathit{0}\alpha\triangleright h)=h$

For a rule
It reduces a Boolean$f=a\alpha\triangleright h$,

we define a$lpp(a\alpha\triangleright h)=\alpha$$\mathrm{c}A$on the set of Boolean polynomials.
as follows:
such that$\mathrm{r}\mathrm{e}\mathrm{d}\mathrm{u}\mathrm{c}\mathrm{t}\mathrm{i}_{\mathrm{o}\mathrm{n}}\Rightarrow f$$\mathrm{p}_{\mathrm{o}1_{\mathrm{Y}^{r}\mathrm{n}}\mathrm{i}\mathrm{a}1}.\mathrm{n}\mathrm{o}1b\alpha_{f}^{\wedge}\cdot+g$$ab\neq 0$. $+g\Rightarrow f(1+a)b\alpha\gamma+b_{f’}^{\wedge}h+g$$b\alpha^{\wedge},|$, we sayis reduced to by $F$ (denotedof rules and Boolean polynomials. The transitive reflexive closure and symmetricifforrespectively. For
are denot
finitetransitive reflexive closure$F$ of rules, we canthehas a termination property, i.e. there is noset.
infinit reduction sequence of Boolean polynomials such thatsuch thatto denote one of Boolean polynomials
abuse theare induced because of the following reason. Let, $F$
and is not redtlcible
be an arbitrary set of rules, then for each Boolean polynomial and we have $f+g\in I$ if, whereby $F$ . This property does not generallyis the ideal
and only ifholds unless $F$ is a set of rules.

For a$h,$ $h’$$\mathrm{s}e\mathrm{t}_{1}F$$h\Rightarrow f’ h’)$$h\Rightarrow fh’$

$h’$

$h$

$\mathrm{s}\mathrm{o}\ln ef\cdot\in F$$e\mathrm{d}\mathrm{b}\mathrm{y}\Rightarrow_{F’}^{*}\mathrm{a}\mathrm{n}\mathrm{d}\Leftrightarrow_{F’}^{*}$$\mathrm{o}\mathrm{f}\Rightarrow F$$\mathrm{a}11\backslash ^{r}\vee$$\mathrm{s}\mathrm{h}o\mathrm{w}$$\mathrm{r}e\mathrm{d}\mathrm{u}\mathrm{c}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}\Rightarrow_{F’}$$f_{0}\Rightarrow F’ f_{1}\Rightarrow \mathit{1}^{l}’ f_{\mathit{2}}\cdot\Rightarrow F’\ldots$$e$’$\mathrm{t}^{f}\iota^{-}\prime \mathrm{e}$$\mathrm{n}\mathrm{o}\mathrm{t}|\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}h\downarrow F$

$h’$

$h’$

’

$h\Rightarrow^{*}F’ h’$$\mathrm{b}\mathrm{y}\Rightarrow F’\cdot \mathrm{R}\iota\iota 1\mathrm{e}\mathrm{S}$$f$$f\Leftrightarrow_{\mathit{1}’}^{*}.g$

$I$

$g$

$\mathrm{g}e\mathrm{n}\mathrm{e}\mathrm{r}\mathrm{a}\mathrm{t}_{1}\mathrm{e}\mathrm{d}$efinition 2.1
Let be a finit,ely generated ideal of
the following.
a finit set of rules$\mathrm{D}$$I$$B(X_{1,-}\mathrm{Y}\underline{‘)}, \ldots , -\mathrm{Y}_{n})$$e$$C_{7}$. A Boolean Gr\"obner basis of

$I$

is

$\mathrm{s}\mathrm{a}\mathrm{t}_{\mathrm{t}}\mathrm{i}\mathrm{s}\mathrm{f}\backslash ’\vee \mathrm{i}\mathrm{n}\mathrm{g}$(BG 1)$C_{7}$(BG 2)$g+g’\in I$ if alld only if there is a

generates .

and

$I$

$g’\Rightarrow^{*}Gh$polynomial such that.
. In part,icular, $g\in I$ if and only if$\mathrm{B}\mathrm{o}\mathrm{o}\mathrm{l}\mathrm{e}\mathrm{a}\mathrm{l}\mathrm{l}$$h$$g\Rightarrow_{c}^{*}0$$g\Rightarrow ch*$

280

In
basis.

$\mathrm{a}\mathrm{d}\mathrm{d}\mathrm{i}\mathrm{t}_{\tau}\mathrm{i}\mathrm{o}\mathrm{n}$if it has the following two properties, it is called a normal Boolean Gr\"obner

is not reducible, for any $g’\in C_{7}$ distinct from

(BG 3)Each(BG 4)The leading Boolean power product of each Boolean
distinct, each other.

$g\in C_{7}$$\mathrm{b}\mathrm{y}\Rightarrow_{g}$$\mathrm{p}\mathrm{o}1_{\mathrm{Y}^{\prime \mathrm{n}\mathrm{o}}1}\mathrm{n}\mathrm{i}\mathrm{a}1$$g$.

of $G$ isIn the definition of standard Gr\"obner bases of polynomial rings over fields: the property(BG 4) is not included. It is a direct conclusion from the property (BG 3).
require itt,oin orderhave the following property.
(Normal) Boolean Gr\"obner bases have the following
properties.
$\backslash \prime \mathrm{V}^{-}\mathrm{e}$$(\mathrm{P}2)$$\mathrm{i}\mathrm{l}\mathrm{n}\mathrm{p}_{\mathrm{o}\mathrm{r}}\mathrm{t}\mathrm{a}\mathrm{n}\mathrm{t}$The constraint given by $F,$
is a set of equations $\{f=0|f\cdot\in F\}$ ,is unsatisfiable if and only if the Boolean Gr\"obner bases of (the ideal
generated by) includes a non-zero constant elelnent of $B$ .

$(\mathrm{P}1)$$\mathrm{t}\mathrm{h}\mathrm{a}\mathrm{t}_{\iota}$$F$

For any finitely generated ideal, there
Boolean Gr\"obner basis.

$(\mathrm{P}2)$

The property
canonical

enables us to considerof thegiven by$(\mathrm{P}2)$$\mathrm{s}\mathrm{o}\mathrm{l}\mathrm{u}\mathrm{t}_{1}\mathrm{i}\mathrm{o}\mathrm{n}$$\mathrm{t}_{\mathrm{t}}\mathrm{h}\mathrm{e}$$\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{s}\mathrm{t}\mathrm{r}\mathrm{a}\mathrm{i}\mathrm{n}\mathrm{t}|$$F$.

$\mathrm{u}\mathrm{n}\mathrm{i}\mathrm{q}\iota \mathrm{l}\mathrm{e}\mathrm{l}\mathrm{y}(\mathrm{w}.\mathrm{r}.\mathrm{t}$. $>)$ exists its normal

normal Boolean Gr\"obner basis of $F$ as a

In order to calculate Boolean Gr\"obner bases, we need to define several notations.
.
For a pair of rules and , its critical polynomialis the following Boolean
polynomial:$f$$(\mathrm{d}\mathrm{e}\mathrm{n}\mathrm{o}\mathrm{t}\mathrm{e}\mathrm{d}\mathrm{c}\mathrm{p}(f, g))$$g$.

$lc(g) \frac{lpp(g)}{\mathrm{c}^{1\mathrm{C}\mathrm{D}(p}lp(\mathit{1}),lpp(g))}.f$

where
For a rule$+lc(f.) \frac{lpp(f)}{\mathrm{G}\mathrm{C}^{\mathrm{t}}\mathrm{D}(l\mathrm{P}p(f)lpp(g))}.\cdot,g$denotes the greatest conlmon divisor of $lpp(f)$ and $lpp(g)$ .
its variable critical poly$nom,ial$ is the following Boolean polynonlial:$\mathrm{G}\mathrm{C}\mathrm{D}(lpp(\mathit{1}), lpp(g))$

$f$

,

.

$(1+X)f$

where
is a variable included indenoted by.
$z\mathrm{Y}$$lpp(f\cdot)$. The set of variable crit,ical$\mathrm{P}^{\mathrm{o}1}\mathrm{y}\mathrm{n}\mathrm{o}\mathrm{l}\mathrm{n}\mathrm{i}\mathrm{a}\mathrm{l}\mathrm{S}$

of

$h$,

is

$\mathrm{v}\mathrm{c}\mathrm{p}(h)$Critical polynomials are generally calledin calculation of standard Gr\"obnerbases. Variable critical polynomials are induced since we are working on quotient, rings.
In calculation of a Boolean Gr\"obner basis, a variable critical polynomial $(1+X)f$ plays
the sanle roll as the -polynomial between and.
$\mathrm{S}-\mathrm{P}^{\mathrm{O}}1\mathrm{y}\mathrm{n}\mathrm{o}\mathrm{n}\mathrm{l}\mathrm{i}\mathrm{a}\mathrm{l}\mathrm{s}$$\mathrm{S}$$f$$.\mathrm{Y}^{2}+X$

We can describe Booleall Gr\"obner bases as follows. Hence, we canthem using
these polynomials by a similar completion method of Buchberger’s algorithnl to construct
standard Gr\"obner bases.
$\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{S}\mathrm{t}\mathrm{r}\mathrm{u}\mathrm{C}\mathrm{t}_{\mathrm{t}}$Theorem 2.2
A finite set of rules is a Boolean Gr\"obner basis if and only if every criticaland variable critical polynomial const,ructed by rules of is reduced t,o
$G$

$G$

$\mathrm{p}_{0}1\mathrm{y}\mathrm{n}\mathrm{o}\mathrm{m}\mathrm{i}\mathrm{a}1\square$$0\mathrm{b}\mathrm{y}\Rightarrow^{*}G$.

Throughout the rest of the paper whenever we use Boolean Gr\"obner bases, they are always

281

supposed to be normal. Let us present an importallt classical result before proving several
nice properties of Booleall Gr\"obner bases.
be a,polynomial ring wit, variables
and,(denoted by $I_{B(X)}$ ) fornls also an. For each idofideal of the Boolean polynomial ring,
. Any -tupleof elements of$B$ is called an-solution projection of if there exists an $m$ -tuple,of$B$
elements of such thatis a solution of . Clearly any-solution projection of isa solution of $I_{B(X)}$ . The converse does not generally hold for arbitrary polynomial rings.
But in Boolean polynomial rings it fortunately follows from the following classical result.

Let$1_{1}’\vee,$$B(_{z\overline{\mathrm{Y}}_{!}\overline{Y}})$$\mathrm{B}\mathrm{o}\mathrm{o}\mathrm{l}\mathrm{e}\mathrm{a}\mathrm{l}\mathrm{l}$$z\overline{\mathrm{Y}}=\lrcorner \mathrm{Y}_{1,\lrcorner}\mathrm{Y}_{2},$$\mathrm{h}$$]^{-}/’=$$d\mathrm{Y}_{n}$$\ldots$$e\mathrm{a}1$$1_{m}^{\prime’}$$\mathrm{I}’\underline{‘ J}’,$$\ldots$$I$$B(d\overline{\mathrm{Y}}, 1^{-}/’),$$I\cap B(\lrcorner\overline{\mathrm{Y}})$$n$$B(_{z}\overline{\mathrm{Y}})$$\overline{a}=a_{1_{!}}a_{2},$$\ldots$$I$$(_{z}\overline{\mathrm{Y}})$$a_{n}$$\overline{b}=b_{1},$ $b_{2},$$I$$\overline{b}$$\overline{a},$$\ldots$$b_{m}$$I$$(_{d}\overline{\mathrm{Y}})$

Lemma 2.3
Let be a finitely generated ideal of the Boolean polynomial ring
. Suppose$I_{B(X)}$ has a solution, then each solut,ion can be extended to a whole solution of.
$I$$B(-\overline{\mathrm{Y}}, \mathrm{I}^{-}/)$$I$

give a brief sketch. We
there is only one variable $1’-_{r}=1’’$ . Generalcase. Recall that any finitely generated ideal in a Boolean ring
. follows
is a principal ideal. Hence there is a Boolean polynomial such that $I=(J)$ . Note that
we can express. Then we can show that.
, i.e.
Let be aof. T’hen the equation
has a solution
where is any element of $B$ .
proof:$\mathrm{W}’- \mathrm{e}$$\mathrm{a}\mathrm{s}\mathrm{s}\mathrm{U}\mathrm{l}\mathrm{l}\mathrm{l}\mathrm{e}$$e\mathrm{a}\mathrm{s}\mathrm{i}1\backslash ^{r}$$\mathrm{i}\mathrm{n}\mathrm{d}\mathrm{u}\mathrm{c}\mathrm{t}\mathrm{i}\backslash \prime \mathrm{e}\mathrm{l}\mathrm{y}$$f$$f=1’\prime g(z\overline{\mathrm{Y}})+h(_{x}\overline{\mathrm{Y}})$$I_{B(X)}=((\mathit{9}(d\overline{\mathrm{Y}})+1)h(\overline{X}))$$(g(\overline{a})+1)h(\overline{a})=0$$I_{B(X)}$$\mathrm{S}\mathrm{o}\mathrm{l}\mathrm{u}\mathrm{t}_{(\mathrm{i}\mathrm{n}}\mathrm{O}$$\overline{a}$$c,(g(\overline{a})+1)+h(\overline{a})$$Yg(\overline{a})+h,(\overline{a})=0$$c$$\square$Let us consider the following two problems.
Problem 1. How can we find solution projections ?
Problem 2. How can we extend a given solution projection to a whole solution ?

first consider t,he first problem.
next lemma is a standard technique of Gr\"obner bases to calculate $I_{B(X)}$ which immediately follows from the definition of Boolean Gr\"obner bases.

$\mathrm{t};\mathrm{b}^{\overline{\prime}}\mathrm{e}$$\mathrm{T}^{1}\mathrm{h}\mathrm{e}$Lemma 2.4
Le,$\mathrm{t}>\mathrm{b}\mathrm{e}$$1_{1}’r,$$\}_{2}’’‘,$$\ldots$

uct

an
,

order onset of power products of variables,
such thatfor anyand power prod. Under this order let
be the Boolean Gr\"obner basis of aof. Thenis a Boolean Gr\"obner basis of $I_{B(X)}$ .

$\mathrm{a}\mathrm{d}_{1}\mathrm{n}\mathrm{i}_{\mathrm{S}\mathrm{S}}\mathrm{i}\mathrm{b}\mathrm{l}\mathrm{e}\mathrm{t}\mathrm{O}\mathrm{t}\mathrm{a}\mathrm{l}$$\mathrm{t},\mathrm{h}e$’$1_{m}^{\prime^{=}}$$-\mathrm{Y}_{1,-}\mathrm{Y}_{\mathit{2}}‘,$$.\mathrm{Y}_{n}$$1_{i}’’>X_{1^{1}2}^{\delta}d\mathrm{Y}^{S2}‘’\cdot\cdot-\mathrm{Y}_{n}^{S}n$$\ldots$$,$$C_{7}$$-\mathrm{Y}_{1^{1}\mathit{2}-}S-\mathrm{Y}^{\mathit{8}2},\ldots \mathrm{Y}^{S\iota}?\iota^{\mathrm{v}}$generated ideal$1_{i}’$$\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{t}\mathrm{e}\mathrm{l}\mathrm{y}\coprod$$I$$B(arrow\overline{\mathrm{Y}}, ]^{-}/’)$$G\cap B(\lrcorner\overline{\mathrm{Y}})$

By the above Lemma 2.3-2.4, we can immediately conclude the following property ofBoolean Gr\"obner bases.
Theorem 2.5
Using the same notations as in the above lemmas,
and only if
for every Boolean polynomial$g(\overline{a})=0$$\overline{a}$is an$(.\overline{\mathrm{Y}})$-solution projection of.

$I\mathrm{i}\mathrm{f}\square$$g(\overline{X})\in G\cap B(-\overline{\mathrm{Y}})$This theorenl provides us a nice own property of Boolean Gr\"obner bases in the following
sense. In a general polvnomial ring, after we find a candidat of-solution projectionsof by solving the equations, we have to check if there
exists such thatis a solution of . This check, in general, depends on. But,
in a Boolean polynomial ring, it does not depend. In, Theorem 2.5 guarantees usthat this check is not ven.
$e\overline{a}$$I$$(_{z}\overline{\mathrm{Y}})$$\{g(_{\overline{\mathrm{Y}})},=0|g(-\overline{\mathrm{Y}})\in G\cap B(_{d}\overline{\mathrm{Y}})\}$$I$$\overline{b}$$\overline{b}$$\overline{a},$$e\mathrm{a},\mathrm{c}\mathrm{h}\overline{a}$$\mathrm{f}\mathrm{a}\mathrm{c},\mathrm{t}$$e$$\mathrm{n}\mathrm{e}\mathrm{c}e\mathrm{s}\mathrm{s}\mathrm{a}\mathrm{r}\backslash .r$

282

Let us now consider the second problem. That is we want to find how we can extend
a-solution projection of to a whole solutionof . Since is a solut,ion of
the instantiated idealofalld it is generat by, we can solve it by
its Boolean Gr\"obner basisin. This calculation, however, strongly depends on the values .
Fortunately there is all another approach which allows us extend-solution projections
simultaneously.
$(\overline{X})$$I$$\overline{a}$$I$$\overline{b}$$\overline{a},$$I(\overline{a})=\{p(\overline{a}, 1^{-}/’)|p(_{z}\overline{\mathrm{Y}}, 1’-’)\in I\}$

$G(\overline{a})=\{p(\overline{a}, 1-/)|p(\overline{x},\overline{\mathrm{Y}})\in G\}$$\overline{b}$$B(\overline{\mathrm{Y}})$$e\mathrm{d}$$\mathrm{c}\mathrm{a}1_{\mathrm{C}}\mathrm{u}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{n}\mathrm{g}$$B(1^{-}/)$$\overline{a}$$(\overline{X})$Let be an ideal of a Boolean polynomial ring
. For each -tuple of elementsoflet. Then it is easy to check thatis an ideal of a
Boolean polynomial ring.
Since a Boolean polvnomial ring is also a Boolean ring,can be regarded a.s
Boolean polynomial ringover aring
with variables . In
Booleanring we can also calculate a Boolean Gr\"obner basis of . Let it bedenoted by. For each -tuple of elelnents of $B$ , define$I$$B(d\overline{\mathrm{Y}},1’-’)$$n$$\overline{a}$$I(\overline{a})=\{p(\overline{a}, 1/’)|p(d\overline{\mathrm{Y}}-, 1^{-}/’)\in I\}$

$B_{!}$$I(\overline{a})$$B(1^{-}/)’$$B(-\overline{\mathrm{Y}}, \mathrm{J}^{-}/)$$\mathrm{a}_{1}$$(B(.\overline{\mathrm{Y}}))(\overline{\mathrm{y}}’)$$\mathrm{B}\mathrm{o}\mathrm{o}\mathrm{l}\mathrm{e}\mathrm{a}\mathrm{l}\mathrm{l}$$]^{-}/’$$B(_{z}\overline{\mathrm{Y}})$$I$$\mathrm{p}\mathrm{o}1.\backslash ’\mathrm{n}\mathrm{o}\mathrm{m}\mathrm{i}\mathrm{a}1$$G(_{z\overline{\mathrm{v}})}$$n$$C_{7}(\overline{a}\mathrm{I}=$We call$G(_{z}\overline{\mathrm{Y}})$

$n$

(1)

$G(\overline{a})${$\overline{a}$$g(\overline{a},$$1^{-_{r}}/)|g(_{r}\overline{\mathrm{Y}},$$\overline{a}$$g(\overline{a},$$1^{-}/’)\neq 0$}.
$\mathrm{t}_{\mathrm{t}}\mathrm{h}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{e}111$.

of elelnents of $B$ ,is the Boolean Gr\"obner basis of the ideal

Moreover for each Boolean polynonlial
(2)

and

$1”)-\in C_{7}(-\overline{\mathrm{Y}})$a paramet.ric Boolean Gr\"obner basis because of the following

Theorem 2.6
For each -tuple$\mathrm{t}_{}\mathrm{h}\mathrm{i}\mathrm{s}$$f(d\overline{\mathrm{Y}},$$f.(\overline{a}_{!}1^{-}/’)\downarrow c(a)=(f.(A\overline{\mathrm{Y}}, 1^{-}/\cdot)\downarrow G(X))(\overline{O},\}^{-}/\cdot)$$\iota_{)}^{-}\prime\prime$$I(\overline{a})$of$B(1^{-}/)’$.

we have,.

proof: Note that a substitution
naturally induce a homomorphism fronl
into $B$ . Hence we can easily show the following
and c,orollary. Using them t,oget,her
with Theorenl 2.2, at first (1) follows, then (2) follows immediat$-\overline{\mathrm{Y}}arrow\overline{a}$$B(_{z}\overline{\mathrm{Y}})$$\mathrm{l}\mathrm{e}\mathrm{n}\mathrm{l}\mathrm{n}\mathrm{l}\mathrm{a}\mathrm{s}$$\square$$e1\}^{r}\vee\cdot$

Lemma 2.7
If
then$f\cdot(d\overline{\mathrm{Y}}, 1^{-}/)’\Rightarrow_{g(1)}X,f’(z\overline{\mathrm{Y}}, l-_{r}’)$$f(\overline{a}, ]^{\prime’})=J’-(\overline{a}, 1^{-}/’)$

orCorollary 2.8
If
then

in

$(B(\lrcorner\overline{\mathrm{Y}}))(\mathrm{y}/)-’$$f(_{z}\overline{\mathrm{Y}}, ]^{-}/’)\Rightarrow_{G(x)}f^{;}(_{-}*\overline{\mathrm{Y}}, \}^{-}’)’$$f(\overline{a}, ]^{-}/)\Rightarrow^{*}G(a)f’(\overline{a},\overline{\mathrm{Y}}’)$inin$(B(_{z\overline{\mathrm{v}}}))(1’’)-$$B(\overline{\mathrm{Y}}’)$$\mathrm{n}\mathrm{o}\mathrm{t}_{}$$\mathrm{b}\mathrm{y}\Rightarrow_{G(}x$$f(\overline{a}, 1^{-}/)’$$\square$$\overline{a}$$\square$$(B(d\overline{\mathrm{Y}}))(1’)-$in,$B(\overline{Y})$$\mathrm{a}\mathrm{l}\mathrm{t}\mathrm{e}\mathrm{r}\mathrm{n}\mathrm{a}‘ \mathrm{t}\mathrm{i}\backslash ^{\prime \mathrm{e}}$$\ldots$

for each .

$\overline{a}$By (1) of Theorem 2.6, we can give an
1 alld 2.
In general
has the following form, where,of onlv variables.
$]_{1}’’,]’\prime 2,$$B(1’)-_{\nu}$,$\mathrm{b}\mathrm{y}\Rightarrow c(a)$$C_{7}(\lrcorner\overline{\mathrm{Y}})$infor each .

Lemma 2.9
Ifisreducible) in
thenis not either reducible$f\cdot(\lrcorner\overline{\mathrm{Y}}, 1^{-_{j}}’)$,$f(\overline{a}, ]^{\prime’})\Rightarrow_{g}(a-,\iota)f\cdot;(\overline{a},\overline{\mathrm{P}’}’)$$\alpha_{1},$for each .

$\square$$\overline{a}$method to answer the above problenls$\alpha_{2},$$\ldots$,$\alpha_{k}$are power$\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{d}\mathrm{u}\mathrm{C}\mathrm{t}|\mathrm{S}$consisting$]_{m}’’$$C_{7}(_{-}\overline{\mathrm{Y}})=\{h_{1}(d\overline{\mathrm{Y}})\alpha_{1}\triangleright g_{1}(A\overline{\mathrm{Y}},1^{-}j’), h2(A\overline{\mathrm{v}})\alpha 2\triangleright g2(_{-}\overline{\mathrm{Y}}, 1^{-}/’), \ldots , h_{k}(-\overline{\mathrm{Y}})\alpha k\triangleright g_{k}(\vee\overline{\mathrm{v}},1’’), h(-d\overline{\mathrm{v}})\}$

283

Then we have:

1.

is an

$\overline{a}$$(_{z}\overline{\mathrm{Y}})$-solution projection of$I$

if and only if$h,(\overline{a})=0$.

-solution projection of
can be regarded as a canonical
2. If is anofsolution for the variables of the whole extension of , by the property
as a functional which assigns
Boolean Gr\"obner bases. Hence, we can consider
the )solution for the variables of the whole extension for each-solution
of .
proj
$I,$

$(_{z}\overline{\mathrm{Y}})$$\overline{a}$$G(\overline{a})$$]^{-}/’$$(\mathrm{P}2)$$\overline{a}$$G(_{z}\overline{\mathrm{Y}})$$\overline{\mathrm{Y}}’$$\mathrm{o}\mathrm{n}\mathrm{i}\mathrm{c}\mathrm{a}\mathrm{l}$$(_{d}\overline{\mathrm{Y}})$$\mathrm{c}\mathrm{a}\mathrm{l}$$I$$e\mathrm{c}\mathrm{t},\mathrm{i}\mathrm{o}\mathrm{n}$Note that this approach is better thati the previous one for the problem 2 since it provides us
extensions
parameter . For the problem 1, however, it is not.
complete. NVe have to check if there exists such that$z\overline{\mathrm{Y}}$$\backslash \mathrm{v}\mathrm{i}\mathrm{t}\mathrm{h}$$\mathrm{s}\mathrm{i}\mathrm{m}\mathrm{u}\mathrm{l}\mathrm{t}‘ \mathrm{a}\mathrm{n}\mathrm{e}\mathrm{o}\mathrm{t}\mathrm{l}\mathrm{s}$$h(\overline{a})=0$$\overline{a}$conclude this section, by showing the following type of problems concerning validity
defined in Theorem 2.1 can be solved also using Boolean Gr\"obner bases.

$\mathrm{t}(\backslash ^{-}\prime \mathrm{e}$Problem 3.
Letandbe Boolean polynomials of a Boolean:. Then our problem is depolynomial ring
scribed as follows.
of elelnents of such that the set of equations {11Find all,has a solution and the equation
holds for each solutionof it.
’$f_{1}(d\overline{\mathrm{Y}}, 1^{-}j’),$$f_{l}(-\overline{\mathrm{Y}}, ]^{-}/)$$f\underline{\cdot,}(.\overline{\mathrm{Y}}, 1’-’),$$J(\lrcorner\overline{\mathrm{Y}},\overline{Y})$$\ldots$$B(_{-}\overline{\mathrm{Y}},\overline{Y})=B(X_{1},\lrcorner \mathrm{Y}_{2}‘, \ldots , X_{n}, 1_{1}’’, ]_{2}’’‘, \ldots , 1_{m}^{\prime’})$$B$$n- \mathrm{t},\iota \mathrm{t}\mathrm{p}\mathrm{l}\mathrm{e}\overline{a}$$0,$$\ldots$$(\overline{a}, \iota^{-}/’)=0,$$f_{l}(\overline{a}, 1/’)-=0\}$$f‘ 2(\overline{a},\overline{\mathrm{y}}’)=$$\overline{b}$$J.(\overline{a},\overline{b})=0$

By t,heorem 2.1 it is equivalent to findingbv
is included in
and
.
Let
t,he
Gr\"obner basis of$\overline{a}$such that
idealof $B(1”)-$ generated
does not include non-zero elements of $B$$\mathrm{t}_{\partial}\mathrm{h}\mathrm{e}$$I(\overline{a})$$\{f_{1}(\overline{a}, 1’\vee)-=0, f‘ 2(\overline{a}, 1^{-}j’)=0, \ldots , f_{l}(\overline{a}, 1^{-}/’)=0\}$$f(\overline{a}, l^{-}/)$$I(\overline{a})$beand let$G(_{-}\overline{\mathrm{Y}})=\{h_{1}(arrow\overline{\mathrm{Y}})\alpha_{1}\triangleright g_{1}(_{-}\overline{\mathrm{Y}},]^{-_{j}}’), h_{2}‘(_{z\overline{\mathrm{Y}}})02\triangleright g2(-\overline{\mathrm{Y}}, 1^{-}/)_{:}’\ldots, h_{k}(z\overline{\mathrm{Y}})\alpha k\triangleright g_{k}(-\overline{\mathrm{Y}}, \iota-\prime\prime), h(d\overline{\mathrm{Y}})\}$$\{f_{1}(-\overline{\mathrm{Y}},\iota^{-}/’), f_{2(-}‘\overline{\mathrm{Y}}, 1’-’), \ldots, f_{l}(d\overline{\mathrm{Y}},\overline{Y})\}$$\mathrm{B}\mathrm{o}\mathrm{o}\mathrm{l}\mathrm{e}\mathrm{a}\mathrm{l}\mathrm{l}$$J’.(-\overline{\mathrm{Y}},\overline{Y})=(f(-\overline{\mathrm{Y}},\}^{-}/’)\downarrow_{G()}X)(_{-}\overline{\mathrm{Y}}, \}/’)-$

By

, it

is

.
to finding

such
and
. Let
. be the representation of $f’$ in.
is equivalent to that satisfies the equations. Hence, we can solve by calculating the Boolean Gr\"obner basis of$\mathrm{T}\mathrm{h}\mathrm{e}\mathrm{o}\mathrm{r}\mathrm{e}\ln 2.6$$\mathrm{e}\mathrm{q}\mathrm{u}\mathrm{i}\backslash ^{r}\mathrm{a}\mathrm{l}\mathrm{e}\mathrm{n}\mathrm{t}_{1}$$\mathrm{t}_{}\mathrm{h}\mathrm{a}\mathrm{t}|h(\overline{a})=0$$\overline{a}$$0,$$\ldots$$f’(\overline{O}_{!}Y)\equiv 0$, $p_{k}(\overline{a})=0$$f’(\overline{a}, l^{-}’)\equiv 0$$(B(\lrcorner\overline{\mathrm{Y}}))(]^{-}/’)$$f’(\lrcorner\overline{Y}, 1^{-}’)’=p_{1}(d\overline{\mathrm{Y}})\theta_{1}-,+p_{2}(d\overline{\mathrm{Y}})\rho_{\mathit{2}}+\cdots+p_{k}(.\overline{\mathrm{Y}})’,‘ fk$

Then

in

$(B(-\overline{\mathrm{Y}}))(1’)-$$p_{1}(\overline{a})=0,p_{2}(\overline{O})=$$\overline{a}$$\overline{a}$$\{h(\lrcorner\overline{\mathrm{Y}}),p_{1}(_{z}\overline{\mathrm{Y}}),p2(_{z}\overline{\mathrm{Y}}), \ldots,pk(_{-}\overline{\mathrm{v}})\}$.

Set Constraints

3

we describe how we can apply Boolean Gr\"obner bases to solve set conconstraints, let us first give a language.
. In order to describe

In this$\mathrm{s}\mathrm{e}c\mathrm{t}_{1}\mathrm{i}_{0}\mathrm{n}$$\mathrm{s}\mathrm{t}\mathrm{r}\mathrm{a}\mathrm{i}\mathrm{n}\mathrm{t}|\mathrm{s}$$\mathrm{s}\mathrm{e}\mathrm{t}_{2}$A language of set constraints is a second order lallguage given by the following svmbols.
$a_{!}b,$ $c,$$x,$ $y,$$\emptyset$$\approx,$$\ldots$$\ldots$: first-order constant symbols for$\ldots$nts: first,-order variables for elements: second-order$X_{:}1_{:}^{\prime’}z,$$e1\mathrm{e}\ln e$,$\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{S}\mathrm{t}\mathrm{a}\mathrm{n}\mathrm{t}$symbols for an empty set: second-order variabl es for sets

284$\in,$: predicate symbols for elements and sets$\not\in,\underline{\subseteq}$$\{\cdot\},$$\{\cdot, \cdot\},$: function svnubols for functions fronl elements to sets$\ldots$: function symbols for functions fronl sets to,$\cup^{\sim}$$\cap,$$\{\cdot, \cdot, \cdot\},$($,$$\wedge,$$\neg,$: logical$arrow$$X$$\mathrm{s}\mathrm{e}\mathrm{t}_{\mathrm{b}}\mathrm{s}$denotes the conlplenlent of $X$ )$\mathrm{s}\mathrm{y}\mathrm{n}\mathrm{l}\mathrm{b}_{0}1\mathrm{s}$Let us first note that any constraint given by the above language can be represented as.
the following$\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{l}\mathrm{n}$$\bigvee_{i=1}^{k}H^{i}$

where

,

$H^{i} \equiv\bigwedge_{j^{t}=}^{l}1H_{j}i$

is either an atomic formula or a negation of an atolnic formula.
Each. (set of solutions ofwill concentrate on solving eachof solutions of)given as a union of each
$H_{j}^{i}$’$\mathrm{T}^{\mathrm{t}}\mathrm{h}\mathrm{e}$$\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{l}\mathrm{p}\mathrm{o}\mathrm{n}\mathrm{e}\mathrm{n}\mathrm{t}_{\mathrm{t}}H^{i}$$\mathrm{v}\iota_{\mathrm{e}}^{-}$$\mathrm{V}_{\dot{?}=1}^{k}H^{i}$is$H^{i}.$$\mathrm{s}\mathrm{e}\dot{\mathrm{t}}$Let. us first consider t.he following constraint, $H$ with only atomic forlnulas$H_{j}$.

$H \equiv\bigwedge_{j=1}^{\iota}H_{j}$

,
,
. Let
be sonue secSuppose $H$ includes first order variablestranslateby eliminating
ond order variables which do not appear in H.
into
as follows.
,
using
for some first-order variable , it is translated
has a fornl such a.s $x_{i}\in T$ or
If$\{x_{i}\}\cap
T=\{x_{i}\}$orrespectively. After this translation any
into-order. Note that any ternu such as
variable occurs only in a term such as
can be represented as a union of singletons of first-order variables and a finite set of constant symbols. For exalllple $\{a,x, b, y\}$ is represented as $\{x\}\cup\{y\}\cup\{a, b\}$ .
by , any term is translated into a term with no first-order variables,
each singleton
which does not include any first-order variables.
and we get
By the construction, the following should be clear.
$x_{1},$ $x_{2},$$X_{1},$$x_{p}$$\ldots$$\backslash 1’- \mathrm{e}$$x_{1},$ $x_{2},$$.\mathrm{v}_{1,-}\mathrm{Y}_{2},$$x_{p}$$\ldots$$\ldots$$d\mathrm{Y}_{2}‘,$$\ldots$$H_{j}$$d\mathrm{Y}_{p}$$H_{j}’$$-Y_{p}$$,$$x_{i}\not\in T$$H_{j}$$x_{i}$$\{x_{i}\}\cap T=\emptyset$$\mathrm{f}\mathrm{i}\mathrm{r}\mathrm{s}\mathrm{t}_{\rangle}$$\{\cdots , x_{i}, \cdots\}$$x_{i}$$\{\cdots\}$${\rm Re}_{\text{ノ}}\mathrm{p}\mathrm{l}\mathrm{a}\mathrm{C}\mathrm{i}\mathrm{n}\mathrm{g}$$\{x_{i}\}$$d\mathrm{Y}_{i}$$H_{j}’$$H \Leftrightarrow\exists_{d}\mathrm{Y}_{1\mathit{2}p}\exists_{\lrcorner}\mathrm{Y}‘\cdots\exists d\mathrm{Y}(d\mathrm{Y}_{1}=\{x_{1}\}\bigwedge_{d}\mathrm{Y}_{2}‘=\{x_{\underline{J}}‘\}\wedge\cdots\bigwedge_{d}\mathrm{Y}_{p}=\{x_{p}\}\bigwedge_{j=1}lH_{j};)$Let, $U$ be$\mathrm{t}_{}\mathrm{h}\mathrm{e}$set of all (onstant symbols $a,$$b,$ $c,$$\ldots$. Then the set of all subsets of

$U$

nat-

urally forms a Boolean ring by defining
andset,with an empty set as and a wholeas 1.
for each
Boolean ring by inrest of this section. Note that the atomic forWe denoteare represented by the equations $\{a\}X=\{a\},$ $\{a\}X=0$
lntlla $a\in X,$ $a\not\in X$ andand $XY=X$ respectively. Hence, if a constraint in the fornu of an atonuic fornlula, has
no first-order variables for elements, it can be represented by a polynomial equation of a
, where,are second-order variable,
Booleanring
included in the constraint.
into the form
Therefore we can translatewith some Boolean polynollli],
for solne second-order
in
als
.
and
Now we have the following representation.
$X+Y=(_{d}\mathrm{Y}\mathrm{n}^{\sim}Y)\cup(^{\sim}X\cap Y)$$d\mathrm{Y},$$1’\subseteq U$

$U$

$0$

$B$

$\mathrm{t}_{9}\mathrm{h}\mathrm{i}\mathrm{s}$$X1^{\prime’}=-\mathrm{Y}\cap 1’$$\mathrm{t}_{l}\mathrm{h}\mathrm{e}$$arrow\dot{\mathrm{Y}}\subseteq 1’-$’$\mathrm{p}\mathrm{o}1\}^{r}.\mathrm{n}\mathrm{o}\mathrm{n}\mathrm{l}\mathrm{i}\mathrm{a}1$$B(1_{1,2}’\iota’’‘, \ldots , Y_{n})$$\bigwedge_{j=1}^{l}H_{j}’$$f_{1},$$\ldots$$f_{l}$$1_{n}’$$\}’’]’1,\prime \mathit{2},$$\ldots$$\mathrm{s}$$\bigwedge_{j=1}^{l}f_{j}=0$$B(_{-\mathrm{v}}1,-\mathrm{v}_{2}‘, \ldots, \mathrm{r}\mathrm{Y}\}’\prime 1’p’ 1,2’, \ldots , 1_{n}^{J}’)$$\iota^{r}\mathrm{a}\mathrm{r}\mathrm{i}\mathrm{a}\mathrm{b}\mathrm{l}\mathrm{e}\mathrm{s}$$/\prime 1,1’‘ 2,$$\ldots,$$z\mathrm{Y}_{1,\lrcorner}\mathrm{Y}_{2,.,\prime \mathrm{Y}_{p}}‘..$$H\Leftrightarrow\exists X_{1}\exists d\mathrm{Y}‘ 2\ldots\exists d\mathrm{Y}_{P}$($d\mathrm{Y}_{1}=\{x_{1}\}\wedge.\mathrm{Y}_{2}=\{x_{2}\}\wedge\cdots$A$. \mathrm{Y}_{p}=\{x_{p}\}\bigwedge_{j=1}^{l}f_{j}=0$)’$]_{n}/$

285

Gr\"obner bases.
We will describe two methods to solve this constraint by using Bool,The first one is appropriate when we are interested in the first-order variables,
the second one is appropriat when we are interested in the second-order$e\mathrm{a}\mathrm{n}$$x_{1},$$x_{\mathit{2}}‘,$$\ldots$$x_{P!}$$\backslash ^{r}\mathrm{a}\mathrm{r}\mathrm{i}\mathrm{a}\mathrm{b}\mathrm{l}\mathrm{e}\mathrm{s}1_{1}’’.1’\underline{\prime\prime’},$$e$$1_{n}’’$$\ldots$

Solution method 1
and power
for each
be a total admissible order suc.h that
Letof
. Under this order, calcula.te the Boolean Gr\"obner basis
form.
. In general it has the following$>$$1_{i}^{\prime’}$$l_{i}’’>X_{12^{2}\cdot p}^{s_{1}}x‘ S\ldots \mathrm{Y}^{s_{p}}$$G$$\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{d}\iota \mathrm{l}\mathrm{C},\mathrm{t}d\mathrm{Y}_{1}^{s_{1}}arrow \mathrm{Y}_{2^{2}p^{p}}‘ \mathrm{c}\mathrm{s}\ldots- \mathrm{Y}^{b}\backslash$$\{f_{1}(_{-\overline{\mathrm{Y}}}, ]-/’), \mathit{1}2(A\overline{\mathrm{Y}},\overline{Y}), \ldots , f_{l}(_{z\overline{\mathrm{Y}}}, \overline{Y})\}$$c_{\tau}=\{g_{1}(d\overline{\mathrm{Y}}, 1^{j’}), g_{2}(--\overline{\mathrm{Y}},1/)-’, \ldots, g_{m}(d\overline{\mathrm{Y}},]^{-}/)’, h1(\lrcorner\overline{\mathrm{Y}}), h_{2}(\overline{x}), \ldots, h_{7}.(\overline{x})\}$

solution for the first-order variables
By Theorem 2.5, we can conclude that
, $h,.(\{x\})=$of the constraint $H$ is a solution ofthe equations {, and vice versa.
solve second-order variables , we have to calculate the Boolean Gr\"obner
In order,of thefor each solution.
basis of {
,
,
and
and
denoteabove equations. Where
respectively.

$x_{1},$ $X_{\mathit{2}_{-}}‘,\ldots.x_{P}$$\mathrm{a}111^{r}\vee$$h_{1}(\{\overline{x}\})=0,$ $h2(\{\overline{x}\})=0,$$\ldots$$0\}$$1^{-}/’$$\mathrm{t}_{1}\mathrm{o}$$g_{1}(\{\overline{a}\}, \mathrm{y}^{-}/’),$$.,(-g_{m}\{\overline{a}\},1^{-}’)’\}$$g2(\{\overline{a}\underline{\}}, ]^{-}/)’,$$\overline{a}=a_{1},$$a_{2},$$,$$\{x_{1}\},$ $\{x_{2}\},$$\{a\}$$\{x,\}$

Solution method 2
Boolean Gr\"obner basis
Calculate theIn general it has the following form.
$\mathrm{p}\mathrm{a}\mathrm{r}\mathrm{a}\mathrm{n}\mathrm{l}\mathrm{e}\mathrm{t}\Gamma \mathrm{i}_{\mathrm{C}}$$G(\lrcorner\overline{\mathrm{Y}})$$\ldots$of$\{f_{1}(.\overline{\mathrm{Y}}, \}^{-}J)’,$$\ldots$$\{a_{1}\},$ $\{a_{2}\},$$\{x_{p}\}$$f‘ \mathit{2}(_{x\overline{\mathrm{Y}}},1^{-}/)’,$$\ldots$$a_{p}$$\ldots$,$\{a_{p}\}$$f_{l}(\overline{x}, 1^{-}/)\}$$c(-\overline{\mathrm{Y}})=\{g1(-\overline{\mathrm{Y}}, \iota_{),g}--’\overline{\mathrm{Y}},]/)’, \ldots,(-\overline{\mathrm{Y}}, \mathrm{I}-_{j}\prime 2(\lrcorner g_{m})’, h(-\overline{\mathrm{v}})\}$.
By Theorem 2.6 (1), we can conclude the fol1
$H$
has a solution if and only if $h(\{x\})=0$ has a solution. Furtherlnore, for
The constraint
can be considered as a canonical solution for the second-ordereach solution of it,.
variables$(-)11^{\prime\cdot \mathrm{i}}\underline{\mathrm{n}}\mathrm{g}$$C_{7}(\{\overline{a}\})$$\overline{a}$$1_{1,2}^{j^{r}}1/’‘,$$\mathrm{I}_{n}’’$$\ldots,$

Remark 1
In case there are no first,-order variables in$H_{:}$

these methods are same.

Remark 2.
general, howNote that we can also solve first-order variables by
eve. , it is more complex than solving $\{h_{1}(\{\overline{x}\})=0, h_{2}(\{x\})=0, \ldots , h_{7}.(\{X\})=0\}$ , since.
is the Boolean Gr\"obner basis of
Gr\"obner basis of.
,
Booleanthecalculating
by
can
we
get
think
One might
by the second lnethod. Our experimental data show that calculaafter
is much heavier
Gr\"obner
ring
bas es of the Booleantion of Boolean. The
than calculation of Boolean Gr\"obner bases of the Boolean polynomial ring(,aregenerallyofmuchof Boolean polynomialsreason is that$B$
heavier than calculation of elenuents of .
$\mathrm{s}\mathrm{o}1\backslash ’\mathrm{i}\underline{\mathrm{n}}\mathrm{g}h(\{\overline{X}\})=0$$\mathrm{I}\underline{\mathrm{n}}$$\mathrm{r}$$\{h.(_{-}\overline{\mathrm{Y}})\}$$\{h_{1}.(d\overline{\mathrm{Y}}), h_{2}(\sim\overline{\mathrm{Y}}), \ldots , h_{r}(_{z}\overline{\mathrm{Y}})\}$$h_{1},$ $h_{2}.,$$\mathrm{t}_{\mathfrak{a}}\mathrm{h}\mathrm{a}\mathrm{t}$$\{h\}$$\ldots$$h_{r}$$\mathrm{c}\mathrm{a}\mathrm{l}\mathrm{c}\iota 1\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{n}\mathrm{g}h$’$(B(_{z\overline{\mathrm{Y}}}))(]^{-}/)$$\mathrm{p}\mathrm{o}1_{\mathrm{Y}^{r},\vee}\mathrm{n}\mathrm{o}\mathrm{n}\mathrm{l}\mathrm{i}\mathrm{a}1$$B(_{-}\overline{\mathrm{Y}}, ]/)-’$$\mathrm{e}\mathrm{S}\mathrm{S}e\mathrm{n}\mathrm{t}_{1\mathrm{i}1}\mathrm{a}$$B(d\overline{\mathrm{Y}})$$\mathrm{a}\mathrm{l}\mathrm{c}\mathrm{u}\mathrm{l}\mathrm{a}\mathrm{t}\mathrm{i}_{\mathrm{o}\mathrm{n}}$can be not, only an atonlic
where eachconsider a const,raint.
formula but, also a negation of an,her, it can be represented by anof a
If the inside of the nega.tion iside as an equation $f=0$ as efore, it is repreforlnula. Otherwise representing thefor somesented by $f\neq 0$ . Note that this is equivalent todoesoccur in .
first-order$H \equiv\bigwedge_{j=1}^{l}H_{j}$$\backslash \backslash ^{-}\prime \mathrm{e}\prime \mathrm{n}\mathrm{e}\mathrm{x}\mathrm{t}_{\iota}$$H_{j}$$\mathrm{a}\mathrm{t}_{\mathrm{O}\ln}\mathrm{i}_{\mathrm{C}}\mathrm{f}_{\mathrm{o}\mathrm{r}\mathrm{n}}1\mathrm{u}\mathrm{l}\mathrm{a}$$\mathrm{a}\mathrm{t}_{1\mathrm{o}\mathrm{n}}\mathrm{u}\mathrm{i}\mathrm{c}$$\mathrm{e}\mathrm{i}\mathrm{t}$$\mathrm{f}\mathrm{o}\mathrm{r}\mathrm{n}\mathrm{l}\in \mathrm{o}\mathrm{r}\not\in$$\mathrm{b}$$\mathrm{i}\mathrm{n}.\mathrm{s}$$\exists z\{z\}f=\{z\}(\mathrm{i}.\mathrm{e}.

$\backslash ^{r}\mathrm{a}\mathrm{r}\mathrm{i}\mathrm{a}\mathrm{b}\mathrm{l}\mathrm{e}\approx \mathrm{w}\mathrm{h}\mathrm{i}\mathrm{c}\mathrm{h}$$\mathrm{n}\mathrm{o}\mathrm{t}_{l}$$f$\exists\approx\approx\in f)$

.

.

286

Therefore by adding some new first-order variables we can translat $eH$ into a form without.
$\mathrm{n}\mathrm{e}\mathrm{g}\mathrm{a},\mathrm{t}_{}\mathrm{i}\mathrm{o}\mathrm{n}\mathrm{s}$Remark 3$\ldots.]’n$In the above solutions, if we are not interested in all second-order variables, . . . ,, we can solve the constraint only for these vari} some variables
but
ables using a total adnlissible order such that any power product consisting of onlyis less thall any of other variable .
:$1_{1}’’,$’$\mathrm{o}\mathrm{n}1$$]_{i_{1}}’,]_{\dot{f}}’2$$]_{2}’,$$1_{i_{m}}’$$\vee$’$1_{i_{1}}’’,1_{i_{2}}/,$$\ldots$$1_{k}’$$1_{i_{m}}’$conclude this section with a solution method for a special type of set constraints withquantifiers.
Special type of set constraints
Given Boolean polynomialsof.
Find constant symbols
the set of equations,
has a solution for the second-order variables
and $f(\overline{S}, \{a\})=0$
holds for each solution of it.

$\mathrm{t}\prime 1’’- \mathrm{e}$$f_{1}(z\overline{\mathrm{Y}},\overline{Y}),$$t‘ 2(.\overline{\mathrm{Y}}, 1’)-,$$\ldots,$$f_{l}(z\overline{\mathrm{Y}}!

$\overline{a}\mathrm{s}\iota \mathrm{l}\mathrm{c},\mathrm{h}\mathrm{t}_{\mathrm{t}}\mathrm{h}\mathrm{a}\mathrm{t}$$0,$\mathrm{J}^{-}/)\mathrm{a}\mathrm{n}\mathrm{d}_{-}f(d\overline{\mathrm{v}}, 1’-’)$$B(_{z}\overline{\mathrm{v}-}, 1^{-}/)$$\{f_{1}(.\overline{\mathrm{Y}}, \{a\})=0, f2(\lrcorner\overline{\mathrm{v}},\underline{\{}a\})=$$\mathit{1}\iota(_{z}\overline{\mathrm{Y}}_{!}\{\overline{a}\})=0\}$$d\overline{\mathrm{Y}}$$\ldots$$\overline{S}$It can be solved by the method given at the end of section 2. Using the sa,me notations
there, it is equivalent to finding such that satisfies the equations$\overline{a}$$0,p2(\{\overline{a}\})=0,$$\ldots$!

$pk(\{\overline{a}\})=0$$h(\{\overline{a}\})=0.p_{1}(\{\overline{a}\})=$$\overline{a}$.

Since our domain is not all subsets of but only singleton sets of $B$ , we can not solve it
by simply calculating the Boolean Gr\"obner basis $H$ of.
have to solve the equations in the domain of singleton sets of $B$ . In general it i,seasier to solve
than solving the equations$\ldots,pk(\{X\})=0$ .
$B$$\{h(_{x}\overline{\mathrm{Y}}),p1(d\overline{\mathrm{Y}})!p2(\overline{X}), \ldots , p_{k}(\overline{X})\}$$\mathrm{t}^{f}\iota^{-}\prime \mathrm{e}$$h.(\{\overline{X}\})=0,p_{1}(\{\overline{x,}\})=$$\{q(\{\overline{X,}\})=-0|q(d\overline{\mathrm{Y}})\in H\}$$0,p_{2}(\{\overline{T,}\})=0,$

4

Examplesgive several xamples of our
methods described in section 3.

$\iota\iota_{\mathrm{e}}^{-}\prime\prime$$e$$\mathrm{i}\mathrm{n}\mathrm{l}\mathrm{p}\mathrm{l}\mathrm{e}\mathrm{m}\mathrm{e}\mathrm{n}\mathrm{t}\mathrm{a}\mathrm{t}\mathrm{i}_{0}\mathrm{n}$of set constraint solvers based on the). :’, we input a(Cons,In the following query,
list,
constraint in aof aof equations for Cons, aof second-order variables in which
we are int,erested forand a list of-order variables for AtomVar. The
and V. The symbols
in $\{\}$ represent
constant symbols of elements unless they are incltlded in the list
. Symbols
included in
represent first-order variables.
’$‘?-\mathrm{s}\mathrm{o}\mathrm{l}\mathrm{V}\mathrm{e}_{-^{\mathrm{S}\mathrm{e}}}\mathrm{t}_{-}\mathrm{e}\mathrm{l}\mathrm{e}\mathrm{m}\mathrm{e}\mathrm{n}\mathrm{t}$$\mathrm{f}_{\mathrm{o}\mathrm{r}}111$$\mathrm{S}\mathrm{e}\mathrm{t}\mathrm{V}\mathrm{a}\mathrm{r},\mathrm{A}\mathrm{t}\mathrm{o}\mathrm{m}\mathrm{V}\mathrm{a}\mathrm{r}$$\mathrm{l}\mathrm{i}.\mathrm{s}\mathrm{t}$$\mathrm{S}\mathrm{e}\mathrm{t}\mathrm{V}\mathrm{a}\mathrm{r}$$\mathrm{f}\mathrm{i}\mathrm{r}\mathrm{s}\mathrm{t}_{1}$$.\mathrm{s}\backslash ’\mathrm{m}\mathrm{b}\mathrm{o}1_{\mathrm{S}}\vee/\backslash$$\mathrm{r}\mathrm{e}_{\mathrm{P}^{\mathrm{r}\mathrm{e}\mathrm{s}}}\mathrm{e}\mathrm{n}\mathrm{t}\cap \mathrm{a}\mathrm{n}\mathrm{d}\cup \mathrm{r}\mathrm{e}\mathrm{s}\mathrm{p}\mathrm{e}\mathrm{c}\mathrm{t}\mathrm{i}\backslash r\mathrm{e}1\vee 1^{r}$$\mathrm{a}1_{!}\mathrm{a}2,$$\mathrm{d}\mathrm{i}\mathrm{f}\mathrm{f}\mathrm{e}\mathrm{r}\mathrm{e}\mathrm{n}\mathrm{t}_{1}$$\ldots$$\mathrm{A}\mathrm{t}\mathrm{o}\mathrm{m}\mathrm{v}\mathrm{a}\mathrm{r}$$\mathrm{A}\mathrm{t}\mathrm{o}\mathrm{m}\mathrm{v}\mathrm{a}\mathrm{r}$$?-\mathrm{S}\mathrm{o}1_{\mathrm{V}\mathrm{e}\mathrm{s}}-\mathrm{e}\mathrm{t}-^{\mathrm{e}}1\mathrm{e}\mathrm{m}\mathrm{e}\mathrm{n}\mathrm{t}([$,$\{\mathrm{a}\mathrm{l}, \mathrm{a}9\}/\backslash (\mathrm{X}2\backslash /\sim \mathrm{X}1)=\{\mathrm{a}2, \mathrm{a}5, \mathrm{a}7\}/\backslash \mathrm{S}5$$\mathrm{S}1/\backslash (\mathrm{S}2/\backslash \sim\{\mathrm{a}5\}\backslash /(\mathrm{S}3/\backslash (\mathrm{S}4/\backslash \sim(\mathrm{X}1\backslash /\{\mathrm{a}6\}))))=(\mathrm{S}5/\backslash \mathrm{S}6)\backslash /(\mathrm{S}4/\backslash \mathrm{S}7/\backslash \mathrm{S}2)\backslash /\mathrm{S}8$,,$\mathrm{S}5/\backslash \mathrm{S}4/\backslash \mathrm{S}9/\backslash \mathrm{S}6/\backslash \mathrm{S}2/\backslash (\mathrm{S}\mathrm{l}0\backslash /\mathrm{X}3\backslash /\{\mathrm{a}7\})/\backslash (\{\mathrm{a}9\}\backslash /\mathrm{X}2)=0,\mathrm{S}5/\backslash \mathrm{S}8/\backslash \sim(\mathrm{X}3\backslash /\{\mathrm{a}5, \mathrm{a}8\})=0$$\mathrm{S}2/\backslash (^{\sim}\{\mathrm{a}6, \mathrm{a}8\})=\mathrm{s}4\backslash /\mathrm{S}8,\mathrm{S}2/\backslash (^{\sim}\{\mathrm{a}9\})=\mathrm{s}11\backslash /\mathrm{S}10\backslash /\mathrm{X}2\backslash /\{\mathrm{a}5, \mathrm{a}7\}\backslash /\mathrm{S}7,\mathrm{S}\mathrm{l}1/\backslash \mathrm{S}3=0$$\mathrm{S}10/\backslash \mathrm{S}3=0,\mathrm{s}12=\mathrm{S}9\backslash /\mathrm{S}7,$,$\mathrm{S}9/\backslash \mathrm{S}7/\backslash \mathrm{S}15/\backslash \sim(\mathrm{X}\mathrm{l}\backslash /\mathrm{X}2\backslash /\mathrm{X}3\backslash /\{\mathrm{a}4, \mathrm{a}5, \mathrm{a}6, \mathrm{a}7, \mathrm{a}8, \mathrm{a}9, \mathrm{a}\mathrm{l}\mathrm{o}\})=0$,,$\{\mathrm{a}4\}/\backslash \mathrm{S}6=\{\mathrm{a}4\},\mathrm{x}1/\backslash \mathrm{S}9=\mathrm{X}1,\mathrm{x}3/\backslash \mathrm{S}7=\mathrm{X}3,\mathrm{S}\mathrm{l}\backslash /\mathrm{S}\mathrm{l}0\backslash /\mathrm{X}\mathrm{l}\backslash /\mathrm{X}2=(\mathrm{s}\mathrm{l}2\backslash /\mathrm{S}\mathrm{l}3)/\backslash \{\mathrm{a}4\}\backslash /\mathrm{X}2\backslash /\mathrm{S}\mathrm{l}0$$(\mathrm{S}1\backslash /\mathrm{S}12\backslash /\mathrm{S}2)/\backslash \mathrm{X}1\backslash /\mathrm{X}2\backslash /\mathrm{S}6=(\mathrm{S}10\backslash /\mathrm{S}9)\backslash /(\mathrm{S}7/\backslash \mathrm{X}3)\backslash /\mathrm{S}2$,$(\mathrm{S}5\backslash /\mathrm{S}3\backslash /\{\mathrm{a}4\})/\backslash (\mathrm{S}2\backslash /\mathrm{S}4\backslash /\mathrm{S}3\backslash /\mathrm{S}6)=(\mathrm{S}1\backslash /(\mathrm{X}1\backslash /\mathrm{X}2/\backslash (\mathrm{S}3\backslash /\mathrm{S}10)))/\backslash \mathrm{S}1\backslash /\mathrm{S}14$$]$, [Xl, X2, X3] , $[])$ .

287

contradiction deduced as follows$\{\mathrm{a}9\}=0$

In this query, there is no first-order variables. Hence two methods described in section
3 are salne. Our
calculated the Boolean Gr\"obner basis of the first list to solve
XI,X2 and X3 and detected it includes the constant element. Hence it returned theabove answer.
, in the next query we made a9 a variable inSince we got a contradiction byorder to get some condit,ions to make the constraint satisfiable. The symbol Cl denotes
the equations in the first list of the above query.
$\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{g}\mathrm{r}\mathrm{a}‘ \mathrm{n}\mathrm{l}$$\{\mathrm{a}9\}$$\{\mathrm{a}9\}=0$$?-\mathrm{s}\mathrm{o}\mathrm{l}\mathrm{v}\mathrm{e}-^{\mathrm{S}}\mathrm{e}\mathrm{t}_{-}\mathrm{e}\mathrm{l}\mathrm{e}\mathrm{m}\mathrm{e}\mathrm{n}\mathrm{t}$([C1]. []. [a9]).

constraint is satisfiable when$(^{\sim}\{\mathrm{a}2,\mathrm{a}4\})*\{\mathrm{a}9\}=0$

proceeds the method 1 when we input no second-order variables. Hence,
Our
it returned the answer. We can see that it holds if and only if
a9
a2 or a9.
In the following third and forth queries, we replaced a9 by a2 and a4 resp ctively, that is
C2 (C3) is given from Cl replacing a9 by a2 (a4).
$\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{g}\mathrm{r}\mathrm{a}\ln$$(^{\sim}\{\mathrm{a}2, \mathrm{a}4\})*\{\mathrm{a}9\}=0$$=$$=\mathrm{a}4$$e$-element ([C2] , [Xl, X2, X3]. []).

$?-\mathrm{s}\mathrm{o}\mathrm{l}\mathrm{v}\mathrm{e}_{-\mathrm{S}}\mathrm{e}\mathrm{t}$constraint is always satisfiable
under the above condition$[\mathrm{X}1,\mathrm{x}2,\mathrm{X}3]$

has the following form$\{\mathrm{a}5\}*\mathrm{X}3*\mathrm{x}\mathrm{l}=0$$\{\mathrm{a}5, \mathrm{a}7\}*\mathrm{X}3*\mathrm{x}2=\{\mathrm{a}5,\mathrm{a}7\}*\mathrm{X}3$$\{\mathrm{a}2\}*\mathrm{X}3=0$$\{\mathrm{a}\mathrm{l},\mathrm{a}2\}*\mathrm{X}\mathrm{l}=\{\mathrm{a}1\}$$\{\mathrm{a}\mathrm{l}, \mathrm{a}2\}*\mathrm{X}2=0$$?-\mathrm{s}\mathrm{o}\mathrm{l}\mathrm{V}\mathrm{e}_{-}\mathrm{S}\mathrm{e}\mathrm{t}_{-}\mathrm{e}\mathrm{l}\mathrm{e}\mathrm{m}\mathrm{e}\mathrm{n}\mathrm{t}$([C3] , [Xl, X2, X3]. []).

constraint is always satisfiable
under the above condition$[\mathrm{X}1,\mathrm{x}2,\mathrm{X}3]$

has the following form$\{\mathrm{a}5\}*\mathrm{X}3*\mathrm{x}\mathrm{l}=0$$\{\mathrm{a}2,\mathrm{a}5, \mathrm{a}7\}*\mathrm{x}3*\mathrm{x}2=\{\mathrm{a}2, \mathrm{a}5,\mathrm{a}7\}*\mathrm{X}3$$\{\mathrm{a}4\}*_{\mathrm{X}3}=0$$\{\mathrm{a}\mathrm{l},\mathrm{a}4\}*\mathrm{X}\mathrm{l}=${al,a4}$\{\mathrm{a}\mathrm{l},\mathrm{a}4\}*\mathrm{X}2=0$

In the next query, each list of
the nlethod 2.

$\backslash ^{r}\mathrm{a}\mathrm{r}\mathrm{i}\mathrm{a}\mathrm{b}1e\mathrm{s}$is non-empty. In t,his case, our program proceed288$?-\mathrm{s}\mathrm{o}\mathrm{l}\mathrm{V}\mathrm{e}_{-}\mathrm{S}\mathrm{e}\mathrm{t}_{-}\mathrm{e}\mathrm{l}\mathrm{e}\mathrm{m}\mathrm{e}\mathrm{n}\mathrm{t}$([C1]. [Xl, X2, X3]. [a9]).

constraint is satisfiable when$(^{\sim}\{\mathrm{a}2, \mathrm{a}4\})*\{\mathrm{a}9\}=0$

under the above condition$[\mathrm{X}1,\mathrm{x}2,\mathrm{X}3]$

has the following form$(\{\mathrm{a}5\}*\{\mathrm{a}9\}+\{\mathrm{a}5\})*\mathrm{x}3*\mathrm{x}\mathrm{l}=0$$(\{\mathrm{a}2, \mathrm{a}5, \mathrm{a}7\}*\{\mathrm{a}9\}+\{\mathrm{a}2, \mathrm{a}5, \mathrm{a}7\})*\mathrm{x}3*\mathrm{x}2=(\{\mathrm{a}2,\mathrm{a}5, \mathrm{a}7\}*\{\mathrm{a}9\}+\{\mathrm{a}2, \mathrm{a}5, \mathrm{a}7\})*\mathrm{x}3$$(\{\mathrm{a}2, \mathrm{a}4\}*\{\mathrm{a}9\})*\mathrm{x}3=0$$(\{\mathrm{a}\mathrm{l}, \mathrm{a}2, \mathrm{a}4\}*\{\mathrm{a}9\}+\{\mathrm{a}\mathrm{l}\})*\mathrm{x}\mathrm{l}=\{\mathrm{a}\mathrm{l}, \mathrm{a}4\}*\{\mathrm{a}9\}+\{\mathrm{a}\mathrm{l}\}$$(\{\mathrm{a}\mathrm{l}, \mathrm{a}2, \mathrm{a}4\}*\{\mathrm{a}9\}+\{\mathrm{a}\mathrm{l}\})*\mathrm{x}2=0$

is a general form of the above two solutions, i.e. when
Note that the solution of
a2 (a9) it is sanue as the solution of the third(fort,h) query.
a9$\mathrm{X}\mathrm{l},\mathrm{x}2,\mathrm{x}3$$=\mathrm{a}4$$=$$\iota\iota^{-}\prime \mathrm{e}$next show an example of the solvers discuss$e\mathrm{d}$at the end of section 3.

)
we input a list of equations forIn the following)
as before. Our
returns its
Cons and a list of first-order variables for
Gr\"obner
ba.sis into the output variable .
Boolean(Eq, ).::, we input an equation for Eq and a
In the qtlerv
conditions ofBoolean Gr\"obner basis given by the above query. Our progranlfirst-order variables such that Eq becomes valid under the constraints given by .
$\mathrm{q}\mathrm{u}\mathrm{e}\mathrm{r}.\backslash ^{r}‘?-\mathrm{g}\mathrm{e}\mathrm{t}_{-}\mathrm{g}\mathrm{b}$(Cons, AtomVar,”$\mathrm{G}\mathrm{B}$

$.$

$!$

$\mathrm{A}\mathrm{t}\mathrm{o}\mathrm{m}\mathrm{V}\mathrm{a}\mathrm{r}$$\mathrm{u}$$\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{g}\mathrm{r}\mathrm{a}\mathrm{l}$$\mathrm{G}\mathrm{B}$$\mathrm{G}\mathrm{B}$$‘?-\mathrm{m}\mathrm{a}\mathrm{k}\mathrm{e}_{-}\mathrm{v}\mathrm{a}\mathrm{l}\mathrm{i}\mathrm{d}_{-}\mathrm{u}\mathrm{n}\mathrm{d}\mathrm{e}\mathrm{r}_{-}\mathrm{g}\mathrm{b}$$\mathrm{r}\mathrm{e}\mathrm{t}_{\mathrm{b}}\mathrm{u}\Gamma \mathrm{n}\mathrm{s}$$\mathrm{G}\mathrm{B}$

Using the salne$?-\mathrm{g}\mathrm{e}\mathrm{t}_{-\mathrm{g}}\mathrm{b}$$\mathrm{l}\mathrm{i}.\mathrm{s}\mathrm{t}_{l}$of equations [C1] as above,, let us execute the following query.

([C1]. [a9] ,$\mathrm{G}\mathrm{B}$).

Our program returned a Boolean Gr\"obner basis into the variable . Fortion,
can ask conditions to lllake it valid, using this Boolean Gr\"obner basis.
Let us execute the following query.
$\mathrm{G}\mathrm{B}$$\backslash \mathfrak{i}\mathrm{e}$.

$?-\mathrm{m}\mathrm{a}\mathrm{k}\mathrm{e}_{-^{\mathrm{v}\mathrm{a}}}1\mathrm{i}\mathrm{d}-^{\mathrm{u}\mathrm{n}}\mathrm{d}\mathrm{e}\mathrm{r}-\mathrm{g}\mathrm{b}(\{\mathrm{a}9\}/\backslash (\mathrm{S}1\backslash /\mathrm{S}2)=0,\mathrm{G}\mathrm{B})$equation is valid when$(^{\sim}\{\mathrm{a}2\})*\{\mathrm{a}9\}=0$

It lneans$\{\mathrm{a}9\}/\backslash (\mathrm{S}1\backslash /\mathrm{S}2)=0$$(^{\sim}\{\mathrm{a}2\})*\{\mathrm{a}9\}=0$$1!\mathrm{b}^{-}\prime \mathrm{e}$, i.e.

a9

is valid under the const,raints if and onlv if$=\mathrm{a}2$.

can also ask other questions using the salne$\mathrm{G}\mathrm{B}$.

$?-\mathrm{m}\mathrm{a}\mathrm{k}\mathrm{e}_{-}\mathrm{v}\mathrm{a}\mathrm{l}\mathrm{i}\mathrm{d}-^{\mathrm{u}}\mathrm{n}\mathrm{d}\mathrm{e}\mathrm{r}_{-\mathrm{g}\mathrm{a}9\}}\mathrm{b}(\{/\backslash (\mathrm{S}\mathrm{l}\mathrm{l}\backslash /\mathrm{S}\mathrm{l}2)=\{\mathrm{a}9\},\mathrm{G}\mathrm{B})$equation is valid when$(^{\sim}\{\mathrm{a}4\})*\{\mathrm{a}9\}=0$.

$\mathrm{a}\mathrm{r}\mathrm{b}\mathrm{i}\mathrm{t},\mathrm{r}\mathrm{a}\mathrm{r}\mathrm{y}$

equa-

289

It means$\{\mathrm{a}9\}/\backslash (\mathrm{S}\mathrm{l}\mathrm{l}\backslash /\mathrm{S}\mathrm{l}2)=\{\mathrm{a}9\}$i.e. a9$(^{\sim}\{\mathrm{a}4\})*\{\mathrm{a}9\}=0.$’5$=\mathrm{a}4$is$\backslash ^{r}\mathrm{a}\mathrm{l}\mathrm{i}\mathrm{d}$under the constraints if and$\mathrm{o}\mathrm{n}\mathrm{l}\mathrm{v}\vee$if.

Conclusion

Our research of this paper was originally motivated by a desire to install a set constraint,
solver in CAL that is a constraint logic programming language we have developed in. In colistraint logic, we have to keep a constraint in a
ICOT
of its canonical representation. The following two properties are indispensable forthis representation.
$([\mathrm{A}\mathrm{i}\mathrm{b}\mathrm{a}88])$$\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{g}\mathrm{r}\mathrm{a}\mathrm{n}\mathrm{l}\mathrm{n}\mathrm{l}\mathrm{i}\mathrm{n}\mathrm{g}$$\mathrm{f}\mathrm{o}\mathrm{r}\ln$

1. Canonical repres ntation is unique, that is if twoaredefined as they have same solutions),
canonical representation forms are identical.
$e$$\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{S}\mathrm{t}\Pi \mathrm{r}\mathrm{a}\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}$$\mathrm{e}\mathrm{q}\mathrm{u}\mathrm{i}\backslash ^{r}\mathrm{a}\mathrm{l}\mathrm{e}\mathrm{n}\mathrm{t}(\mathrm{u}\mathrm{S}\mathrm{u}\mathrm{a}\mathrm{l}\mathrm{l}\mathrm{y}$$\mathrm{t}_{6}\mathrm{h}\mathrm{e}\mathrm{i}\mathrm{r}$2. We can easily checkform.

$\mathrm{s}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{s}\mathrm{f}\mathrm{i}\mathrm{a}\mathrm{b}\mathrm{i}\mathrm{l}\mathrm{i}\mathrm{t}\backslash ^{r}\vee$of a constraint using its canonical representation

In general, simple callonical representation is preferable in order to get simple solutions.
It is also preferred
we can handle nlore problenls relating to a constraint besides
checking only satisfiability.
In our set constraint solver: we did not want to use any parameter to represent a canonical form in order to make solutions easy to read. Moreover, in order to manage many
problems relating to a constra, , we wanted to make its canonicalhave powers
to decide problenls concerning validity.
$\mathrm{t}\mathrm{h}\mathrm{a}\mathrm{t}_{\mathrm{t}}$$\mathrm{i}\mathrm{n}\mathrm{t}_{c}$$\mathrm{s}\mathrm{o}\mathrm{l}\mathrm{u}\mathrm{t}_{1}\mathrm{i}\mathrm{o}\mathrm{n}$Boolean Gr\"obner bases enable us to have such canonical solution forms. In fact, they
have the following further nice property.
Boolean Gr\"obner bases provide lnanv types of canonical solution forms according
to the employed admissible total orders of power products.
Admissible total orders of powerheavily
the shap es of Gr\"obner ba.ses.
When we use an admissible total order
power products of variables,,
andsuch thatfor each variableand power, Gr\"obner bases generally have the following form:
product$\mathrm{a}\mathrm{f}\mathrm{f}\mathrm{e}\mathrm{t}^{\backslash }.\mathrm{t}$$\mathrm{P}^{\mathrm{r}\mathrm{o}\mathrm{d}\mathrm{u}}\mathrm{c}\mathrm{t}|\mathrm{s}$$>\mathrm{o}\mathrm{f}$$\lrcorner\overline{\mathrm{Y}}=d\mathrm{Y}_{1,\wedge}\mathrm{Y}\underline{‘’},$$d\mathrm{Y}_{\tau\iota}$$\ldots$$]^{-}/’=1_{1}^{\prime^{r}},\mathrm{I}_{\mathit{2}}^{j^{\vee}}.,$$l_{m}^{\prime’}$$\ldots$$\mathrm{J}_{i}’’>-\mathrm{Y}_{1}^{s_{1}}\mathrm{s}\mathrm{Y}^{\delta}‘ \mathit{2}\ldots\lrcorner \mathrm{Y}_{n}^{s_{n}}2$$1_{i}^{\prime’}$$\lrcorner \mathrm{Y}_{1-}^{\epsilon_{1}}\mathrm{v}^{s}‘ \mathit{2}\ldots-\mathrm{Y}^{S}n2n$$\{g_{1}(_{-}\overline{\mathrm{Y}}, \iota/)-’, g_{\underline{J}}‘(-\overline{\mathrm{Y}},\overline{\iota’}’), \ldots, gl(d\overline{\mathrm{Y}},\overline{Y}), h_{1}.(d\overline{\mathrm{Y}}), h_{2}(A\overline{\mathrm{v}}), \ldots, h_{k}(d\overline{\mathrm{Y}})\}$

Hence, if we want to solve equations

priorit,y for the variable over the other varit,han , such orders are suit.able. E,specially,, that is we are lnore interested in.
if we want to solve equations with aorder of variabl es for priority, a purely lexicographic order is suitable.
On the other hand, if we do not want to give priority to any variable, a tot,al degree order(or a total degree reverse lexicographic order to get
influence) is suitable.
Gr\"obner .ses generally have simple
In our Boolean polynomial rings ofi.e. easy to read) forms when we use a tota,1 degree order. In the first exalnple of our..
programs in section 4, the power products of the variables inare compared by atotal degree order to get simple answers.
$-\overline{\mathrm{Y}}$$1\mathrm{h}^{J}\mathrm{i}\mathrm{t}l\mathrm{h}$$\mathrm{a}\mathrm{b}\mathrm{l}\mathrm{e}\mathrm{s}\}^{-}\prime\prime$$\overline{\mathrm{Y}}$$1^{-}/’$$\mathrm{s}\mathrm{t}_{1}\mathrm{r}\mathrm{i}\mathrm{c}\mathrm{t}$$\mathrm{C}\mathrm{o}\mathrm{m}_{\mathrm{P}^{1\mathrm{e}}}e\mathrm{t}_{}$$\mathrm{s}e\mathrm{t}\mathrm{s},$$\mathrm{B}\mathrm{o}\mathrm{o}\mathrm{l}\mathrm{e}\mathrm{a}\mathrm{l}\mathrm{l}$$\mathrm{b}\mathrm{a}$$($$\mathrm{S}\mathrm{e}\mathrm{t}\mathrm{V}\mathrm{a}\mathrm{r}$Of course there are many other nlet,hods to solve Boolean equations. As far as we know,t,hey aredivided into twoof methods. One is based on Boole’s classical$\mathrm{e}\mathrm{S}\mathrm{S}\mathrm{e}\mathrm{n}\mathrm{t}_{1\mathrm{i}1}\mathrm{a}$$\mathrm{t}_{_{\vee}}\}^{r}\mathrm{P}^{\mathrm{e}}\mathrm{s}$290

on L\"owenheim’s fornlula. In order t,o compare our lnethod with them, let us see how the answer of the third example of the section
4 looks like when we solve it by the above two classical methods.

varia,ble elimina,tion

method: a,nother is bas$e\mathrm{d}$If we use Boole’s classical variable elimination method, we c.all have a canonical solution
andas follows.
with parameters$\mathrm{f}\mathrm{o}\mathrm{r}\ln$$L_{1}^{7}’,$$C^{\tau}‘ 2$$L_{\mathit{3}}^{7}.’,\cdot$$-\mathrm{Y}_{1}=(^{\sim}\{a_{1}, a_{2}\})*L^{l}\tau_{1}+\mathrm{t}a_{1}\}$$d\mathrm{Y}_{2}=(^{\sim}\{\mathit{0}_{1},a2\})*L^{\tau_{2}}’$‘.

$d\mathrm{Y}_{t}.\cdot=\{a_{5}\}*L_{1}^{r}’*c_{2}^{\tau_{9}}’*L_{3}^{7}\prime\prime.+\{a_{5}, a\}\overline{\prime}*c_{2}^{7}‘*L_{s}’’\cdot+(^{\sim}\{a_{2}, a5, a_{7}\})*L_{s}^{7}’$It is possible to eliminate parameters
get the following canonical solution.
though we can not simply use it to decide problems concerning$\mathrm{t}_{\mathrm{t}}\mathrm{o}$$\mathrm{f}\mathrm{o}\mathrm{r}\iota \mathrm{n}$,al-$\backslash ’\mathrm{a},1\mathrm{i}\mathrm{d}\mathrm{i}\mathrm{t}_{1\backslash ,\vee}’$$\{a_{1}\}\leq\lrcorner \mathrm{Y}_{1}\leq^{\sim}\{a_{2}\}$$0\leq X_{2}\leq\sim\{a1, a2\}$$0\leq-\mathrm{Y}_{3}.\cdot\leq\{a_{5}\}*-\mathrm{Y}_{1}*d\mathrm{Y}_{2}‘+\{a_{5},a_{7}\}*d\mathrm{Y}_{2}‘+^{\sim}\{a_{2}, a_{5,7}a\}$. By Boole’s met,hod,
Neither of then seem to look sinlpler than the solution of our )each set of equations is solved with a strict order of variables for priority, that is variables
isby using the solutions ofandare solved st by st . In the exalnple,, hence the solution does not look so simple for.
$1\mathrm{e}\mathrm{t}\mathrm{h}_{\mathrm{o}\mathrm{d}}$$1$‘$-\mathrm{Y}_{\delta}$$e\mathrm{p}$$e\mathrm{p}$$X_{1}$$\mathrm{s}\mathrm{o}1\backslash ^{r}\mathrm{e}\mathrm{d}$$z\mathrm{Y}_{S}.$$z\mathrm{Y}_{2}‘$$\mathrm{L}_{\ddot{\mathrm{O}}\mathrm{W}\mathrm{e}\mathrm{n}}\mathrm{h}e\mathrm{i}\mathrm{l}\mathrm{n}’ \mathrm{s}$forlnula, constructs a general solution form of given equat,ions using as many

paranleters as the variables included in the equations from a special inst,ance of solutionof thenu. (It does not, offer a unique canonical soltltion form since a general solution fornu
possiblestrongly depends on an instance of solution we c,hoose. In general, isto get a canonical solution form without paranieters by simply eliminating its parameand . asters.) By this fornlula, we can get a general solution withas anof solutions.
usedfollows.
$\mathrm{i}\mathrm{t}_{1}$$\mathrm{n}\mathrm{o}\mathrm{t}\Upsilon \mathrm{e}\mathrm{i}\mathrm{t}\mathrm{D}\mathrm{h}\mathrm{e}\mathrm{r}$$\mathrm{p}\mathrm{a}\mathrm{r}\mathrm{a}111\mathrm{e}\mathrm{t}_{1}\mathrm{e}\mathrm{r}\mathrm{s}c_{1}^{r}’,$$\backslash ’\iota^{-}\prime \mathrm{e}$$d\mathrm{Y}_{1}=\{a_{1}\},X_{2},=0_{A},\mathrm{Y}_{\mathit{3}}.\cdot=0$$c_{2}^{\tau}’$‘$L_{\delta}^{r}’$$\mathrm{i}\mathrm{n}\mathrm{s}\mathrm{t}|\mathrm{a}\mathrm{n}\mathrm{C}\mathrm{e}$$-\mathrm{Y}_{1}=\{a_{7}\}*L_{\delta}^{f}’\cdot*\mathrm{L}_{\mathit{2}}^{\tau}’‘*L_{1}^{\tau}’+\{a_{5}, a_{7}\}*L_{\delta}^{\tau}’\cdot*L_{1}’\tau\sim+\{a1_{!}a_{2}\}*L_{1}^{r}’+\{a_{1}\}$$d\mathrm{Y}_{2}‘=\{a_{5}\}*L_{t}^{r}’.\cdot*L_{2}^{\tau}’*L_{1}’\tau+\{\sim a1,O_{2}\}*U_{2}^{\tau}$.

$X_{\mathrm{J}}.‘=\{a_{1}, a_{5}\}*C_{l}^{\tau}.\cdot*L_{2}^{\tau}’*L_{1}^{\tau}’+\{a_{5}, a\cdot,\}*C_{3}’*U_{2}‘+\{a_{1}\}*L_{\delta}^{r}’\cdot*L_{1}’’+\sim\{a_{1}, a2, a_{5}, a_{7}\}*D_{s}^{7}$

This, again, does not seem to look simpler than the solution of our method.

describe our solvers for constraints among first-order variables such as thedidof the exanlpl es of section 4, since solving these equaequation
tions belong to discret conlbinatorial problelns and very few mathemat,ical (Boolean)
to be embedded.

$\backslash \eta^{-}\prime \mathrm{e}$$\mathrm{n}\mathrm{o}\mathrm{t}_{\mathrm{t}}$$(^{\sim}\{\mathrm{a}2, \mathrm{a}4\})*\{\mathrm{a}9\}=0$$e$$\mathrm{s}\mathrm{t}_{\eta}\mathrm{r}11\mathrm{c}\mathrm{t}_{J}\mathrm{U}\mathrm{r}\mathrm{e}\mathrm{s}\mathrm{S}\mathrm{e}\mathrm{e}\ln$

References[Aiba 88] Akira Aiba, Ko Sakai, Yosuke Sato, David J.Hawley, Ryuzo Hasegawa (1988).
Constraint Logic Programnling Language CAL Proceedings of The
Conference on Fifth Generation Computer, 263276$\mathrm{I}\mathrm{n}\mathrm{t}_{1\mathrm{e}}\mathrm{r}\mathrm{n}\mathrm{a}\mathrm{t},\mathrm{i}_{0}\mathrm{n}\mathrm{a}1$zunl Auffinden der Basisele[Buchberger 65] Buchberger, B. (1965). Ein
mente des Restklassenrings nach einem nulldimensionalen Polynomideal. PhD thesis,
Innsbruck.
$\mathrm{A}\mathrm{l}\mathrm{g}\mathrm{o}\mathrm{r}\mathrm{i}\mathrm{t}\mathrm{h}_{\ln}\mathrm{t}\mathrm{l}\mathrm{s}$$\mathrm{U}\mathrm{n}\mathrm{i}\backslash ^{r}\mathrm{e}\mathrm{r}\mathrm{S}\mathrm{i}\mathrm{t}\ddot{\mathrm{a}}\mathrm{t}$291[Buchberger 85] Buchberger, B. (1985). Gr\"obner bases: An algorithmic method in polynomial ideal theory, chap 6 in Recent Trends in Multidimentional System Theory, N.
K. Bose Ed., Reidel Publ. Comp.
[Martin 79]
U.. Nipkow, T’. (1990). Boolean
Unification, ed. C.Kirchner: Academic$\mathrm{h}/\mathrm{I}\mathrm{a}\mathrm{r}\mathrm{t}\mathrm{i}\mathrm{n}_{\}$$\mathrm{U}\mathrm{n}\mathrm{i}\mathrm{f}\mathrm{i}_{\mathrm{C}\mathrm{a}\mathrm{t}}|\mathrm{i}\mathrm{o}\mathrm{n}$$\mathrm{P}\mathrm{r}e\mathrm{s}\mathrm{S}_{!}437455$-

The Story So Far.

.

[Robbiano 85] Robbiano, L. (1985). Term orderings on the polynomial ring, EUROCAL’85, Springer LNCS V’ol 204,513517.

[Rudeanu 74] Rudeanu, S. (1974). Boolean Functions and E,quations, North-Holland[Sakai 88] Sakai, K., Sato, Y. (1988). Boolean Gr\"obner bases. Proceeding of LASymposium in wint,er, RIMS, Kyoto Univ.: 2940
[Sakai 90] Sa,kai, K., Sato, Y., Menju, S. (1990). Boolean Gr\"obner bases(revised). ICOT
for publication.
Technical Report 613, also$\mathrm{s}\mathrm{u}\mathrm{b}\mathrm{m}\mathrm{i}\mathrm{t}_{}\mathrm{t}e\mathrm{d}$B.Buchbergers Verfahren, Systeme algebraischer Gle78] T’rinks, W. (1978).
ichungen zu l\"osen. J.Nulnber Theory 10, 475488.
$i^{-}\mathrm{b}\mathrm{e}\mathrm{r}$$1^{\mathrm{T}^{\backslash }\mathrm{i}\mathrm{n}}\mathrm{k}\mathrm{s}$[V. (1989). Gr\"obner bases in polynomial rings over commu,. Davenport Ed., Springer LNCS
tative regular rings, EUROCAL ’87,
336347.

$\backslash ’\iota\prime\prime \mathrm{i}- \mathrm{f}\mathrm{e}\mathrm{n}\mathrm{n}\mathrm{i}\mathrm{e}\mathrm{s}_{\mathrm{P}\mathrm{g}}\mathrm{n}1\backslash 4^{-}\prime \mathrm{e}\prime \mathrm{i}_{\mathrm{S}}\mathrm{p}\mathrm{f}\mathrm{e}\mathrm{n}\mathrm{n}\mathrm{i}\mathrm{n}\mathrm{g}$,$\backslash /’ 013\tau 8$$\mathrm{J}.\mathrm{H}$[Zacharias 78] Zacharias, G. (1978). Generalized Gr\"obner bases in. Sci.
mial rings. Thesis at M.I.T., Dept.
$\mathrm{c}_{011}^{\mathrm{t}}1\mathrm{P}$$\mathrm{c}\mathrm{o}\mathrm{m}\mathrm{n}\mathrm{l}\mathrm{U}\mathrm{t}\mathrm{a}\mathrm{t}\mathrm{i}\backslash ^{\gamma}\mathrm{e}$polyno-