Solving Q SAT in bounded space and time by geometrical computation

Description

Niveau: Supérieur, Doctorat, Bac+8
Solving Q-SAT in bounded space and time by geometrical computation Denys Duchier, Jérôme Durand-Lose, Maxime Senot LIFO, University of Orleans, BP 6759, F-45067 ORLEANS Cedex 2, FRANCE. Abstract. Abstract geometrical computation can solve PSPACE-com- plete problems efficiently: any quantified boolean formula, instance of Q- SAT – the problem of satisfiability of quantified boolean formula – can be decided in bounded space and time with simple geometrical construc- tions involving only drawing parallel lines on an Euclidean space-time. Complexity as the maximal length of a sequence of consecutive segments is quadratic. We use the continuity of the real line to cover all the possi- ble boolean valuations by a recursive tree structure relying on a fractal pattern: an exponential number of cases are explored simultaneously by a massive parallelism. Keywords. Abstract geometrical computation; Signal machine; Q-SAT; Fractal computation; Massive parallelism; Unconventional computation. 1 Introduction When defining and studying a new model of computation, especially an uncon- ventionnal one, these questions arise naturally: what can we compute (in terms of decidability), how can we compute it, and what does it cost (in terms of com- plexity)? Answers could be found by taking representative problems of classical complexity classes, e.g. SAT for NP or Q-SAT for PSPACE, and coding them in the new computation model.

• bounded space


• exactly matching rule


• boolean


• required meta-signals


• meta-signals speed


• space-time diagram


• signals


• x1

Sujets

• Metric space
• Boolean
• Signals

Informations

• Publié par: profil-zyak-2012
• Nombre de lectures: 13
• Langue: English

Extrait

SolvingQ-SATinboundedspaceandtimeby
geometricalcomputation

DenysDuchier,JérômeDurand-Lose,MaximeSenot
LIFO,UniversityofOrleans,BP6759,F-45067ORLEANSCedex2,FRANCE.

Abstract.
AbstractgeometricalcomputationcansolvePSPACE-com-
pleteproblemsefficiently:anyquantifiedbooleanformula,instanceofQ-
SAT–theproblemofsatisfiabilityofquantifiedbooleanformula–can
bedecidedinboundedspaceandtimewithsimplegeometricalconstruc-
tionsinvolvingonlydrawingparallellinesonanEuclideanspace-time.
Complexityasthemaximallengthofasequenceofconsecutivesegments
isquadratic.Weusethecontinuityofthereallinetocoverallthepossi-
blebooleanvaluationsbyarecursivetreestructurerelyingonafractal
pattern:anexponentialnumberofcasesareexploredsimultaneouslyby
amassiveparallelism.
Keywords.
Abstractgeometricalcomputation;Signalmachine;Q-SAT;
Fractalcomputation;Massiveparallelism;Unconventionalcomputation.

1Introduction
Whendefiningandstudyinganewmodelofcomputation,especiallyanuncon-
ventionnalone,thesequestionsarisenaturally:whatcanwecompute(interms
ofdecidability),howcanwecomputeit,andwhatdoesitcost(intermsofcom-
plexity)?Answerscouldbefoundbytakingrepresentativeproblemsofclassical
complexityclasses,e.g.SATforNPorQ-SATforPSPACE,andcodingthemin
thenewcomputationmodel.ThiswasdoneforNP-problemswithactivemem-
branessystem[Păun,2001]andwithanhyperbolicspaceofcellularautomata
[MargensternandMorita,2001].Similarly,somesolutionsforQ-SATwerepro-
posedwithP-systemsandmembranes[AlhazovandPérez-Jiménez,2007],and
withclosedtimelikecurvesinrelativisticcomputation.Weshowedin[Duchier
etal.,2010]that
signalmachines
,ageometricalandabstractmodelofcomputa-
tion,arecapableofsolvingSATinboundedspaceandtime.Inthepresentpaper,
weextendthisresulttothehighercomplexityclassPSPACEbydescribinga
geometricalconstructionsolvingQ-SATthrough
fractalparallelization
,stillin
constantspaceandtime.
Wealsoofferamorepertinent,model-specific,notionoftime-complexity,
namely
collisiondepth
,whichisquadraticforourproposedconstruction.
Thegeometricalcontextproposedhereisthefollowing:dimensionless
parti-
cles
moveuniformlyontherealaxis.Whenasetofparticlescollide,theyare
replacedbyanewsetofparticlesaccordingtoachosencollectionof
collision
rules
.Weconsiderthetemporalevolutionofthesesystemsthroughtheir
space-
timediagram
,inwhichtracesoftheparticlesarematerializedbylinessegment

