Diplomverko pri programado kun limigoj

Resumo

La simulilo ripetas multajn kondiĉojn laŭeble pli ofte kiam okazaĵoj povas okazi plej diversmaniere. Se eblas taksi el la progreso, ke 'ĉi tiu kondiĉo jam neniam validos', ĉu eblas sekure ĉesi tiu inspektadon? Ni desegnis kaj efektivigis metodon por la modeliga lingvo de hibrida sistemo HydLa, kiu, uzante la direkton de valoroŝanĝo kiel indikon, forigas neiniciatajn kondiĉojn el aktuala serĉado.

En la taksa modelo, la realigtempo estis mallongigita al ĉirkaŭ duono de la tradicia sen ŝanĝi la simulan rezulton. La graveco ne estas en simple rapido de ĉiuj kalkuloj, sed en la uzo de la problemo-strukturo por malpliigi la eblecojn necesajn konsideri.

La koncepto de limigita programado lernita en ĉi tiu esploro nun formas la fundamenton de Mia desegnfilozofio. Anstataŭ rekte specifii unuopajn rezultojn, oni difinas regulojn, prioritatojn kaj limojn, kaj derivemsolvojn el ili interne.

Defioj — ju pli da eblecoj, des pli malrapida estas la kalkulado

HydLa estas lingvo por priskribi “hibridajn sistemojn”, kiuj kombinas kontinuan ŝanĝon kaj diskretajn eventojn, kiel matematikajn kaj logikajn limigojn. Sen neceso skribi ĉiujn procedurojn en ordo, oni povas simuli konduton kiu kontentigas kondiĉojn per deklarado kio devus okazi.

Aliflanke, en modelo kun multaj reguloj kiuj validas depende de kondiĉoj, la simuililo ripete kontrolas grandan nombron da kandidatoj. Ĉar ili restas kiel kandidatoj eĉ se la kondiĉoj jam ne validas aŭ iam en la estonteco, la pli granda la modelo, des pli multaj nebezonataj kalkuloj akumuliĝas.

Temo — Sistemo kie miksiĝas kontinua kaj diskreta

La saltanta pilko estas klara ekzemplo de hibrida sistemo. En aerospaco ĝia pozicio kaj rapido ŝanĝiĝas kontinue, sed kiam ĝi frapas la plankon, okazas disreta evento de reboto. Termostato, aŭtomobilo kaj roboto ankaŭ enhavas la samajn du tipojn de ŝanĝoj interne, kvankam sur malsamaj skaloj.

Por taksado, oni uzis modelon en kiu horizontale moviĝanta pilko rebatis sur surfaco dividita en plurajn sekciojn. Ĉiu sekcio havas regulon kun kondiĉo: 'se la pilko atingas ĉi tiun gamon, ĝi rebatos'. Pliigante la nombro de sekcioj, oni povas reprezenti pli da objektoj, sed ankaŭ la simulatoro devas esplori pli da kondiĉoj.

Kollo — la nombro de kondiĉoj plialtigas la komputdan laboron

Reguloj kiuj validas nur kiam certaj kondiĉoj estas plenumitaj estas nomataj 'kun-gvardiaj restriktoj'. En la taksa modelo, la rebatiĝa regulo de specifa sekcio validas nur kiam la pilko atingas la plankon kaj ĝia horizontala pozicio troviĝas ene de tiu sekcio.

Kiam oni pliigis la nombron de sekcioj de 10 ĝis 200, la tradicia simuliilo malrapidis proksimume laŭ la kvadrato de la sekcia nombro. En grandaj modeloj, ĉar la nombro de objektoj, kontaktoareoj kaj eblaj eventoj kreskas, la sama problemo fariĝas pli granda.

Esploro — 96% de la prilaborada tempo troviĝis kie

Kiam oni mezuris la prilaboran tempon, en modelo kun 100 blokoj, 96% de la tuta tempo estis uzata por FindMinTime. Ĉi tio estas la procezo por trovi la «plej proksime okazos» inter la kandidatoj. Tial ĉiuj gardaj kondiĉoj estis taksataj plurfoje.

La lokoj por plibonigo fariĝis klaraj. Anstataŭ rekrei la tutan kalkulmetodon, simple sekure malpliigi la kandidatojn transdonotajn al FindMinTime. La celo estis ne ŝanĝi la simulan rezulton sed forigi nur la nebezonatajn eblecojn.

