Change search
Link to record
Permanent link

Direct link
BETA
Alternative names
Publications (10 of 44) Show all publications
de Rezende, S. F., Meir, O., Nordström, J. & Robere, R. (2019). Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling. In: Proceedings of the 34th Annual Computational Complexity Conference (CCC ’19): . Paper presented at Computational Complexity Conference (pp. 18:1-18:16).
Open this publication in new window or tab >>Nullstellensatz Size-Degree Trade-offs from Reversible Pebbling
2019 (English)In: Proceedings of the 34th Annual Computational Complexity Conference (CCC ’19), 2019, p. 18:1-18:16Conference paper, Published paper (Other academic)
Abstract [en]

We establish an exactly tight relation between reversible pebblings of graphs and Nullstellensatz refutations of pebbling formulas, showing that a graph G can be reversibly pebbled in time t and space s if an only if there is a Nullstellensatz refutation of the pebbling formula over G in size t + 1 and degree s (independently of the field in which the Nullstellensatz refutation is made). We use this correspondence to prove a number of strong size-degree trade-offs for Nullstellensatz, which to the best of our knowledge are the first such results for this proof system.

National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-249609 (URN)
Conference
Computational Complexity Conference
Note

QC 20190527

Available from: 2019-04-12 Created: 2019-04-12 Last updated: 2019-05-27Bibliographically approved
Atserias, A., Bonacina, I., de Rezende, S. F., Lauria, M., Nordström, J. & Razborov, A. (2018). Clique Is Hard on Average for Regular Resolution. In: Diakonikolas, I Kempe, D Henzinger, M (Ed.), STOC'18: PROCEEDINGS OF THE 50TH ANNUAL ACM SIGACT SYMPOSIUM ON THEORY OF COMPUTING. Paper presented at 50th Annual ACM Symposium on Theory of Computing, STOC 2018; Los Angeles; United States; 25 June 2018 through 29 June 2018 (pp. 866-877). ASSOC COMPUTING MACHINERY
Open this publication in new window or tab >>Clique Is Hard on Average for Regular Resolution
Show others...
2018 (English)In: STOC'18: PROCEEDINGS OF THE 50TH ANNUAL ACM SIGACT SYMPOSIUM ON THEORY OF COMPUTING / [ed] Diakonikolas, I Kempe, D Henzinger, M, ASSOC COMPUTING MACHINERY , 2018, p. 866-877Conference paper, Published paper (Refereed)
Abstract [en]

We prove that for k << (4)root n regular resolution requires length n(Omega(k)) to establish that an Erdos Renyi graph with appropriately chosen edge density does not contain a k-clique. This lower bound is optimal up to the multiplicative constant in the exponent, and also implies unconditional n(Omega(k)) lower bounds on running time for several state-of-the-art algorithms for finding maximum cliques in graphs.

Place, publisher, year, edition, pages
ASSOC COMPUTING MACHINERY, 2018
Keywords
Proof complexity, regular resolution, k-clique, Erdos-Renyi random graphs
National Category
Discrete Mathematics
Identifiers
urn:nbn:se:kth:diva-244573 (URN)10.1145/3188745.3188856 (DOI)000458175600074 ()2-s2.0-85043471352 (Scopus ID)
Conference
50th Annual ACM Symposium on Theory of Computing, STOC 2018; Los Angeles; United States; 25 June 2018 through 29 June 2018
Note

QC 20190308

Available from: 2019-03-08 Created: 2019-03-08 Last updated: 2019-07-29Bibliographically approved
Vinyals, M., Elffers, J., Giráldez Crú, J., Gocht, S. & Nordström, J. (2018). In between resolution and cutting planes: A study of proof systems for pseudo-boolean SAT solving. In: 21st International Conference on Theory and Applications of Satisfiability Testing, SAT 2018 Held as Part of the Federated Logic Conference, FloC 2018: . Paper presented at 21st International Conference on Theory and Applications of Satisfiability Testing, SAT 2018 Held as Part of the Federated Logic Conference, FloC 2018, Oxford, United Kingdom, 9 July 2018 through 12 July 2018 (pp. 292-310). Springer, 10929
Open this publication in new window or tab >>In between resolution and cutting planes: A study of proof systems for pseudo-boolean SAT solving
Show others...
2018 (English)In: 21st International Conference on Theory and Applications of Satisfiability Testing, SAT 2018 Held as Part of the Federated Logic Conference, FloC 2018, Springer, 2018, Vol. 10929, p. 292-310Conference paper, Published paper (Refereed)
Abstract [en]