thatwecall
signals
.Thespace-timediagramofasignalmachineconstitueda
geometricalcomputation
.
Modelsofcomputation,conventionalornot,arefrequentlybasedonmath-
ematicalidealizationsofphysicalconceptsandinvestigatetheconsequences,on
computationalpower,ofsuchabstractions(quantum,membrane,closedtime-
likecurves,blackholes...).However,oftentimes,theidealizationissuchthat
itmustbeinterpretedeitherasallowinginformationtohaveinfinitedensity
(e.g.anoracle),ortobetransmittedatinfinitespeed(globalclock,nospatial
extension...).Onthisissue,themodelofsignalmachinesstandsincontradis-
tinctionwithotherabstractmodelsofcomputation:itrespectstheprincipleof
causality,densityandspeedofinformationarefinite,asarethesetsofobjects
manipulated.Nonetheless,itremainsaresolutelyabstractmodelwithnoapri-
oriambitiontobephysicallyrealizable;itdealswiththeoreticalissuessuchas
computationalpower.
ItispossibletodoTuring-computationwithsuchasystem[Durand-Lose,
2005]andeventodoanalogcomputationbyasystematicuseofthecontinuityof
spaceandtime[Durand-Lose,2009a,b].Other
geometrical
modelsofcomputa-
tionexistandallowtocompute:coloreduniverses[JacopiniandSontacchi,1990],
geometricmachines[Huckenbeck,1989],piece-wiseconstantderivativesystems
[Bournez,1997],opticalmachines[NaughtonandWoods,2001]...
Mostoftheworktodateinthisdomain,called
abstractgeometricalcom-
putation
(AGC),hasdealtwiththesimulationofsequentialcomputationseven
thoughthemodel,seenasacontinuousextensionofcellularautomata,isinher-
entlyparallel(seeFig.1).Inthepresentpaper,wedescribeamassivelyparallel
evaluationofallpossiblevaluationsforagivenpropositionalformulaandwe
provideawaytocollecttheresults.Thisisthefirsttimethatparallelismis
reallyusedinAGC.

Space(
Z
)Space(
R
)
Fig.1.
Fromcellularautomatatosignalmachines.
Toachievemassiveparallelism,wefollowafractalpatterntoadepthof
n
(for
n
propositionalvariables)inordertopartitionthespacein
2
n
regions
correspondingtothe
2
n
possiblevaluationsoftheunquantifiedformula.Wecall
theresultinggeometricalconstructionthe
combinatorialcomb
ofpropositional
assignments.Withasignalmachine,suchanexponentialconstructionfitsin
boundedspaceandtimeregardlessofthenumberofvariables.
Oncethecombinatorialcombisinplace,itisusedtoimplementabinary
decisiontreeforevaluatingtheformula,whereallbranchesareexploredinparal-
lel.Finally,alltheresultsarecollectedandaggregatedrespectingthequantifiers