Alproksimiĝo — sekure forigi kondiĉojn, kiujn ne eblas plu ricevi

Bonvolu imagi pilkon malsupren saltantan ŝtuparon. Se la pilko preterpasas unu paŝon kaj daŭre progresas antaŭen, tiu paŝo jam ne povas influi la pilkon. Homo rigardanta la diagramon tuj ignoras la paŝojn malantaŭ la pilko. La originala algoritmo daŭre kontrolis ĉiun el ili unu post alia.

La malfacilaĵo estas montrado ke la forigita gardilo poste ne estos bezonata. Se oni forigas ĝin nur ĉar nuntempe ĝi estas falsa, kiam ĝi denove fariĝos vera, ĝi povus silenteme doni malĝustan rezulton. Tial la proponita metodo uzas monotonecon — ĉu oni povas garantii, ke certa variablo daŭre kreskas aŭ malpliiĝas dum certa tempointerspaco.

Kiam la direkto de ŝanĝo ne ŝanĝiĝas

La unua aliro taŭgas kiam variablo moviĝas unuflanken tra la tuta simulaĵo. En modelo kun dividitaj surfacoj, la horizontala pozicio de la pilko ĉiam kreskas. Post kiam ĝi transpasos iun sekcion, la kondiĉoj de tiu sekcio neniam plu estos plenigitaj. Ĉi tiu trajto povas esti kontrolita antaŭ la simulaĵo per modela kontrola tekniko, do la gardoj, kiuj fariĝis nenecesaj dum la ekzekuto, povas esti sekure forigitaj.

Kiam la direkto de ŝanĝo ŝanĝiĝas meze

Multaj realaj sistemoj ne moviĝas ĉiam en unu direkto. Variabloj povas pliiĝi, ŝanĝi direkton kaj poste malpliiĝi. Tial la artikolo prezentis duan aliron. Unue oni supozas direkton, monitoras tiun supozon per aserto, kaj refaras la reduktan procezon ekde la momento kiam la direkto ŝanĝiĝas. Gardoj forigitaj por unu monotona segmento estas revenigitaj kiam la sekva segmento komenciĝas.

Rezulto — Reduci la ekzekutan tempon de la taksila modelo proksimume je duono

Ni efektivigis respondon al uniforma monotoneco kaj taksis ĝin per modelo kun dividitaj surfacoj. Tamen, ĉu la originala algoritmo aŭ la proponita metodo, la bezonata tempo pliiĝas kiam la nombro de segmentoj kreskas. Tamen, la proponita metodo konstante postulas malpli da laboro. Komparante la kongruajn kurbojn, la plej alta koeficiento malkreskis de 1.1463 al 0.6083, kaj en ĉi tiu referenca testado la tuta simula tempo reduktiĝis preskaŭ duoble.

Ĉi tio ne estas aserto, ke ĉiuj modeloj de HydLa duobliĝos je rapideco. Ĝi montras, kie ĉi tiu metodo funkcias — en modeloj kun multaj celoj kun gardoj, kie la direkto de ŝanĝo povas esti pruvita, kaj dum la ekzekuto la gardoj fariĝas permanente neapartenantaj.

Perspektivoj akiritaj de ĉi tiu esploro

En ĉi tiu esploro, oni ne celis iom post iom plirapidigi individuajn kalkulojn. Oni uzis tion, kion oni scias pri la konduto de la sistemo, por malpliigi la aron de eblecoj konsiderindaj. La ideo limigi la serĉospacon sen ŝanĝi la rezulton estas la forto de restrikta programado.

La efektivigo kaj taksado estis farita por la kazo, kie variablo daŭre moviĝas en unu direkto. Se la direkto de ŝanĝo ŝanĝiĝas meze, ĝi restas nur ĝis la projektado, kaj la taksado restis kiel estonta tasko. Eblas ankaŭ uzi proprietojn krom monotoneco por trovi ankoraŭ pliajn malbezonatajn limigojn.

La fakto ke nun mi ne desegnas rekte la produktadon de AI, sed desegnas la kondiĉojn kaj limojn kiujn AI povas esplori, ankaŭ devenas de ĉi tiu sperto. Kiam oni traktas kompleksajn rezultojn, gravas difini kion oni ne bezonas konsideri, same grave kiel kion kalkuli.