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

Resolution over linear equations is a natural extension of the popularresolution refutation system, augmented with the ability to carry out basiccounting. Denoted Res(lin_R), this refutation system operates with disjunctionsof linear equations with boolean variables over a ring R, to refuteunsatisfiable sets of such disjunctions. Beginning in the work of [RT08],through the work of [IS14] which focused on tree-like lower bounds, thisrefutation system was shown to be fairly strong. Subsequent work (cf.[Kra17,IS14, KO18, GK18]) made it evident that establishing lower bounds againstgeneral Res(lin_R) refutations is a challenging and interesting task since thesystem captures a 'minimal' extension of resolution with counting gates forwhich no super-polynomial lower bounds are known to date.  We provide the first super-polynomial size lower bounds on general (dag-like)resolution over linear equations refutations in the large characteristicregime. In particular we prove that the subset-sum principle 1+x1+...+2^n xn=0requires refutations of exponential size over Q. Our proof technique isnontrivial and novel: roughly speaking, we show that under certain conditionsevery refutation of a subset-sum instance f=0 must pass through a fat clausecontaining an equation f=alpha for each alpha in the image of f under booleanassignments. We develop a somewhat different approach to prove exponentiallower bounds against tree-like refutations of any subset-sum instance thatdepends on n variables, hence also separating tree-like from dag-likerefutations over the rationals. (Abstract continued in the full paper.)

Resolution with Counting: Dag-Like Lower Bounds and Different Moduli