oftheQ-SATformulatoyieldthefinalanswer.Ourconstructionproceedsin
stages:wegenerateandcalibrateabeamofsignalsencodingtheformula,making
surethatitfitsinthecombinatorialcomb,wepropagateitthroughthebinary
decisiontree,wecomputethetruthvaluewhenreachingeachvaluation,and
finalizetheansweratthetopofthediagram.
SignalmachinesarepresentedinSection2.Sections3to7detailstepby
stepourgeometricalsolutiontoQ-SAT:splittingthespace,codingtheformula,
broadcastingtheformula,evaluatingitandfinalizingtheanswerbycollecting
theresults.ComplexitiesarediscussedinSection8andconclusionandremarks
aregatheredinSection9.
2Definitions
Satisfiabilityofquantifiedbooleanformulae.
Q-SATisthesatisfiability
problemforquantifiedbooleanformulae(QBF).AQBFisaclosedformulaof
theform:
φ
=
Qx
1
Qx
2
...Qx
n
ψ
(
x
1
,x
2
,...,x
n
)
where
Q
∈{∃
,
∀}
and
ψ
is
aquantifier-freeformulaofpropositionallogic.SATisthefragmentofQ-SAT
usingonlytheexistentialquantifier.
Q-SATis
PSPACE-complete
[StockmeyerandMeyer,1973]:itcanbesolved
byapolynomial-spacealgorithmandanyPSPACE-problemcanbereducedin
polynomialtimetoQ-SAT.Theclassicalalgorithmisrecursive:givenaformula
Qxφ
(
x
)
,itrecursivelydeterminesthesatisfiabilityof
φ
(
true
)
and
φ
(
false
)
,
thenaggregatestheresultswith
∨
if
Q
=
∃
orwith
∧
if
Q
=
∀
.
Signalmachines.
Signalmachinesareanextensionofcellularautomatafrom
discretetimeandspacetocontinuoustimeandspace.Dimensionlesssignals/par-
ticlesmovealongthereallineandrulesdescribewhathappenswhentheycollide.
Signals.
Each
signal
isaninstanceofa
meta-signal
.Theassociatedmeta-signal
definesits
velocity
andwhathappenwhensignalsmeet.Figure2presentsavery
simplespace-timediagram.Timeisincreasingupwardsandthemeta-signalsare
indicatedaslabelsonthesignals.Meta-signalsarelistedontheleftofFig.2.

Meta-SignalsSpeed
0w→−d
−→
iv
3
1ih→−3olb
←
a
−
c
−
k
-3

Fig.2.
Computingthemiddle

Collisionrules
{
w
,
d
−
i
→
v
}
→
{
w
,
h
−→
i
,
l
−→
o
}
−−←→−{
lo
,
w
}
→
{
back
,
w
}
{
h
−→
i
,
b
←
a
−
c
−
k
}
→
{
w
}

Generally,weuseover-linearrowstoindicatethedirectionofpropagationof
ameta-signal.Forexample,
a
←−
and
−
a
→
denotetwodifferentmeta-signals;butas
canbeexpected,theyhavesimilarusesandbehaviors.Similarly
b
r
and
b
l
are
different;botharestationary,butoneismeanttobetheversionforrightand
theotherforleft.

Collisionrules.
Whenasetofsignalscollide,theyarereplacedbyanewsetof
signalsaccordingtoamatchingcollisionrule
{
σ
1
,...,σ
n
}→{
σ
1
0
,...,σ
0
p
}
where
all
σ
i
and
σ
j
0
aremeta-signals.Arulematchesasetofcollidingsignalsifits
left-handsideisequaltothesetoftheirmeta-signals.Bydefault,ifthereisno
exactlymatchingruleforacollision,thebehaviorisdefinedtoregenerateexactly
thesamemeta-signals.Insuchacase,thecollisioniscalled
blank
.Collisionrules
canbededucedfromspace-timediagramasonFig.2.Theyarealsolistedon
therightofthisfigure.
Signalmachine.
Asignalmachineisdefinedbyasetofmeta-signals,asetof
collisionrules,andaninitialconfiguration,i.e.asetofparticlesplacedonthe
realline.Theevolutionofasignalmachinecanberepresentedgeometricallyasa
space-timediagram
:spaceisalwaysrepresentedhorizontally,andtimevertically,
growingupwards.TheexampleofFig.2computesthemiddl