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 Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Generating proofs of unsatisfiability is a valuable capability of most SATsolvers, and is an active area of research for SMT solvers. This paperintroduces the first method to efficiently generate proofs of unsatisfiabilityspecifically for an important subset of SMT: SAT Modulo Monotonic Theories(SMMT), which includes many useful finite-domain theories (e.g., bit vectorsand many graph-theoretic properties) and is used in production at Amazon WebServices. Our method uses propositional definitions of the theory predicates,from which it generates compact Horn approximations of the definitions, whichlead to efficient DRAT proofs, leveraging the large investment the SATcommunity has made in DRAT. In experiments on practical SMMT problems, ourproof generation overhead is minimal (7.41% geometric mean slowdown, 28.8%worst-case), and we can generate and check proofs for many problems that werepreviously intractable.

DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories