English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

In Verification and in (optimal) AI Planning, a successful method is toformulate the application as boolean satisfiability (SAT), and solve it withstate-of-the-art DPLL-based procedures. There is a lack of understanding of whythis works so well. Focussing on the Planning context, we identify a form ofproblem structure concerned with the symmetrical or asymmetrical nature of thecost of achieving the individual planning goals. We quantify this sort ofstructure with a simple numeric parameter called AsymRatio, ranging between 0and 1. We run experiments in 10 benchmark domains from the InternationalPlanning Competitions since 2000; we show that AsymRatio is a good indicator ofSAT solver performance in 8 of these domains. We then examine carefully craftedsynthetic planning domains that allow control of the amount of structure, andthat are clean enough for a rigorous analysis of the combinatorial searchspace. The domains are parameterized by size, and by the amount of structure.The CNFs we examine are unsatisfiable, encoding one planning step less than thelength of the optimal plan. We prove upper and lower bounds on the size of thebest possible DPLL refutations, under different settings of the amount ofstructure, as a function of size. We also identify the best possible sets ofbranching variables (backdoors). With minimum AsymRatio, we prove exponentiallower bounds, and identify minimal backdoors of size linear in the number ofvariables. With maximum AsymRatio, we identify logarithmic DPLL refutations(and backdoors), showing a doubly exponential gap between the two structuralextreme cases. The reasons for this behavior -- the proof arguments --illuminate the prototypical patterns of structure causing the empiricalbehavior observed in the competition benchmarks

Structure and Problem Hardness: Goal Asymmetry and DPLL Proofs in SAT-Based Planning