Click here
to see it in KOI-7.
Logic Seminar of POMI. 24 February 1997
Speakers: B. Konev (graduate student, POMI)
Title:
"Construction of example for lower bound and sharpening of upper bound
of terms height in the most general unifier in terms of differences of
variables depth."
ABSTRACT
An example proving the exponential nature of dependence of terms height in
the most general unifier on number of variables having non-zero differences of
depth will be constructed.
The following upper bound of height of terms in the most general unifier
was known:
$h \leq n \delta \rho ^n + h_0$, where $n$ -- is a number of variables,
$\delta$ -- is the greatest difference of depth of variablesm, $\rho$ --
the greatest number of occurences of variables in the original terms, $h_0$ --
the heifth of original terms. The following will be proved
$h \leq n \delta 2^{n+1} + h_0$.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Logical Seminar of POMI. 3 March 1997
Speakers: M.A.Vsemirnov (graduate student, POMI)
Title: "Bijective polynomial mappings from N^k onto N"
ABSTRACT
It is known that among quadratic polynomials in two variables
with rational coefficients only two Cantor polunomials
bijectively map N^2 onto N. The original proof,
which is due to Fueter and Polya, is not elementary and,
in particular, requires some results on transcendental numbers.
An elementary proof of the Fueter-Polya theorem will be presented.
An attempt to extend this technique to higher dimensions leads
to some interesting number-theoretical problems. These problems
will be also discussed.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Logical Seminar of POMI. 16 June 1997
Speakers: Olivier Teytaud
Title: "Decidability of the halting problem for Matiyasevich
deterministic machines"
ABSTRACT
\documentstyle[fullpage,12pt]{article}
\usepackage{french}
\title{
Decidability of the halting problem for Matiyasevich
deterministic machines}
\author{Olivier Teytaud}
\date{}
\begin{document}
\maketitle
Problems raised by genetics have been expressed as decidability
questions about the mono{\"\i}d of traces. Professor Yuri
Matiyasevich has transformed these problems into a halting problem
for apparently very weak machines. The decidability or undecidability
of the general non deterministic case hasn't been proved yet;
however we prove the following deterministic case is decidable:
with $k$ a constant, the operators on the integer register are
$X \leftarrow X + 1$, $X \leftarrow X - 1$, $X \leftarrow k \times
X$, $X \leftarrow \lfloor X / k \rfloor $, with a congruence test
modulo $k$ and an equality test; in fact, we show that there is
an effective computation that transforms such a machine into a finite
automaton.
\end{document}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Logical Seminar of POMI. 2 July 1997
Speakers: Regimantas Pliuskevicius (Lithuania)
Title: "Saturation method for a first order linear
temporal logic"
ABSTRACT
The report presents a reasoning system - saturation method - for
a restricted first order linear temporal logic with "next" and
"always". The most attractive property of saturation method consists
in that it allows to built derivations uniformly both for a finitary
complete and finitary incomplete first order linear temporal logic.
Logical Seminar of POMI. 29 September 1997
Speakers: G.I. Goremikina (Balashovo)
Title: "Intuitionistic proofs of classical algebraic theorems"
ABSTRACT
It was found out a class of formulas in the order-rings language
such that their deducibility in the classical set theory implies the
intuitionistic set theory deducibility of the same formulas. The
intuitionistic set theory has the usual properties of effectiveness.
It was found out a translation of a formula from some wide class
such that if it can be classically deduced then the translation can be
intuitionistically deduced (without any additional negations).
It was found out the intuitionistic (in the sense of some
semantics) proofs of variants of some well-known classical algebraic
theorems as for example the properties of splitting fields, Hilbert and
Ritt Nullstellensatz, Weierstrass theorem on roots.
Logical Seminar of POMI. 6 October 1997
Speakers: A.V.Chagrov (Tver State University)
Title: "ALGORITHMIC PROBLEMS IN MODAL LOGIC"
ABSTRACT
The aim of the talk is to discuss the current situation in algorithmic
problems in modal logic with the presentation of speaker's results in this
subjects.
Decidability of logics and calculi (i.e. finitely axiomatizable logics)
is the starting-point of all investigations here. Problems of modeling
computations by means of modal logics are considered. Creation of simple
(with minimal number of used variables, comfortable for applications, etc.)
undecidable calculi is a direction of the solving of the problems.
Representation of computations by derivations in calculus gives only
one - syntactical - variant of algorithmic consideration of "logical
sequence". Another is semantical one. For example, what can be said about
the decidability of the semantical consequence problem on the finite models
(the old folklore question).
`How can we recognize, given axioms and inference rules of a calculus,
whether the calculus has such-and-such property (consistency, decidability,
etc.)?' A question of this kind arises whenever we deal with a new logic
system. For large families of logics, this question may be considered as an
algorithmic problem.
Various (positive, negative) facts from these directions will be given
in the talk. A part of speaker's results in Russian maybe found in
[A.V.Chagrov. Undecidable properties of superintuitionistic logics.
In: S.V.Jablonskij, editor, Mathematical Problems of Cybernetics, volume 5,
pages 67--108. Physmatlit, Moscow, 1994.].
Logical Seminar of POMI. 3 November 1997
Speakers: Tatiana L. Sidon (Moscow University)
Title: "Dinamic logic of proofs."
ABSTRACT
The idea of provability interpretation of the modality belongs to Godel.
In 1993 he introduced a modal system S4 as describing properties of the
general notion of provability. Unfortunately S4 failed to be correct with
respect to straightforward arithmetical interpretation of the modality by
Godel provability formula. R.Solovay in 1976 proved that propositional
modal logic arithmetically complete under this interpretation coinside
with Godel-Lob system GL. However GL is incompatible with Godel's system
S4. This fact can be explained as follows: properties of provability are
destorted at the stage of arithmetical encoding.
The solution for the problem of finding an absolute provability logic was
suggested by S.N.Artemov in 1995. He suggested to consider bynary operator
"t is a proof of F" instead of the modality "F is provable" where t is the
exact term representing the proof. It is constructed from proof variables
with the help of elementary operations on proofs that realize modus ponens
rule, proof checking and nondeterministic choice. The dinamic logic of
proofs LP represented by S.N.Artemov is complete with respect to the
intended proof semantics, namely it axiomatizes the set of all formulas
provable in PA (true in the standard model) under every arithmetical
interpretation. LP is sufficient to realize any operation on proofs
admitting propositional description. It is also proved that Godel
provability logic S4 is term-forgetting projection of LP.
The main results of the speaker are the following:
1. Natural axiomatization for provability logic with operations on proofs
is presented. The obtained system MLP includes both Solovay's provability
logic GL and Artemov's dinamic logic of proofs LP. The presence of the
modal operator in the language of MLP makes it possible to introduce two
new elementary operations on proofs that complete the basis of LP to the
basis of the new "joint" logic.
2. MLP is proved to be complete with respect to the intended arithmetical
semantics.
3. MLP is supplied with the appropriate notion of Kripke-style model and
the corresponding completeness theorem is proved.
4. MLP also suffices to realize all operations on proofs admitting
description in the modal propositional language. This fact justifies the
choice of basic operations.
Logical Seminar of POMI. 17 November 1997
Speakers: V.Durnev (Yaroslavl University)
Title: "STUDYING SOME ALGORITHMIC PROBLEMS FOR FREE SEMI-GROUPS
AND GROUPS."
ABSTRACT
\input amstex
\define\al{\alpha}
\define\ph{\varphi}
\define\om{\omega}
\define\De{\Delta}
\define\la{\lambda}
\define\si{\sigma}
\define\cl{\operatorname{cl}}
\define\sbs{\subset}
\define\La{\Lambda}
\define\ind{\operatorname{ind}}
\define\rlh{\rightleftharpoons}
\documentstyle{amsppt}
\NoRunningHeads
\catcode`\@=3D11
\def\nologo{\def\logo@{}}
\catcode`\@=3D13
\nologo
\parindent0.7cm
\TagsOnRight
\pageheight{20cm}
\pagewidth{13cm}
\pageno1
\document
\head
STUDYING SOME ALGORITHMIC PROBLEMS\\ FOR FREE SEMI-GROUPS AND GROUPS
\endhead
\centerline {V.Durnev}
\head
Unsolvability of positive $\forall\exists^3$-theory of a free semi-group
\endhead
Denote as $\Pi_m$ {\it free semi-group of rank $m$ with free generators}
$a_1,\ldots,a_m$.
As far back as 1946 W.Quine have proved unsolvability
of elementary theory of semi-group $\Pi_m$ for $m \ge 2$.
In 1973 the
author have proved unsolvability of
positive
$\exists \forall \exists^3$-theory of a free semi-group
$\Pi_m$ for $m \ge 2$.
S.S.Marchenkov in 1982 have proved unsolvability of positive
$\forall \exists^4$-theory of a free semi-group $\Pi_m.$
This fact improves our result
from the standpoint of a number of the quantor blocks in the
considered formulae, but the general number of the used quantors
is the same.
We obtained further intensification of thise results
as from the standpoint of the number of the quantor blocks as from the
standpoint of the general number of the quantors in the prefix.
\proclaim{Theorem} For $m \ge 2$ positive $\forall\exists^3$-theory
of free semi-group $\Pi_m$ is algorithmically unsolvable.
\endproclaim
Note that according to G.S.Makanin's theorem the universal and
existential theories of semi-group $\Pi_m$ are algorithmically solvable.
\head
Problem of solvability of equations with the right-hand part in free
semi-groups and groups
\endhead
We will consider the following problem in arbitrary semi-group $\Pi$:
"{\it To define by an equation of the form}
$$
w\,(\,x_1,\,\ldots,\,x_n)\, =3D\, g, \tag$*$
$$
{\it where $w\,(\,x_1,\,\ldots,\,x_n)$ is a word in the alphabet of
unknowns}
$$
\{x_1,\ldots\;\ldots,x_t,\ldots\},
$$
{\it and $g$ is an element of semi-group $\Pi$, whether it has a
solution}".
Equations of $(*)$ form were studied in a number of papers and were called:
{\it the equations with the right-hand part} or {\it the equations solved
with respect to unknowns.}
If $\Pi$ is free semi-group of $\Pi_2$ with free generators $a_1, a_2,$
then we consider the number
$$
L =3D | w(x_1,\ldots,x_n)| + |g(a_1,a_2)|, \text { where } |A| - \text { is=
a
length of word } A
$$
as {\it dimension of the solvability problem for equations of $(*)$ form}.
\proclaim{Theorem}
The solvability problem for equations of $(*)$ form in free semi-group
$\Pi_2$ is $NP$-complete.
\endproclaim
Equation of $(*)$ form in the case when semi-group $\Pi$ is a group
is called as {\it the equation with one coefficient.}
The solvability question for equation of $(*)$ form in a free group was
considered of R.Lyndon and P.Schupp and was called
{\it the substitution problem for free groups}.
\proclaim{Theorem}
The solvability problem for equations in free group $F_m$
is linearly reduced to
the solvability problem for the equations with one coefficient in group
$F_{m+1}$, and the solvability problem for systems of equations in group
$F_m$ is polynomially reduced to the solvability problem for the equations
with one coefficient in group \;$F_{m+1}.$
\endproclaim
\proclaim{Theorem}
The solvability problem for the equations with one coefficient in free
group
$F_2$ is $NP$-difficult.
\endproclaim
\head
Equations in words and generalized lengths in free semi-groups
\endhead
Denote as $M(n)$ a set of all non-ordered couples $\{i,j\}\ \
(i, j =3D 1,\,\ldots,n)$ for arbitrary natural number $n$.
If $X$ is a word of semi-group $\Pi_m$ then we denote as $|X|$ a length of
word $X$, and we denote as $|X|_i$ a number of entries of letter $a_i$
into word $X$.
\proclaim{Theorem}
We can indicate such number $n$, such subset $B$ of set $M(n)$ and such
one-parametric class of the equations
$$
w\,(\,x,\,x_1,\,\ldots,\,x_n,\,a_1,\,a_2)\, =3D\,
v\,(\,x,\,x_1,\,\ldots,\,x_n,\,a_1,\,a_2\,)
$$
with unknowns $x_1,\ldots,x_n$, constants $a_1,a_2$ and parameter $x$, that
there does not exist any algorithm that allows for arbitrary natural number
$k$ to define whether the equation
$$
w\,(\,a_1^k,\,x_1,\,\ldots,\,x_n,\,a_1,\,a_2\,) \,=3D\,
v\,(\,a_1^k,\,x_1,\,\ldots,\,x_n,\,a_1,\,a_2\,)
$$
has such solution $\langle X_1,\ldots,X_n\rangle$ in free semi-group
$\Pi_m\;(m \ge 2),$ that for $\{i, j\} \in B: |X_i|_1 =3D |X_j|_1$ and
$|X_i|_2 =3D |X_j|_2.$
\endproclaim
\proclaim{Theorem}
We can indicate such number $n$, such subset $B$ of set $M(n)$ and such
one-parametric class of the equations
$$
w\,(\,x,\,x_1,\,\ldots,\,x_n,\,a_1,\,a_2\,)\, =3D\,
v\,(\,x,\,x_1,\,\ldots,\,x_n,\,a_1,\,a_2\,)
$$
with unknowns $x_1,\ldots,x_n$, constants $a_1,a_2$ and parameter
$x$, that there does not exist any algorithm that allows for arbitrary
natural
number $k$ to define whether the equation
$$
w\,(\,a_1^k,\,x_1,\,\ldots,\,x_n,\,a_1,\,a_2\,) \,=3D\,
v\,(\,a_1^k,\,x_1,\,\ldots,\,x_n,\,a_1,\,a_2\,)
$$
has such solution $\langle X_1,\ldots,X_n\rangle$ in free semi-group
$\Pi_m\;
(m \ge 2)$ that for $\{i, j\}\in B: |X_i| =3D |X_j|$ =A8 $|X_i|_2 =3D |X_j|=
_2$.
\endproclaim
\newpage
\head
Some algorithmic problems for Diophantine sets in $\Pi_2$
\endhead
\proclaim{Theorem}
There exists an algorithm that allows by any representation of Diophantine
set $S$, i.e. by the corresponding couple of words $\langle u,v\rangle,$
and
by any natural number $k$ to define whether set $S$ contains not less than
$k$ elements, or set $S$ contains not more than $k$ elements, or set $S$
contains exactly $k$ elements.
\endproclaim
\proclaim{Theorem} For any fixed $k$ there does not exist any algorithm
that
allows by arbitrary representation of $\langle u,v\rangle$ of Diophantine
set
$S$ to define whether the complement of $S$ consists of $k$ elements
(consists of not less than $k$ elements if $k > 0$, or consists of not more
than $k$ elements).
\endproclaim
\head
Equations in free groups with subgroup restrictions on the solutions
\endhead
\proclaim{Theorem}
For any free group $F_m$ with free generators $a_1,\ldots,a_m$ $(m \ge 2)$
we can construct such equation
$$
w\,(\,x,\,x_1,\,\ldots,\,x_n,\,a_1,\,a_2\,)\, =3D\, 1
$$
with unknowns $x_1,\ldots,x_n$, constants $a_1, a_2$ and parameter $x$ that
there does not exist any algorithm that allows for arbitrary natural number
$k$ to define whether there exists a solution of the equation
$$
w\,(\,a_1^k,\,x_1,\,\ldots,\,x_n,\,a_1,\,a_2)\, =3D\, 1
$$
with the condition
$$
x_1 \,\in \,[F_m, F_m],\;\ldots, \;x_t\, \in\, [F_m, F_m],
$$
where $[F_m, F_m]$ is a commutant of group $F_m$, $t$ is a certain fixed
number between $1$ and $n$.
\endproclaim
We denote as $\ph_i$ its following endomorphism:
$$
\ph_i(a_j) \rlh a_j \;\text { for } j \ne i, \quad \ph_i(a_i) \rlh 1.
\tag$*$
$$
By analogy with the braid groups
endomorphism $\ph_i$ can be called {\it endomorphism of plucking the
$i$ generator}, then, naturally, we will call $\operatorname{Ker}\ph_i$ as
{\it subgroup of $i$-pure elements}, and
$$
P_m \rlh \bigcap_{i=3D1}^m
\operatorname{Ker}\ph_i
$$
as {\it subgroup of pure or smooth elements}.
It is
clear that $P_m \trianglelefteq F_m,\; P_m \subseteq F^{(1)}_n$ and
$P_2 =3D F^{(1)}_2$,
but for $m \ge 3\; P_m \ne F^{(1)}_m$.
Subgroups $P_m$ are dual to commutants $F^{(1)}_n$ of groups
$F_m$ in the following
sense: we determine endomorphisms $\psi_i$ by following equalities $(**)$
dual to equalities $(*)$:
$$
\psi_i(a_j) \rlh 1 \;\text{ for } j \ne i,\quad \psi_i(a_i) \rlh a_i;
\tag$**$
$$
then
$$
F^{(1)}_m =3D \bigcap_{i =3D 1}^m\operatorname{Ker}\psi_i.
$$
\proclaim{Theorem} For $m \ge 3$ there does not exist any algorithm that
allows
by arbitrary equation in group $F_m$
$$
w\,(\,x_1,\,\ldots,\,x_n,\,a_1,\,\ldots,\,a_m\,)\, =3D\, 1
$$
to define whether it has such solution $x_1,\ldots,x_n$ that $x_1 \in P_m$.
\endproclaim
\proclaim{Theorem}
For any $s \ge 2$ there does not exist any algorithm that allows by
arbitrary
equation
$$
w\,(\,x_1,\,\ldots,\,x_n,\,a_1,\,a_2\,)\, =3D\, 1
$$
in group $F_2$ to define whether it has such solution $g_1,\ldots,g_n$ that
$g_1 \in F_2^{(s)}.$
\endproclaim
\proclaim{Theorem}
We can indicate such $r$ that there does not exist any algorithm that
allows
by arbitrary equation
$$
w(x_1,\ldots,x_n,a_1,\ldots,a_r) =3D 1
$$
in free group $F_r$ to define whether it has such solution $g_1,\ldots,
g_n$ that $g_1 \in (F_r)_2$.
\endproclaim
Let $N$ be the $s$ commutant $F_m^{(s)}$ of free group $F_m$ or be the $s$
term $(F_m)_s$ of its lower central series or be
the subgroup $P_m.$
\proclaim{Theorem}
There exists an algorithm that allows by any equation with one unknown
$$
w\,(\,x_1,\,a_1,\,\ldots,\,a_m)\, =3D\, 1
$$
in group $F_m$ to define whether it has such solution $x_1$ that $x_1 \in
N$.
\endproclaim
\head
Equations with automorphisms and endomorphisms in free groups
\endhead
\proclaim{Theorem} We can indicate automorphism $\psi$, endomorphism
$\varphi$
of free group $F_2$ and a set of the equations
$$
w\,(\,x,
\,x_1,\,\ldots,\,x_n,\,{\psi}(x_n),\,{\varphi}(x_1),\,\ldots,\,{\varphi}(x_=
t
),\,a,\,b\,)\, =3D\, 1
$$
with unknowns $x_1,\ldots,x_n$, constants $a,b$ and parameter $x$ such that
there does not exist any algorithm that allows for arbitrary natural number
$k$ to define whether the equation
$$
w\,(\,a^k,\,x_1,\,\ldots,\,x_n,\,{\psi}(x_n),\,{\varphi}(x_1),\,\ldots,\,{\=
v
arphi}(x_t),\,a,\,b\,)\, =3D \,1
$$
has a solution in free group $F_2$.
\endproclaim
Let $F_3$ be a free group with generators $a,b,c$, and $\varphi_1,
\varphi_2$ be its
endomorphisms determined by the following equalities:
$$
\ph_2(b) \rlh \ph_1(a) \rlh 1,\; \ph_2(a) \rlh a,\; \ph_1(b) \rlh b,\;
\ph_1(c) \rlh \ph_2(c) \rlh c.
$$
\proclaim{Theorem} There does not exist any al\-go\-rithm that al\-lows for
ar\-bit\-ra\-ry equ\-ation
$$
w\,(\,x_1,\,\ldots,\,x_n,\, a,\, b,\, c\,)\, =3D\, 1
$$
in group $F_3$ to define
whether it has such solution $x_1,\ldots,x_n$ that $\ph_1(x_1) =3D 1$ and
$\ph_2(x_1) =3D 1.$
\endproclaim
If we denote as $H$ intersection of kernels of endomorphisms $\ph_1$ and
$\ph_2$ we obtain the following direct corollary of the theorem.
\proclaim{Corollary }
There does not exist any algorithm that allows for arbitrary equation
$$
w\,(\,x_1,\,\ldots,\,x_n,\, a,\, b,\, c\,)\, =3D\, 1
$$
in group $F_3$ to define whether it has such solution $x_1,\ldots,x_n$ that
$x_1 \in H$.
\endproclaim
\enddocument
To make this abstract TeXable, please change \=varphi to =\varphi
Vladik
Also, =3D should be replaced by =
Logical Seminar of POMI. 12 January 1998
Speakers: E.A.Hirsch (POMI)
Title: "Randomized algorithms for the propositional satisfiability
problem."
ABSTRACT
Proofs of all known upper bounds for the propositional satisfiability problem
are based on deterministic algorithms that use splitting. In the talk
upper bounds will be presented that base on the use of new algorithms
that do not use splitting and use random source.
The talk will consist of two (independent) parts,
the first part contains the results from the recent paper
[Paturi,Pudlak,Zane "Satisfiability Coding Lemma", FOCS97],
the second part contains the results of the presentator.
Part I. New upper bound for k-SAT.
We proce that a satisfying assignment for a formula in k-CNF
can be encoded by values of less than (1-1/k)N variables.
This coding can be founs in randomized time of the order 2^{(1-1/k)N}
and in deterministic time that teends to 2^{(1-1/(2k))N} for large k.
In the first part of the talk these two algorithms will be presented.
Also Satisfiability Coding Lemma will be presented, a tool
which these two algorithm use. Satisfiability Coding Lemma
is also useful for proving certain lower bounds.
Part II. Upper bound for a local search algorithm.
We mean that local search algorithm is an algorithm
that goes from an assignment to its neighbour that satisfies
more variables than the first assignment, etc.
During the last years there was a comprehensive experimental research
for SAT algorithms. In particular, local search algorithms
demonstrate very good performance for random formulas and
other problem classes. However, (almost) no theoretical results
(worst-case upper bounds) were published.
In this part of the talk upper bound c^N will be proved
for a simple version of local search algorithm
for a natural class of formulas, namely
for formulas in k-CNF such that each variable
occurs in a formula at most s times.
Here c<2 is a concrete number depending on k and s only.
Logical Seminar of POMI. 26 January 1998
Speakers: E.Dantsin (POMI)
Title: "Logic Programs with Sets and Multisets (based on joint papers
with A.Voronkov)"
ABSTRACT
Logic programming deals with tree-like data represented by terms.
Applications (particularly to databases) require handling other kinds
of data, for example finite sets or multisets. An extension of logic
programming to sets and multisets is considered in the talk.
The procedural semantics of the extension is provided by unification
extended to sets and multisets. An extended unification algorithm
is presented as a nondeterministic algorithm that solves equality
constranits. The unification algorithm runs in nondeterministic
polynomial time, and the unifiability problem for sets and multisets
is shown to be NP-complete. This result is used to characterize the
computational complexity of nonrecursive logic programs with sets and
multisets. Namely, the query answering problem for such programs is
shown to be NEXP-complete.
Logical Seminar of POMI. 9 February 1998
Speakers: S.I.Kublanovsky
ABSTRACT
We study a number of natural algorithmic problems related to finite
0 - simple semigroups. Surprisingly enough ,some of them turn out to be
undecidable. For example ,it is undecidable whether a given finite direct
product of finite 0-simple semigroups. On the other hand, we exhibit
algorithms to decide if a given finite semigroup divides a finite 0 - simple
semigroup or a finite direct product of finite 0 - simple semigroups.
Logical Seminar of POMI. 27 April 1998
Speakers: E. Dantsin, M. Gavrilovich, E. Hirsch,
B. Konev (POMI)
Title: "APPROXIMATION ALGORITHMS FOR MAX-SAT: A BETTER PERFORMANCE
RATIO AT THE COST OF A LONGER RUNNING TIME."
ABSTRACT
During the past decade many results concerning approximation algorithms
for the maximum satisfiability problem (MAX-SAT) and for its
subproblems (MAX-3-SAT and MAX-2-SAT) were obtained
(an $\alpha$-approximation algorithm for MAX-SAT is an algorithm that
outputs an assignment satisfying at least a fraction $\alpha$ of the maximal
number of satisfied clauses).
For example, there exists a $7/8$-approximation polynomial-time algorithm for
MAX-3-SAT (Karloff and Zwick, 1997).
On the other hand many negative results were obtained, for example,
Hastad (1997) proved that the existence of a polynomial-time
$(7/8+\epsilon)$-approximation polynomial-time algorithm for MAX-3-SAT
would imply $P=NP$.
We describe an algorithm that approximates MAX-SAT with performance ratio
arbitrarily close to 1. Namely, we show how to construct an
$(\alpha+\epsilon)$-approximation algorithm from a (known) polynomial-time
$\alpha$-approximation algorithm.
In particular, for MAX-3-SAT we can construct a $(7/8+\epsilon)$-approximation
in the time $c^{\epsilon K}$, where $K$ is the number of clauses
in the input formula, $c$ is a constant.
As a byproduct we obtain some upper bounds for the exact MAX-SAT.
Logical Seminar of POMI. 1 June 1998
Speaker: Edward A. Hirsch, (POMI)
Title: "Hard Formulas for SAT Local Search Algorithms."
ABSTRACT
In 1992 B.~Selman, H.~Levesque and D.~Mitchell proposed GSAT,
a greedy local search algorithm for the Boolean satisfiability problem.
Good performance of this algorithm and its modifications has been
demonstrated by many experimental results.
In 1993 I.~P.~Gent and T.~Walsh proposed CSAT,
a version of GSAT that almost does not use greediness.
It has been recently proved that CSAT
can find a satisfying assignment for a restricted class of formulas
in the time $c^n$, where $c<2$ is a constant.
In the talk I shall prove a lower bound of the order $2^n$ for GSAT and CSAT.
Namely, formulas $F_n$ of $n$ variables will be constructed,
such that GSAT or CSAT finds a satisfying assignment for $F_n$
only if this assignment or one of its $n$ neighbours is chosen
as the initial assignment for the search.
Logical Seminar of POMI. 8 June 1998
Speakers: G. Davydov, I. Davydova
Title: "DIVIDING FORMULAS AND POLYNOMIAL CLASSES FOR SATISFIABILITY."
ABSTRACT
Measure q(F) is defined for formula F in CNF in such way that
condition q(F) < 1 is equivalent to satisfiability of formula F.
Consistency graph of formula F is defined for calculation q(F).
The set of its vertices coincides with the set of all non--contradictory
clauses and two vertices are linked with an edge if corresponding
clauses are non--contradictory.
Polynomial classes for satisfiability are described in
consistency graph terms:
1. If the number of connection components is equal to the clauses number n
(in this case we say about dividing formula)
then the measure is calculated in a time O(n^2).
2. If chromatic number of the graph is not more than fixed k
then the measure is calculated in a time O(n^k).
3. If consistency graph is divided into connection components and
for every component the quantity of variables, which have occurences more
than in one clause of this component, is not more than c log(n)
then the measure is calculated in a time O(n^{c+2}).
Logical Seminar of POMI. 15 June 1998
Speaker: N. N. Nepejvoda
Title: "Some notes on NF-style category of all categories."
Logical Seminar of POMI. 14 September 1998
Speakers: A.Tiskin (Oxford University)
Title: "Bulk-synchronous parallel computation."
ABSTRACT
Bulk-synchronous parallel computation (BSP) is a new
model of parallel computation. Its distinguishing features
are simplicity and practicality. The BSP model requires a fresh
look at some classical numerical and combinatorial problems:
sorting, shortest paths computation in a graph, linear algebra,
Boolean matrix multiplication. The obtained algorithms are
often simpler than in other parallel models, and sometimes
lead to surprising theory results.
The talk is based on the author's PhD thesis. It will include
a brief introduction to BSP, and examples of BSP algorithms.
Logical Seminar of POMI. 21 September 1998
Speakers: Dmitri Davydok (ddv@writeme.com)
Title:
ABSTRACT
1. It is known that the problem of determining feasibility of a system of
linear inequalities with integer coefficients, variables taking values in {0,1}
and no more than 3 variables per inequality and the problem of determining
feasibility of a system of linear inequalities with integer coefficients,
integer variables and no more than 2 non-zero coefficients per inequality are
NP-complete. A polynomial algorithm is proposed for determining feasibility of
a system of strict and/or non-strict linear inequalities with rational
coefficients, variables taking a fixed arbitrary finite set of values and no
more than 2 variables per inequality.
2. NP-completeness of the problem of feasibility of a system of strict and/or
non-strict linear inequalities with rational coefficients and integer and/or
rational variables is established.
Logical Seminar of POMI. 5 October 1998
Speakers: Dan E. Willard (State University of New York at Albany)
Title: " Self Verifying Axiom Systems"
ABSTRACT
We will describe some weak axiom systems that are capable of
verifying their own consistency and verifying all the $\Pi_1 $ theorems
of Peano Arithmetic. Some of our axiom systems recognize neither Addition
nor Multiplication as total functions, they thus view them as relations
when they recognize the $\Pi_1 $ theorems of Peano Arithmetic. Other
can recognize Addition as a total function, and in this case they can verify
only their cut-free consistency.
Logical Seminar of POMI. 16 November 1998
Speakers: Boris Konev
Title: "Upper bounds on heights of terms in the most general unifier."
ABSTRACT
We prove an upper bound on the heights of terms occurring in a most general
unifier of a system of pairs of terms in case when unknowns are divided to two
types. An unknown belongs to the first type if all occurrences of this
unknown have the same depth, we call such unknown an unknown of the cut type.
Unknowns of the second type (unknowns of not the cut type) are unknowns that
have arbitrary occurrences. We bound from above the heights of terms occurring
in a most general unifier in terms of the number of unknowns of not the cut
type and other parameters of the system. This bound yields an upper bound on
the heights of terms in proofs with cuts in the Gentzen-style sequent
calculus.