Výsledky vyhledávání

Toward Verifying Nonlinear Integer Arithmetic

Autor: Vincent Liew, Paul Beame

Publikováno v: Journal of the ACM. 66:1-30

We eliminate a key roadblock to efficient verification of nonlinear integer arithmetic using CDCL SAT solvers, by showing how to construct short resolution proofs for many properties of the most widely used multiplier circuits. Such short proofs were

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::43b4785da1e11b1ccbd0bf53d519678f
https://doi.org/10.1145/3319396

Zobrazit plný text záznamu

Exact Model Counting of Query Expressions

Autor: Dan Suciu, Sudeepa Roy, Jerry Li, Paul Beame

Publikováno v: ACM Transactions on Database Systems. 42:1-46

We prove exponential lower bounds on the running time of the state-of-the-art exact model counting algorithms—algorithms for exactly computing the number of satisfying assignments, or the satisfying probability, of Boolean formulas. These algorithm

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::f8c5b1dd8e65692ea323f0e3da0e9fe1
https://doi.org/10.1145/2984632

Zobrazit plný text záznamu

Nondeterminism and An Abstract Formulation of Nečiporuk’s Lower Bound Method

Autor: Nathan Grosshans, Pierre McKenzie, Luc Segoufin, Paul Beame

Publikováno v: ACM Transactions on Computation Theory
ACM Transactions on Computation Theory, ACM, 2016, 9 (1), pp.1-34. ⟨10.1145/3013516⟩
ACM Transactions on Computation Theory, 2016, 9 (1), pp.1-34. ⟨10.1145/3013516⟩

A formulation of Nečiporuk’s lower bound method slightly more inclusive than the usual complexity-measure-specific formulation is presented. Using this general formulation, limitations to lower bounds achievable by the method are obtained for seve

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7cf18065ee7bb264ea3124d24b7bd3dd
https://doi.org/10.1145/3013516

Zobrazit plný text záznamu

Time-Space Trade-offs in Resolution: Superpolynomial Lower Bounds for Superlinear Space

Autor: Chris Beck, Paul Beame, Russell Impagliazzo

Publikováno v: SIAM Journal on Computing. 45:1612-1645

We give the first time-space trade-off lower bounds for resolution proofs that apply to superlinear space. In particular, we show that there are formulas of size $N$ that have resolution refutations of size (and space) $T(N)= N^{\Theta(\log N)}$ (and

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::1b1ae18015085f042150e417579e8253
https://doi.org/10.1137/130914085

Zobrazit plný text záznamu

Technical perspective: Two for the price of one

Autor: Paul Beame

Publikováno v: Communications of the ACM. 63:96-96

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::b974269d1da7c4861ce915f468b4c697
https://doi.org/10.1145/3416264

Zobrazit plný text záznamu

On the Bias of Reed-Muller Codes over Odd Prime Fields

Autor: Xin Yang, Shayan Oveis Gharan, Paul Beame

We study the bias of random bounded-degree polynomials over odd prime fields and show that, with probability exponentially close to 1, such polynomials have exponentially small bias. This also yields an exponential tail bound on the weight distributi

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::66047ec2e8072bc303bcb2c72d164625
http://arxiv.org/abs/1806.06973

Zobrazit plný text záznamu

Edge Estimation with Independent Set Oracles

Autor: Cyrus Rashtchian, Makrand Sinha, Paul Beame, Sivaramakrishnan Natarajan Ramamoorthy, Sariel Har-Peled

We study the task of estimating the number of edges in a graph with access to only an independent set oracle. Independent set queries draw motivation from group testing and have applications to the complexity of decision versus counting problems. We

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4765a0cf77de2ed9e4895c96b8e27bbe

Zobrazit plný text záznamu