We initiate a proof complexity theoretic study of subsystems of cutting planes (CP) modelling proof search in conflict-driven pseudo-Boolean (PB) solvers. These algorithms combine restrictions such as that addition of constraints should always cancel a variable and/or that so-called saturation is used instead of division. It is known that on CNF inputs cutting planes with cancelling addition and saturation is essentially just resolution. We show that even if general addition is allowed, this proof system is still polynomially simulated by resolution with respect to proof size as long as coefficients are polynomially bounded. As a further way of delineating the proof power of subsystems of CP, we propose to study a number of easy (but tricky) instances of problems in NP. Most of the formulas we consider have short and simple tree-like proofs in general CP, but the restricted subsystems seem to reveal a much more varied landscape. Although we are not able to formally establish separations between different subsystems of CP—which would require major technical breakthroughs in proof complexity—these formulas appear to be good candidates for obtaining such separations. We believe that a closer study of these benchmarks is a promising approach for shedding more light on the reasoning power of pseudo-Boolean solvers.

Place, publisher, year, edition, pages
Springer, 2018
Series
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ISSN 0302-9743 ; 10929
National Category
Other Engineering and Technologies
Identifiers
urn:nbn:se:kth:diva-238362 (URN)10.1007/978-3-319-94144-8_18 (DOI)2-s2.0-85049666666 (Scopus ID)9783319941431 (ISBN)
Conference
21st International Conference on Theory and Applications of Satisfiability Testing, SAT 2018 Held as Part of the Federated Logic Conference, FloC 2018, Oxford, United Kingdom, 9 July 2018 through 12 July 2018
Note

OC 20181812

Available from: 2018-11-12 Created: 2018-11-12 Last updated: 2018-11-12Bibliographically approved
Elffers, J., Giráldez-Cru, J., Nordström, J. & Vinyals, M. (2018). Using combinatorial benchmarks to probe the reasoning power of pseudo-boolean solvers. In: 21st International Conference on Theory and Applications of Satisfiability Testing, SAT 2018 Held as Part of the Federated Logic Conference, FloC 2018: . Paper presented at 21st International Conference on Theory and Applications of Satisfiability Testing, SAT 2018 Held as Part of the Federated Logic Conference, FloC 2018, Oxford, United Kingdom, 9 July 2018 through 12 July 2018 (pp. 75-93). Springer, 10929
Open this publication in new window or tab >>Using combinatorial benchmarks to probe the reasoning power of pseudo-boolean solvers
2018 (English)In: 21st International Conference on Theory and Applications of Satisfiability Testing, SAT 2018 Held as Part of the Federated Logic Conference, FloC 2018, Springer, 2018, Vol. 10929, p. 75-93Conference paper, Published paper (Refereed)
Abstract [en]

We study cdcl-cuttingplanes, Open-WBO, and Sat4j, three successful solvers from the Pseudo-Boolean Competition 2016, and evaluate them by performing experiments on crafted benchmarks designed to be trivial for the cutting planes (CP) proof system underlying pseudo-Boolean (PB) proof search but yet potentially tricky for PB solvers. Our experiments demonstrate severe shortcomings in state-of-the-art PB solving techniques. Although our benchmarks have linear-size tree-like CP proofs, and are thus extremely easy in theory, the solvers often perform quite badly even for very small instances. We believe this shows that solvers need to employ stronger rules of cutting planes reasoning. Even some instances that lack not only Boolean but also real-valued solutions are very hard in practice, which indicates that PB solvers need to get better not only at Boolean reasoning but also at linear programming. Taken together, our results point to several crucial challenges to be overcome in the quest for more efficient pseudo-Boolean solvers, and we expect that a further study of our benchmarks could shed more light on the potential and limitations of current state-of-the-art PB solving.

Place, publisher, year, edition, pages
Springer, 2018
Series
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ISSN 0302-9743 ; 10929
National Category
Other Engineering and Technologies not elsewhere specified
Identifiers
urn:nbn:se:kth:diva-238355 (URN)10.1007/978-3-319-94144-8_5 (DOI)2-s2.0-85049662965 (Scopus ID)9783319941431 (ISBN)
Conference
21st International Conference on Theory and Applications of Satisfiability Testing, SAT 2018 Held as Part of the Federated Logic Conference, FloC 2018, Oxford, United Kingdom, 9 July 2018 through 12 July 2018
Note

QC 20181108

Available from: 2018-11-08 Created: 2018-11-08 Last updated: 2018-11-08Bibliographically approved
Alwen, J., de Rezende, S. F., Nordström, J. & Vinyals, M. (2017). Cumulative Space in Black-White Pebbling and Resolution. In: Leibniz International Proceedings in Informatics, LIPIcs: . Paper presented at 8th Innovations in Theoretical Computer Science Conference (ITCS 2017), January 9-11, 2017, Berkeley, CA, USA. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Open this publication in new window or tab >>Cumulative Space in Black-White Pebbling and Resolution
2017 (English)In: Leibniz International Proceedings in Informatics, LIPIcs, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing , 2017Conference paper, Published paper (Refereed)
Abstract [en]

We study space complexity and time-space trade-offs with a focus not on peak memory usage but on overall memory consumption throughout the computation. Such a cumulative space measure was introduced for the computational model of parallel black pebbling by [Alwen and Serbinenko 2015] as a tool for obtaining results in cryptography. We consider instead the nondeterministic black-white pebble game and prove optimal cumulative space lower bounds and trade-offs, where in order to minimize pebbling time the space has to remain large during a significant fraction of the pebbling. We also initiate the study of cumulative space in proof complexity, an area where other space complexity measures have been extensively studied during the last 10-15 years. Using and extending the connection between proof complexity and pebble games in [Ben-Sasson and Nordström 2008, 2011], we obtain several strong cumulative space results for (even parallel versions of) the resolution proof system, and outline some possible future directions of study of this, in our opinion, natural and interesting space measure.

Place, publisher, year, edition, pages
Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2017
Keywords
Clause Space, Cumulative Space, Parallel Resolution, Pebble Game, Pebbling, Proof Complexity, Resolution, Space, Commerce, Optical resolving power, Economic and social effects
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-206582 (URN)10.4230/LIPIcs.ITCS.2017.38 (DOI)2-s2.0-85034241142 (Scopus ID)9783959770293 (ISBN)
Conference
8th Innovations in Theoretical Computer Science Conference (ITCS 2017), January 9-11, 2017, Berkeley, CA, USA
Note

QC 20170509

Available from: 2017-05-05 Created: 2017-05-05 Last updated: 2019-05-29Bibliographically approved
Atserias, A., Lauria, M. & Nordström, J. (2016). Narrow Proofs May Be Maximally Long. ACM Transactions on Computational Logic, 17(3), Article ID 19.
Open this publication in new window or tab >>Narrow Proofs May Be Maximally Long
2016 (English)In: ACM Transactions on Computational Logic, ISSN 1529-3785, E-ISSN 1557-945X, Vol. 17, no 3, article id 19Article in journal (Refereed) Published
Abstract [en]

We prove that there are 3-CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size n(Omega(w)). This shows that the simple counting argument that any formula refutable in width w must have a proof in size n(O(w)) is essentially tight. Moreover, our lower bound generalizes to polynomial calculus resolution and Sherali-Adams, implying that the corresponding size upper bounds in terms of degree and rank are tight as well. The lower bound does not extend all the way to Lasserre, however, since we show that there the formulas we study have proofs of constant rank and size polynomial in both n and w.

Place, publisher, year, edition, pages
Association for Computing Machinery (ACM), 2016
Keywords
Proof complexity, resolution, width, polynomial calculus, polynomial calculus resolution, PCR, Sherali-Adams, SAR, degree
National Category
Other Computer and Information Science
Identifiers
urn:nbn:se:kth:diva-191754 (URN)10.1145/2898435 (DOI)000380019200005 ()2-s2.0-84973879640 (Scopus ID)
External cooperation:
Funder
Swedish Research Council, 621-2010-4797 621-2012-5645EU, FP7, Seventh Framework Programme, 279611
Note

QC 20160902

