Backdoors to tractable answer set programming

Artificial Intelligence - Tập 220 - Trang 64-103 - 2015
Johannes Klaus Fichte1,2, Stefan Szeider1
1Vienna University of Technology, Favoritenstrasse 9-11, 1040 Vienna, Austria
2University of Potsdam, August-Bebel-Strasse 89, 14482 Potsdam, Germany

Tài liệu tham khảo

Andres, 2012, Unsatisfiability-based optimization in clasp, vol. 17, 212 Apt, 1988, Towards a theory of declarative knowledge, 89 Ben-Eliyahu, 1994, Propositional semantics for disjunctive logic programs, Ann. Math. Artif. Intell., 12, 53, 10.1007/BF01530761 Ben-Eliyahu, 1996, A hierarchy of tractable subsets for computing stable models, J. Artif. Intell. Res., 5, 27, 10.1613/jair.223 Bidoít, 1991, Negation by default and unstratifiable logic programs, Theor. Comput. Sci., 78, 85, 10.1016/0304-3975(51)90004-7 Bodlaender, 2008, Combinatorial optimization on graphs of bounded treewidth, Comput. J., 51, 255, 10.1093/comjnl/bxm037 Bodlaender, 2009, On problems without polynomial kernels, J. Comput. Syst. Sci., 75, 423, 10.1016/j.jcss.2009.04.001 Bodlaender, 1993, A tourist guide through treewidth, Acta Cybern., 11, 1 Bodlaender, 1997, Treewidth: algorithmic techniques and results, vol. 1295, 19 Bodlaender, 2005, Discovering treewidth, vol. 3381, 1 Bondy, 2008, Graph Theory, vol. 244 Bonsma, 2011, Feedback vertex set in mixed graphs, vol. 6844, 122 Brass, 1998, Characterizations of the disjunctive well-founded semantics: confluent calculi and iterated GCWA, J. Autom. Reason., 20, 143, 10.1023/A:1005952908693 Cadoli, 1994, The complexity of propositional closed world reasoning and circumscription, J. Comput. Syst. Sci., 48, 255, 10.1016/S0022-0000(05)80004-2 Cai, 2010, Ewls: a new local search for minimum vertex cover, 45 Cai, 2013, Numvc: an efficient local search algorithm for minimum vertex cover, J. Artif. Intell. Res., 46, 687, 10.1613/jair.3907 Cai, 2011, Local search with edge weighting and configuration checking heuristics for minimum vertex cover, Artif. Intell., 175, 1672, 10.1016/j.artint.2011.03.003 Calimeri, 2011, The third answer set programming competition: preliminary report of the system competition track, vol. 6645, 388 Chandra, 1985, Horn clause queries and generalizations, J. Log. Program., 2, 1, 10.1016/0743-1066(85)90002-0 Chen, 2005, A model for generating random quantified Boolean formulas, 66 Chen, 2008, A fixed-parameter algorithm for the directed feedback vertex set problem, J. ACM, 55, 1, 10.1145/1411509.1411511 Chen, 2010, Improved upper bounds for vertex cover, Theor. Comput. Sci., 411, 3736, 10.1016/j.tcs.2010.06.026 Chitnis, 2012, Directed subset feedback vertex set is fixed-parameter tractable, vol. 7391, 230 Chvatal, 1983, Linear Programming Cook, 2013, A hybrid branch-and-bound approach for exact rational mixed-integer programming, Math. Program. Comput., 5, 305, 10.1007/s12532-013-0055-6 Marek Cygan, 2011, Subset feedback vertex set is fixed-parameter tractable, vol. 6755, 449 Dantsin, 2001, Complexity and expressive power of logic programming, ACM Comput. Surv., 33, 374, 10.1145/502807.502810 DeHaan, 2014, The parameterized complexity of reasoning problems beyond NP Denecker, 2009, The second answer set programming competition, vol. 5753, 637 Diestel, 2000, Graph Theory, vol. 173 Dilkina, 2007, Tradeoffs in the complexity of backdoor detection, vol. 4741, 256 Dilkina, 2008, Tradeoffs in backdoor detection for Sat and Unsat formulas, 256 Dowling, 1984, Linear-time algorithms for testing the satisfiability of propositional Horn formulae, J. Log. Program., 1, 267, 10.1016/0743-1066(84)90014-1 Downey, 1999, Parameterized Complexity, 10.1007/978-1-4612-0515-9 Downey, 2013, Fundamentals of Parameterized Complexity, 10.1007/978-1-4471-5559-1 Downey, 1999, Parameterized complexity: a framework for systematically confronting computational intractability, vol. 49, 49 Drescher, 2008, Conflict-driven disjunctive answer set solving, 422 Drescher, 2008, Heuristics in conflict resolution, vol. UNSW-CSE-TR-0819, 141 Dunne, 2007, Computational properties of argument systems satisfying graph-theoretic constraints, Artif. Intell., 171, 701, 10.1016/j.artint.2007.03.006 Dvořák, 2012, Augmenting tractable fragments of abstract argumentation, Artif. Intell., 186, 157, 10.1016/j.artint.2012.03.002 Eiter, 1995, On the computational cost of disjunctive logic programming: propositional case, Ann. Math. Artif. Intell., 15, 289, 10.1007/BF01536399 Eiter, 2004, Simplifying logic programs under uniform and strong equivalence, vol. 2923, 87 Erdem, 2003, Tight logic programs, Theory Pract. Log. Program., 3, 499, 10.1017/S1471068403001765 Stein Faber, 1999, Using database optimization techniques for nonmonotonic reasoning, 135 Fages, 1994, Consistency of Clark's completion and existence of stable models, Log. Methods Comput. Sci., 1, 51 Fichte, 2011, Backdoors to tractable answer-set programming, 863 Fichte, 2013, Backdoors to normality for disjunctive logic programs, 320 Fichte, 2012, The good, the bad, and the odd: cycles in answer-set programs, vol. 7415, 78 Flum, 2006, Parameterized Complexity Theory, vol. XIV Fortnow, 2011, Infeasibility of instance compression and succinct PCPs for NP, J. Comput. Syst. Sci., 77, 91, 10.1016/j.jcss.2010.06.007 Fortune, 1980, The directed subgraph homeomorphism problem, Theor. Comput. Sci., 10, 111, 10.1016/0304-3975(80)90009-2 Gario, 2012, Horn backdoor detection via vertex cover: benchmark description Gaspers, 2012, Backdoors to acyclic SAT, vol. 7391, 363 Gaspers, 2012, Backdoors to satisfaction, vol. 7370, 287 Gaspers, 2012, Strong backdoors to nested satisfiability, vol. 7317, 72 Gaspers, 2013, Strong backdoors to bounded treewidth SAT, 489 Gaspers, 2014, Guarantees and limits of preprocessing in constraint satisfaction and reasoning, Artif. Intell., 216, 1, 10.1016/j.artint.2014.06.006 Gaspers, 2013, Backdoors to q-Horn, vol. 20, 67 Martin Gebser, Roland Kaminski, Personal communication, 2012. Gebser Gebser, 2007, Conflict-driven answer set solving, 386 Gebser, 2007, The first answer set programming system competition, vol. 4483, 3 Gebser, 2007, Gringo: a new grounder for answer set programming, vol. 4483, 266 Gebser, 2008, Advanced preprocessing for answer set solving, vol. 178, 15 Gebser, 2010 Gebser, 2011, Detecting inconsistencies in large biological networks with answer set programming, Theory Pract. Log. Program., 11, 323, 10.1017/S1471068410000554 Gebser, 2011, Challenges in answer set solving, vol. 6565, 74 Gebser, 2011, Multi-criteria optimization in answer set programming, vol. 11, 1 Gebser, 2011, Complex optimization in answer set programming, Theory Pract. Log. Program., 11, 821, 10.1017/S1471068411000329 Gebser, 2011, Potassco: the Potsdam answer set solving collection, AI Commun., 24, 107, 10.3233/AIC-2011-0491 Gebser, 2012, Conflict-driven answer set solving: from theory to practice, Artif. Intell., 187, 52, 10.1016/j.artint.2012.04.001 Gebser, 2012 Gebser, 2013, Matchmaking with answer set programming, vol. 8148, 342 Gebser, 2013, Domain-specific heuristics in answer set programming, 350 Gebser, 2014, Answer set programming as SAT modulo acyclicity, vol. 263, 351 Van Gelder, 1989, Negation as failure using tight derivations for general logic programs, J. Log. Program., 6, 109, 10.1016/0743-1066(89)90032-0 Gelfond, 1988, The stable model semantics for logic programming, vol. 2, 1070 Gelfond, 1991, Classical negation in logic programs and disjunctive databases, New Gener. Comput., 9, 365, 10.1007/BF03037169 Giunchiglia, 1998, Act, and the rest will follow: exploiting determinism in planning as satisfiability, 948 Giunchiglia, 2002, Dependent and independent variables in propositional satisfiability, 296 Giunchiglia, 2006, Answer set programming based on propositional satisfiability, J. Autom. Reason., 36, 345, 10.1007/s10817-006-9033-2 Gottlob, 2004, Hypergraphs in model checking: acyclicity and hypertree-width versus clique-width, SIAM J. Comput., 33, 351, 10.1137/S0097539701396807 Gottlob, 2008, Fixed-parameter algorithms for artificial intelligence, constraint satisfaction and database problems, Comput. J., 51, 303, 10.1093/comjnl/bxm056 Gottlob, 2002, Fixed-parameter complexity in AI and nonmonotonic reasoning, Artif. Intell., 138, 55, 10.1016/S0004-3702(02)00182-0 Gottlob, 2010, Bounded treewidth as a key to tractability of knowledge representation and reasoning, Artif. Intell., 174, 105, 10.1016/j.artint.2009.10.003 Inc. Gurobi Optimization, Gurobi optimizer reference manual, Version 5.0.2, 2014. Hoos, 2012, Automated algorithm configuration and parameter tuning, 37 IBM, IBM ILOG CPLEX optimization studio CPLEX user's manual, version 12 release 4 edition, 2011. Jakl, 2009, Answer-set programming with bounded treewidth, vol. 2, 816 Janhunen, 2011, Compact translations of non-disjunctive answer set programs to propositional clauses, vol. 6565, 111 Janhunen, 2006, Unfolding partiality and disjunctions in stable model semantics, ACM Trans. Comput. Log., 7, 1, 10.1145/1119439.1119440 Janhunen, 2009, Computing stable models via reductions to difference logic, vol. 5753, 142 Janota, 2011, A tool for circumscription-based MUS membership testing, vol. 6645, 266 Järvisalo, 2009, Limitations of restricted branching in clause learning, Constraints, 14, 325, 10.1007/s10601-008-9062-z Järvisalo, 2008, The effect of structural branching on the efficiency of clause learning SAT solving: an experimental study, J. Algorithms, 63, 90, 10.1016/j.jalgor.2008.02.005 Jost, 2012, Suggesting new interactions related to events in a social network for elderly Kakimura, 2012, Erdös-Pósa property and its algorithmic applications: parity constraints, subset feedback set, and subset packing, 1726 Kanchanasut, 1992, Transforming normal logic programs to constraint logic programs, Theor. Comput. Sci., 105, 27, 10.1016/0304-3975(92)90286-O Karp, 1980, Some connections between nonuniform and uniform complexity classes, 302 Katebi, 2011, Empirical study of the anatomy of modern Sat solvers, vol. 6695, 343 Kawarabayashi, 2010 Kottler, 2008, A new bound for an NP-hard subclass of 3-SAT using backdoors, vol. 4996, 161 Lapaugh, 1984, The even-path problem for graphs and digraphs, Networks, 14, 507, 10.1002/net.3230140403 Lee, 2003, Loop formulas for disjunctive logic programs, vol. 2916, 451 Leone, 1997, Disjunctive stable models: unfounded sets, fixpoint semantics, and computation, Inf. Comput., 135, 69, 10.1006/inco.1997.2630 Leone, 2006, The DLV system for knowledge representation and reasoning, ACM Trans. Comput. Log., 7, 499, 10.1145/1149114.1149117 Lierler, 2005, CMODELS – SAT-based disjunctive answer set solver, vol. 3662, 447 Lin, 2003, On tight logic programs and yet another translation from normal logic programs to propositional logic, 853 Lin, 2004, On odd and even cycles in normal logic programs, 80 Lin, 2004, ASSAT: computing answer sets of a logic program by SAT solvers, Artif. Intell., 157, 115, 10.1016/j.artint.2004.04.004 Liu, 2012, Answer set programming via mixed integer programming, 32 Marek, 1991, Autoepistemic logic, J. ACM, 38, 588, 10.1145/116825.116836 Marek, 1991, Computing intersection of autoepistemic expansions, 37 Marek, 1999, Stable models and an alternative logic programming paradigm, 375 Misra, 2012, Parameterized algorithms for even cycle transversal, vol. 7551, 172 Montalva, 2008, On the complexity of feedback set problems in signed digraphs, Electron. Notes Discrete Math., 30, 249, 10.1016/j.endm.2008.01.043 Morak, 2012, Preprocessing of complex non-ground rules in answer set programming, vol. 17, 247 Morak, 2010, A dynamic-programming based ASP-solver, vol. 6341, 369 Niedermeier, 2006, Invitation to Fixed-Parameter Algorithms, vol. 31 Niemelä, 1994, On the impact of stratification on the complexity of nonmonotonic reasoning, J. Appl. Non-Class. Log., 4, 141, 10.1080/11663081.1994.10510830 Niemelä, 1999, Logic programs with stable model semantics as a constraint programming paradigm, Ann. Math. Artif. Intell., 25, 241, 10.1023/A:1018930122475 Nishimura, 2004, Detecting backdoor sets with respect to Horn and binary clauses, vol. 3542, 96 Nishimura, 2007, Solving #SAT using vertex covers, Acta Inform., 44, 509, 10.1007/s00236-007-0056-x Pfandler, 2013, Backdoors to abduction, 1046 Pichler, 2009, Belief revision with bounded treewidth, vol. 5753, 250 Pipatsrisawat, 2007, A lightweight component caching scheme for satisfiability solvers, vol. 4501, 294 Razgon, 2009, Almost 2-SAT is fixed parameter tractable, J. Comput. Syst. Sci., 75, 435, 10.1016/j.jcss.2009.04.002 Ricca, 2012, Team-building with answer set programming in the Gioia-Tauro seaport, Theory Pract. Log. Program., 12, 361, 10.1017/S147106841100007X Robertson, 1984, Graph minors. III. Planar tree-width, J. Comb. Theory, Ser. B, 36, 49, 10.1016/0095-8956(84)90013-3 Robertson, 1985, Graph minors – a survey, 153 Robertson, 1986, Graph minors. II. Algorithmic aspects of tree-width, J. Algorithms, 7, 309, 10.1016/0196-6774(86)90023-4 Robertson, 1999, Permanents, Pfaffian orientations, and even directed circuits, Ann. Math., 150, 929, 10.2307/121059 Rosamond, 2010, Table of races, 4 Ruan, 2004, The backdoor key: a path to understanding problem hardness, 124 Samer, 2008, Backdoor trees, 363 Samer, 2009, Backdoor sets of quantified Boolean formulas, J. Autom. Reason., 42, 77, 10.1007/s10817-008-9114-5 Samer, 2009, Fixed-parameter tractability, 425 Schnorr, 1981, On self-transformable combinatorial problems, vol. 14, 225 Schrijver, 1998 Simons, 2002, Extending and implementing the stable model semantics, Knowledge Representation and Logic Programming, Artif. Intell., 138, 181 Carsten, 2005, Towards an optimal CNF encoding of boolean cardinality constraints, vol. 3709, 827 Strichman, 2000, Tuning SAT checkers for bounded model checking, vol. 1855, 480 Szeider, 2008, Matched formulas and backdoor sets, J. Satisf. Boolean Model. Comput., 6, 1 Thielscher, 2009, Answer set programming for single-player games in general game playing, vol. 5649, 327 Thomassé, 2009, A quadratic kernel for feedback vertex set, 115 To, 2009, A conformant planner with explicit disjunctive representation of belief states, 305 Truszczyński, 2011, Trichotomy and dichotomy results on the complexity of reasoning with disjunctive logic programs, Theory Pract. Log. Program., 11, 881, 10.1017/S1471068410000463 Van Emden, 1976, The semantics of predicate logic as a programming language, J. ACM, 23, 733, 10.1145/321978.321991 van Rossum, 1995 Vazirani, 1988, Pfaffian orientations, 0/1 permanents, and even cycles in directed graphs, vol. 317, 667 Williams, 2003, Backdoors to typical case complexity, 1173 Williams, 2003, On the connections between backdoors, restarts, and heavy-tailedness in combinatorial search, 222 Yap, 1983, Some consequences of nonuniform conditions on uniform classes, Theor. Comput. Sci., 26, 287, 10.1016/0304-3975(83)90020-8 Zhao, 2003, Answer set programming phase transition: a study on randomly generated programs, vol. 2916, 239 Zhao, 2002