LOGIC PROGRAMMING WITH CARDINALITY CONSTRAINTS

ResearchReports86Teknillisenkorkeakouluntietojenka¨sittelyteorianlaboratoriontutkimusraportti86Espoo2003HUT-TCS-A86LOGICPROGRAMMINGWITHCARDINALITYCONSTRAINTSTommiSyrja¨nenABTEKNILLINENKORKEAKOULUTEKNISKAHÖGSKOLANHELSINKIUNIVERSITYOFTECHNOLOGYTECHNISCHEUNIVERSITÄTHELSINKIUNIVERSITEDETECHNOLOGIED’HELSINKIResearchReports86Teknillisenkorkeakouluntietojenka¨sittelyteorianlaboratoriontutkimusraportti86Espoo2003HUT-TCS-A86LOGICPROGRAMMINGWITHCARDINALITYCONSTRAINTSTommiSyrja¨nenHelsinkiUniversityofTechnologyDepartmentofComputerScienceandEngineeringLaboratoryforTheoreticalComputerScienceTeknillinenkorkeakouluTietotekniikanosastoTietojenka¨sittelyteorianlaboratorioDistribution:HelsinkiUniversityofTechnologyLaboratoryforTheoreticalComputerScienceP.O.Box5400FIN-02015HUTTel.+358-0-4511Fax.[phone]E-mail:[e-mail].ficTommiSyrja¨nenISBN951-22-6896-5ISSN1457-7615MultiprintOyHelsinki2003ABSTRACT:Inthisworkweexaminecardinalityconstraintlogicprograms.Wegiveaformaldefinitionofthestablemodelsemanticsforgeneralcardi-nalityconstraintprogramsanddefineasyntacticsubclassofthem,omega-restrictedprograms,thatstaysdecidableevenwhenfunctionsymbolsareused.Weshowthatthecomputationalcomplexityofomega-restrictedpro-gramsis2-NEXP-completeinthegeneralcaseandNEXP-completeiffunc-tionsymbolsarenotused.Wegiveageneralframeworkforextendingthesemanticsandgivefourextensionstothebasicsemantics,includingclassicalnegationandpartialstablemodelsemantics.Weshowhowtheextensionscanbetranslatedbacktonormalomega-restrictedprogramsandgiveasimi-lartranslationforlogicprogramswithordereddisjunction.Wepresentsomeimplementationdetailsofomega-restrictedprogramsandgiveseveralexam-plesoftheiruse.KEYWORDS:Logicprogramming,cardinalityconstraint,instantiation,sta-blemodelsemantics,smodelsCONTENTSListofSymbolsandNotations....................iii1Introduction11.1OutlineoftheWork.......................51.2ScientificContributions....................52TheStableModelSemanticsofNormalPrograms63CardinalityConstraintPrograms84StableModelSemanticsofCardinalityConstraintPrograms114.1DataModels..........................12HerbrandInterpretations....................15CombiningHerbrandInterpretationsandEvaluatedFunctions174.2RemovalofGlobalVariables..................184.3Expansion............................204.4ReductandStableModelSemantics..............224.5Example.............................255Omega-RestrictedPrograms275.1DependencyGraphs......................285.2TheStableModelSemanticsof!-RestrictedPrograms....356GeneralizingCardinalityConstraints406.1CardinalityConstraints.....................406.2Interpretations,Valuators,andModels.............416.3ImposinganOrderoverModels................426.4StableModels..........................446.5VariablesinCardinalityConstraintBounds..........456.6WeightConstraintLiterals...................466.7ClassicalNegation.......................476.8PartialModels..........................487TranslationsforSemanticExtensions547.1ClassicalNegation.......................557.2Preferences...........................568ComputationalComplexity618.1TuringMachineTranslation..................638.2ComplexityResultsforOmega-RestrictedPrograms......669Implementation779.1Smodels.............................779.2Lparse..............................78Rewriter.............................78Instantiator...........................79LiteralsSets...........................81ivCONTENTS10Examples8110.1APlanningPuzzle.......................8210.2Sokoban.............................8710.3CreatingFiniteAutomata....................9011ConclusionsandFutureWork9511.1FutureWork..........................95Acknowledgements..........................96References96ASourceCodeforExamplePrograms103A.1PlanningPuzzle.........................103A.2HeavilyOptimizedPlanningPuzzle..............104A.3Sokoban.............................106A.4FiniteAutomataConstructor..................115CONTENTSiLISTOFSYMBOLSANDNOTATIONS;theemptyset[setunion\setintersection^logicaland_logicalor:logicalnot(classicalnegation)notnegationasfailureanatomthatisalwaystrueorthemaxi-mumtruthvalue?theminimumtruthvalueX1Xn:hl:a1;:::;amialiteralsetvarsL(S)localvariablesofSlit(S)themainliteralofSonds(S)theconditionsofSLfS1;:::;SngUacardinalityconstraintboundL(C)thelowerboundofCboundU(C)theupperboundofCL(C)theliteralsetsofCpred(A)thepredicatesymboloftheatomAvars(t)thesetofvariablesoccurringinthl1;:::;lnarulehead(r)theheadofrbody+(r)positiveliteralsoccuringinthebodyofrbody(r)negativeliteralsoccuringinthebodyofrbodys(r)simpleconstraintliteralsoccurringinrPalogicprogramDadatamodelhP;DiacombinedprogramandadatamodelavocabularyUanuniverseIaninterpretationNasetofnamesFthesetofallfunctionsymbolsPthesetofallpredicatesymbolsPDthesetofdatapredicatesPPthesetofprogrampredicates℄datamodelaugmentationoperatorDPthefinaldatamodelofan!-restrictedprogramPasubstitutioninst(P;D)apartialinstantiationofhP;DiE(S;D)theexpansionofSw.r.t.DE0(S;D)thesimpleexpansionofSw.r.t.DE0s(S;D)thesatisfiedexpansionofSw.r.t.DHI(P;D)theHerbrandinstantiat