Available from: 2016-09-02 Created: 2016-09-02 Last updated: 2018-01-10Bibliographically approved
Berkholz, C. & Nordström, J. (2016). Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler-Leman Refinement Steps. In: PROCEEDINGS OF THE 31ST ANNUAL ACM-IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2016): . Paper presented at 31st Annual ACM-IEEE Symposium on Logic in Computer Science (LICS), JUL 05-08, 2016, New York City, NY (pp. 267-276). Institute of Electrical and Electronics Engineers (IEEE)
Open this publication in new window or tab >>Near-Optimal Lower Bounds on Quantifier Depth and Weisfeiler-Leman Refinement Steps
2016 (English)In: PROCEEDINGS OF THE 31ST ANNUAL ACM-IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2016), Institute of Electrical and Electronics Engineers (IEEE), 2016, p. 267-276Conference paper, Published paper (Refereed)
Abstract [en]

We prove near-optimal trade-offs for quantifier depth versus number of variables in first-order logic by exhibiting pairs of n-element structures that can be distinguished by a k-variable first-order sentence but where every such sentence requires quantifier depth at least n(Omega(k/logk)). Our trade-offs also apply to first-order counting logic, and by the known connection to the k-dimensional Weisfeiler-Leman algorithm imply near-optimal lower bounds on the number of refinement iterations. A key component in our proof is the hardness condensation technique recently introduced by [Razborov ' 16] in the context of proof complexity. We apply this method to reduce the domain size of relational structures while maintaining the quantifier depth required to distinguish them.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE), 2016
Keywords
First-order logic, first-order counting logic, bounded variable fragment, quantifier depth, Weisfeiler-Leman, refinement iterations, lower bounds, trade-offs, hardness condensation, XORification
National Category
Computer Systems
Identifiers
urn:nbn:se:kth:diva-197841 (URN)10.1145/2933575.2934560 (DOI)000387609200027 ()2-s2.0-84994626925 (Scopus ID)978-1-4503-4391-6 (ISBN)
Conference
31st Annual ACM-IEEE Symposium on Logic in Computer Science (LICS), JUL 05-08, 2016, New York City, NY
Note

QC 20161222

Available from: 2016-12-22 Created: 2016-12-08 Last updated: 2016-12-22Bibliographically approved
Berkholz, C. & Nordström, J. (2016). Supercritical space-width trade-offs for resolution. In: Leibniz International Proceedings in Informatics, LIPIcs: . Paper presented at 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, 12 July 2016 through 15 July 2016. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Open this publication in new window or tab >>Supercritical space-width trade-offs for resolution
2016 (English)In: Leibniz International Proceedings in Informatics, LIPIcs, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing , 2016Conference paper, Published paper (Refereed)
Abstract [en]

We show that there are CNF formulas which can be refuted in resolution in both small space and small width, but for which any small-width resolution proof must have space exceeding by far the linear worst-case upper bound. This significantly strengthens the space-width trade-offs in [Ben- Sasson 2009], and provides one more example of trade-offs in the "supercritical" regime above worst case recently identified by [Razborov 2016]. We obtain our results by using Razborov's new hardness condensation technique and combining it with the space lower bounds in [Ben-Sasson and Nordström 2008].

Place, publisher, year, edition, pages
Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2016
Keywords
Proof complexity, Resolution, Space, Supercritical, Trade-offs, Width, Automata theory, Commerce, Optical resolving power, Trade off, Economic and social effects
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:kth:diva-207495 (URN)10.4230/LIPIcs.ICALP.2016.57 (DOI)2-s2.0-85012892631 (Scopus ID)9783959770132 (ISBN)
Conference
43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, 12 July 2016 through 15 July 2016
Note

Conference code: 123446; Export Date: 22 May 2017; Conference Paper; Funding details: DAAD, Deutscher Akademischer Austauschdienst; Funding details: 279611, ERC, European Research Council; Funding text: Part of the work of the first author was performed while at KTH Royal Institute of Technology supported by a fellowship within the Postdoc-Programme of the German Academic Exchange Service (DAAD). The research of the second author was supported by the European Research Council under the European Union's Seventh Framework Programme (FP7/2007-2013) / ERC grant agreement no. 279611 and by Swedish Research Council grants 621-2010-4797 and 621-2012-5645. QC 20170607

Available from: 2017-06-07 Created: 2017-06-07 Last updated: 2018-01-13Bibliographically approved
Elffers, J., Johannsen, J., Lauria, M., Magnard, T., Nordström, J. & Vinyals, M. (2016). Trade-offs between time and memory in a tighter model of CDCL SAT solvers. In: 19th International Conference on Theory and Applications of Satisfiability Testing, SAT 2016: . Paper presented at 5 July 2016 through 8 July 2016 (pp. 160-176). Springer
Open this publication in new window or tab >>Trade-offs between time and memory in a tighter model of CDCL SAT solvers
Show others...
2016 (English)In: 19th International Conference on Theory and Applications of Satisfiability Testing, SAT 2016, Springer, 2016, p. 160-176Conference paper, Published paper (Refereed)
Abstract [en]

A long line of research has studied the power of conflict- driven clause learning (CDCL) and how it compares to the resolution proof system in which it searches for proofs. It has been shown that CDCL can polynomially simulate resolution even with an adversarially chosen learning scheme as long as it is asserting. However, the simulation only works under the assumption that no learned clauses are ever forgot- ten, and the polynomial blow-up is significant. Moreover, the simulation requires very frequent restarts, whereas the power of CDCL with less frequent or entirely without restarts remains poorly understood. With a view towards obtaining results with tighter relations between CDCL and resolution, we introduce a more fine-grained model of CDCL that cap- tures not only time but also memory usage and number of restarts. We show how previously established strong size-space trade-offs for resolution can be transformed into equally strong trade-offs between time and memory usage for CDCL, where the upper bounds hold for CDCL with- out any restarts using the standard 1UIP clause learning scheme, and the (in some cases tightly matching) lower bounds hold for arbitrarily frequent restarts and arbitrary clause learning schemes.

Place, publisher, year, edition, pages
Springer, 2016
Keywords
Commerce, Formal logic, Clause learning, Fine grained, Learning schemes, Lower bounds, Memory usage, Resolution proofs, SAT solvers, Upper Bound, Economic and social effects
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-195488 (URN)10.1007/978-3-319-40970-2_11 (DOI)000387430600011 ()2-s2.0-84977484096 (Scopus ID)9783319409696 (ISBN)
Conference
5 July 2016 through 8 July 2016
Note

QC 20161118

Available from: 2016-11-18 Created: 2016-11-03 Last updated: 2018-01-13Bibliographically approved
Mikša, M. & Nordström, J. (2015). A generalized method for proving polynomial calculus degree lower bounds. In: Leibniz International Proceedings in Informatics, LIPIcs: . Paper presented at 30th Conference on Computational Complexity, CCC 2015; Portland; United States (pp. 467-487). Dagstuhl Publishing, 33
Open this publication in new window or tab >>A generalized method for proving polynomial calculus degree lower bounds
2015 (English)In: Leibniz International Proceedings in Informatics, LIPIcs, Dagstuhl Publishing , 2015, Vol. 33, p. 467-487Conference paper, Published paper (Refereed)
Abstract [en]

We study the problem of obtaining lower bounds for polynomial calculus (PC) and polynomial calculus resolution (PCR) on proof degree, and hence by [Impagliazzo et al. ’99] also on proof size. [Alekhnovich and Razborov’03] established that if the clause-variable incidence graph of a CNF formula F is a good enough expander, then proving that F is unsatisfiable requires high PC/PCR degree. We further develop the techniques in [AR03] to show that if one can "cluster" clauses and variables in a way that "respects the structure" of the formula in a certain sense, then it is sufficient that the incidence graph of this clustered version is an expander. As a corollary of this, we prove that the functional pigeonhole principle (FPHP) formulas require high PC/PCR degree when restricted to constant-degree expander graphs. This answers an open question in [Razborov’02], and also implies that the standard CNF encoding of the FPHP formulas require exponential proof size in polynomial calculus resolution. Thus, while Onto-FPHP formulas are easy for polynomial calculus, as shown in [Riis’93], both FPHP and Onto-PHP formulas are hard even when restricted to bounded-degree expanders.

Place, publisher, year, edition, pages
Dagstuhl Publishing, 2015
Keywords
Degree, Functional pigeonhole principle, Lower bound, PCR, Polynomial calculus, Polynomial calculus resolution, Proof complexity, Size
National Category
Mathematical Analysis
Identifiers
urn:nbn:se:kth:diva-187389 (URN)10.4230/LIPIcs.CCC.2015.467 (DOI)2-s2.0-84958256296 (Scopus ID)978-393989781-1 (ISBN)
Conference
30th Conference on Computational Complexity, CCC 2015; Portland; United States
Note

QC 20160527

Available from: 2016-05-27 Created: 2016-05-23 Last updated: 2016-11-30Bibliographically approved
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0002-2700-4285

Search in DiVA

Show all publications