Layout-sensitive grammars have been adopted in many modern programming languages.
In a serious language design phase, the specified syntax—typically a grammar—must be unambiguous.
Although checking ambiguity is undecidable for context-free grammars and (trivially also) layout-sensitive grammars, <i>ambiguity detection</i>, on the other hand, is possible and can benefit language designers from <i>exposing potential design flaws</i>.

In this paper, we tackle the ambiguity detection problem in layout-sensitive grammars.
Inspired by a previous work on checking the <i>bounded ambiguity</i> of context-free grammars via <i>SAT solving</i>, we intensively extend their approach to support layout-sensitive grammars but via <i>SMT solving</i> to express the ordering and quantitative relations over line/column numbers.
Our key novelty lies in a <i>reachability</i> condition, which takes the impact of layout constraints on ambiguity into careful account.
With this condition in hand, we propose an equivalent ambiguity notion called <i>local ambiguity</i> for the convenience of SMT encoding.
We translate local ambiguity into an SMT formula and developed a <i>bounded ambiguity checker</i> that <i>automatically</i> finds a <i>shortest</i> nonempty ambiguous sentence (if exists) for a user-input grammar.
The <i>soundness</i> and <i>completeness</i> of our SMT encoding are mechanized in the Coq proof assistant.
We conducted an evaluation on both grammar fragments and <i>full</i> grammars extracted from the language manuals of domain-specific languages like YAML as well as general-purpose languages like Python, which reveals the effectiveness of our approach.