Graphic summary
  • Show / hide key
  • Information


Scientific and technological production
  •  

1 to 50 of 76 results
  • Improved separations of regular resolution from clause learning proof systems

     Bonet Carbonell, M. Luisa; Buss, Sam; Johannsen, Jan
    Journal of artificial intelligence research
    num. 49, p. 669-703
    Date of publication: 2014-04-01
    Journal article

    Read the abstract Read the abstract View View Open in new window  Share Reference managers Reference managers Open in new window

    This paper studies the relationship between resolution and conflict driven clause learning (CDCL) without restarts, and refutes some conjectured possible separations. We prove that the guarded, xor-ified pebbling tautology clauses, which Urquhart proved are hard for regular resolution, as well as the guarded graph tautology clauses of Alekhnovich, Johannsen, Pitassi, and Urquhart have polynomial size pool resolution refutations that use only input lemmas as learned clauses. For the latter set of clauses, we extend this to prove that a CDCL search without restarts can refute these clauses in polynomial time, provided it makes the right choices for decision literals and clause learning. This holds even if the CDCL search is required to greedily process conflicts arising from unit propagation. This refutes the conjecture that the guarded graph tautology clauses or the guarded xor-ified pebbling tautology clauses can be used to separate CDCL without restarts from general resolution. Together with subsequent results by Buss and Kolodziejczyk, this means we lack any good conjectures about how to establish the exact logical strength of conflict-driven clause learning without restarts.

  • Resolution procedures for multiple-valued optimization

     Ansótegui Gil, Carlos; Bonet Carbonell, M. Luisa; Manyí, Felip; Levy Diaz, Jordi
    Information sciences
    Vol. 227, p. 43-59
    DOI: 10.1016/j.ins.2012.12.004
    Date of publication: 2013-04-01
    Journal article

    Read the abstract Read the abstract View View Open in new window  Share Reference managers Reference managers Open in new window

    Signed clausal forms offer a suitable logical framework for automated reasoning in multiple-valued logics. It turns out that the satisfiability problem of any finitely-valued propositional logic, as well as of certain infinitely-valued logics, can be easily reduced, in polynomial time, to the satisfiability problem of signed clausal forms. On the other hand, signed clausal forms are a powerful knowledge representation language for constraint programming, and have shown to be a practical and competitive approach to solving combinatorial decision problems. Motivated by the existing theoretical and practical results for the satisfiability problem of signed clausal forms, as well as by the recent logical and algorithmic results on the Boolean maximum satisfiability problem, in this paper we investigate the maximum satisfiability problem of propositional signed clausal forms from the logical and practical points of view.

  • SAT-based MaxSAT algorithms

     Ansótegui Gil, Carlos; Bonet Carbonell, M. Luisa; Levy Diaz, Jordi
    Artificial intelligence
    Vol. 196, p. 77-105
    DOI: 10.1016/j.artint.2013.01.002
    Date of publication: 2013-03
    Journal article

    View View Open in new window  Share Reference managers Reference managers Open in new window

  • Improving WPM2 for (weighted) partial MaxSAT

     Ansótegui Gil, Carlos; Bonet Carbonell, M. Luisa; Gabàs, Joel; Levy Diaz, Jordi
    International Conference on Principles and Practice of Constraint Programming
    p. 117-132
    DOI: 10.1007/978-3-642-40627-0_12
    Presentation's date: 2013-09-16
    Presentation of work at congresses

    Read the abstract Read the abstract View View Open in new window  Share Reference managers Reference managers Open in new window

    Weighted Partial MaxSAT (WPMS) is an optimization variant of the Satisfiability (SAT) problem. Several combinatorial optimization problems can be translated into WPMS. In this paper we extend the state-of-the-art WPM2 algorithm by adding several improvements, and implement it on top of an SMT solver. In particular, we show that by focusing search on solving to optimality subformulas of the original WPMS instance we increase the efficiency of WPM2. From the experimental evaluation we conducted on the PMS and WPMS instances at the 2012 MaxSAT Evaluation, we can conclude that the new approach is both the best performing for industrial instances, and for the union of industrial and crafted instances.

  • An improved separation of regular resolution from pool resolution and clause learning (extended abstract).

     Bonet Carbonell, M. Luisa; Buss, Sam
    International Joint Conference on Artificial Intelligence
    p. 2972-2976
    Presentation's date: 2013-08-09
    Presentation of work at congresses

    Read the abstract Read the abstract View View Open in new window  Share Reference managers Reference managers Open in new window

    We establish the unexpected power of conflict driven clause learning (CDCL) proof search by proving that the sets of unsatisfiable clauses ob- tained from the guarded graph tautology principles of Alekhnovich, Johannsen, Pitassi and Urquhart have polynomial size pool resolution refutations that use only input lemmas as learned clauses. We further show that, under the correct heuris- tic choices, these refutations can be carried out in polynomial time by CDCL proof search with- out restarts, even when restricted to greedy, unit- propagating search. The guarded graph tautologies had been conjectured to separate CDCL without restarts from resolution; our results refute this con- jecture

  • The complexity of finding multiple solutions to betweenness and quartet compatibility

     Bonet Carbonell, M. Luisa; Linz, Simone; St. John, Katherine
    IEEE-ACM transactions on computational biology and bioinformatics
    Vol. 9, num. 1, p. 273-285
    DOI: 10.1109/TCBB.2011.108
    Date of publication: 2012-02
    Journal article

    View View Open in new window  Share Reference managers Reference managers Open in new window

  • Improving SAT-based Weighted MaxSAT solvers

     Ansótegui Gil, Carlos; Bonet Carbonell, M. Luisa; Cabàs, Joel; Levy Diaz, Jordi
    International Conference on Principles and Practice of Constraint Programming
    p. 86-101
    DOI: 10.1007/978-3-642-33558-7_9
    Presentation of work at congresses

    View View Open in new window  Share Reference managers Reference managers Open in new window

  • An improved separation of regular resolution from pool resolution and clause learning

     Bonet Carbonell, M. Luisa; Buss, Sam
    International Conference on Theory and Applications of Satisfiability Testing
    p. 44-57
    DOI: 10.1007/978-3-642-31612-8_5
    Presentation of work at congresses

    View View Open in new window  Share Reference managers Reference managers Open in new window

  • Analysis and generation of pseudo-industrial MaxSAT instances

     Ansótegui Gil, Carlos; Bonet Carbonell, M. Luisa; Li, Chu Min; Levy Diaz, Jordi
    International Conference of the Catalan Association for Artificial Intelligence
    p. 173-184
    DOI: 10.3233/978-1-61499-139-7-173
    Presentation's date: 2012
    Presentation of work at congresses

    View View Open in new window  Share Reference managers Reference managers Open in new window

  • TASSAT- Teoría, aplicaciones y sinergia en SAT, CSP y FDL

     Bonet Carbonell, M. Luisa; Esteban Angeles, Juan Luis; Maneva, Elitza; Atserias Peri, Albert
    Competitive project

     Share

  • A new algorithm for Weighted Partial MaxSAT

     Ansótegui Gil, Carlos; Bonet Carbonell, M. Luisa; Levy Diaz, Jordi
    AAAI Conference on Artificial Intelligence
    p. 3-8
    Presentation of work at congresses

    Read the abstract Read the abstract View View Open in new window  Share Reference managers Reference managers Open in new window

    We present and implement a Weighted Partial MaxSAT solver based on successive calls to a SAT solver. We prove the correctness of our algorithm and compare our solver with other Weighted Partial MaxSAT solvers.

  • On the complexity of uSPR distance

     Bonet Carbonell, M. Luisa; John, Katherine St.
    IEEE-ACM transactions on computational biology and bioinformatics
    Vol. 7, num. 3, p. 572-576
    DOI: 10.1109/TCBB.2008.132
    Date of publication: 2010-09
    Journal article

    View View Open in new window  Share Reference managers Reference managers Open in new window

  • Access to the full text
    Efficiently calculating evolutionary tree measures using SAT  Open access

     Bonet Carbonell, M. Luisa; John, Katherine St.
    Lecture notes in computer science
    Vol. 5584, p. 4-17
    DOI: 10.1007/978-3-642-02777-2
    Date of publication: 2009
    Journal article

    Read the abstract Read the abstract Access to the full text Access to the full text Open in new window  Share Reference managers Reference managers Open in new window

    We develop techniques to calculate important measures in evolutionary biology by encoding to CNF formulas and using powerful SAT solvers. Comparing evolutionary trees is a necessary step in tree reconstruction algorithms, locating recombination and lateral gene transfer, and in analyzing and visualizing sets of trees. We focus on two popular comparison measures for trees: the hybridization number and the rooted subtree-prune-and-regraft (rSPR) distance. Both have recently been shown to be NP-hard, and effcient algorithms are needed to compute and approximate these measures. We encode these as a Boolean formula such that two trees have hybridization number k (or rSPR distance k) if and only if the corresponding formula is satisfiable. We use state-of-the-art SAT solvers to determine if the formula encoding the measure has a satisfying assignment. Our encoding also provides a rich source of real-world SAT instances, and we include a comparison of several recent solvers (minisat, adaptg2wsat, novelty+p, Walksat, March KS and SATzilla).

    Postprint (author’s final draft)

  • Towards industrial-like random SAT instances

     Bonet Carbonell, M. Luisa; Levy Diaz, Jordi; Ansótegui Gil, Carlos
    International Joint Conference on Artificial Intelligence
    p. 387-392
    Presentation's date: 2009-07
    Presentation of work at congresses

    Read the abstract Read the abstract View View Open in new window  Share Reference managers Reference managers Open in new window

    We focus on the random generation of SAT instances that have computational properties that are similar to real-world instances. It is known that industrial instances, even with a great number of variables, can be solved by a clever solver in a reasonable amount of time. This is not possible, in general, with classical randomly generated instances. We provide different generation models of SAT instances, extending the uniform and regular 3-CNF models. They are based on the use of non-uniform probability distributions to select variables. Our last model also uses a mechanism to produce clauses of different lengths as in industrial instances. We show the existence of the phase transition phenomena for our models and we study the hardness of the generated instances as a function of the parameters of the probability distributions. We prove that, with these parameters we can adjust the difficulty of the problems in the phase transition point. We measure hardness in terms of the performance of different solvers. We show how these models will allow us to generate random instances similar to industrial instances, of interest for testing purposes.

  • Solving (weighted) partial MaxSAT through satisfiability testing

     Ansótegui Gil, Carlos; Bonet Carbonell, M. Luisa; Levy Diaz, Jordi
    International Conference on Theory and Applications of Satisfiability Testing
    p. 427-440
    DOI: 10.1007/978-3-642-02777-2_39
    Presentation's date: 2009-07
    Presentation of work at congresses

    View View Open in new window  Share Reference managers Reference managers Open in new window

  • On solving MaxSAT through SAT

     Ansótegui Gil, Carlos; Bonet Carbonell, M. Luisa; Levy Diaz, Jordi
    International Conference of the Catalan Association for Artificial Intelligence
    p. 284-292
    Presentation's date: 2009-10-21
    Presentation of work at congresses

    View View Open in new window  Share Reference managers Reference managers Open in new window

  • On the structure of industrial SAT instances

     Ansótegui Gil, Carlos; Bonet Carbonell, M. Luisa; Levy Diaz, Jordi
    Principles and Practice of Constraint Programming
    p. 127-141
    DOI: 10.1007/978-3-642-04244-7_13
    Presentation's date: 2009-09
    Presentation of work at congresses

    View View Open in new window  Share Reference managers Reference managers Open in new window

  • Efficiently calculating evolutionary tree measures using SAT

     Bonet Carbonell, M. Luisa; St. John, Katherine
    International Conference on Theory and Applications of Satisfiability Testing
    p. 4-17
    DOI: 10.1007/978-3-642-02777-2_3
    Presentation's date: 2009-06-30
    Presentation of work at congresses

    View View Open in new window  Share Reference managers Reference managers Open in new window

  • Lógica Multivaluada: Fundamentos y Aplicaciones a la Satisfactibilidad y la Satisfacción de Restricciones (MULOG-2)

     Esteban Angeles, Juan Luis; Bonet Carbonell, M. Luisa; Lozano Bojados, Antoni; Atserias Peri, Albert; Dalmau Lloret, Victor
    Competitive project

     Share

  • Measuring the Hardness of SAT Instances

     Ansótegui Gil, Carlos; María, Luisa Bonet; Bonet Carbonell, M. Luisa; Levy Diaz, Jordi; Manyí, Felip
    Twenty-third AAAI Conference on Artificial Intelligence
    p. 222-228
    Presentation of work at congresses

     Share Reference managers Reference managers Open in new window

  • Resolution for Max-SAT

     Bonet Carbonell, M. Luisa; Levy Diaz, Jordi; Manyí, Felip
    Artificial intelligence
    Vol. 171, num. 8-9, p. 606-618
    Date of publication: 2007-06
    Journal article

     Share Reference managers Reference managers Open in new window

  • Mapping CSP into Many-Valued SAT

     Ansótegui Gil, Carlos; Maria, Luisa Bonet; Bonet Carbonell, M. Luisa; Levy Diaz, Jordi; Manyí, Felip
    Lecture notes in computer science
    Vol. 4501, p. 10-15
    Date of publication: 2007-05
    Journal article

     Share Reference managers Reference managers Open in new window

  • Resolution for Max-SAT

     Ansótegui Gil, Carlos; Maria, Luisa Bonet; Bonet Carbonell, M. Luisa; Levy Diaz, Jordi; Manyí, Felip
    22nd AAAI conference on Artificial Intelligence
    p. 167-172
    Presentation of work at congresses

     Share Reference managers Reference managers Open in new window

  • Mapping CSP into Many-Valued SAT

     Bonet Carbonell, M. Luisa
    Theory and Applications of Satisfiability Testing - SAT 2007, 10th International Conference
    p. 10-15
    Presentation of work at congresses

     Share Reference managers Reference managers Open in new window

  • A Complete Resolution Calculus for Signed Max-SAT

     Bonet Carbonell, M. Luisa
    37th International Symposium on Multiple-Valued Logic
    p. 22
    Presentation of work at congresses

     Share Reference managers Reference managers Open in new window

  • The Logic Behind Weighted CSP

     Ansótegui Gil, Carlos; Maria, Luisa Bonet; Bonet Carbonell, M. Luisa; Levy Diaz, Jordi; Manyí, Felip
    20th International Joint Conference on Artificial Intelligence
    p. 32-37
    Presentation of work at congresses

     Share Reference managers Reference managers Open in new window

  • A Complete Calculus for Max-SAT

     Maria, Luisa Bonet; Bonet Carbonell, M. Luisa; Levy Diaz, Jordi; Manyí, Felip
    Lecture notes in computer science
    Vol. 4121, p. 240-251
    Date of publication: 2006-08
    Journal article

     Share Reference managers Reference managers Open in new window

  • Approximating Subtree Distances Between Phylogenies

     Maria, Luisa Bonet; Bonet Carbonell, M. Luisa; Katherine, Stjohn; Mahindru, Ruchi; Amenta, Nina
    Journal of computational biology
    Vol. 13, num. 8, p. 1419-1434
    Date of publication: 2006-10
    Journal article

     Share Reference managers Reference managers Open in new window

  • Deducción Automática y Satisfactibilidad (IDEAS)

     Atserias Peri, Albert; Bonet Carbonell, M. Luisa
    Competitive project

     Share

  • On the automatizability of resolution and related propositional proof systems

     Atserias Peri, Albert; Bonet Carbonell, M. Luisa
    Information and computation
    Vol. 189, p. 182-201
    Date of publication: 2004-01
    Journal article

     Share Reference managers Reference managers Open in new window

  • Non-Automatizability of Bounded-Depth Frege Proofs

     Bonet Carbonell, M. Luisa; Domingo, Carlos; Gavaldà Mestre, Ricard; Maciel, Alexis; Pitassi, Toniann
    Computational complexity
    Vol. 13, num. 1-2, p. 47-68
    Date of publication: 2004-12
    Journal article

     Share Reference managers Reference managers Open in new window

  • Complexity mesures for resolution  Open access

     Esteban Angeles, Juan Luis
    Department of Computer Science, Universitat Politècnica de Catalunya
    Theses

    Read the abstract Read the abstract Access to the full text Access to the full text Open in new window  Share Reference managers Reference managers Open in new window

    Esta obra es una contribución al campo de la Complejidad de la Demostración, que estudia la complejidad de los sistemas de demostración en términos de los recursos necesarios para demostrar o refutar fórmulas proposicionales. La Complejidad de la Demostración es un interesante campo relacionado con otros campos de la Informática como la Complejidad Computacional o la Demostración Automática entre otros. Esta obra se centra en medidas de complejidad para sistemas de demostración refutacionales para fórmulas en FNC. Consideramos varios sistemas de demostración, concretamente Resolución, R(k) y Planos Secantes y nuestros resultados hacen referencia a las medidas de complejidad de tamaño y espacio.Mejoramos separaciones de tamaño anteriores entre las versiones generales y arbóreas de Resolución y Planos Secantes. Para hacerlo, extendemos una cota inferior de tamaño para circuitos monótonos booleanos de Ran y McKenzie a circuitos monótonos reales. Este tipo de separaciones es interesante porque algunos demostradores automáticos se basan en la versión arbórea de sistemas de demostración, por tanto la separación indica que no es siempre una buena idea restringirnos a la versión arbórea.Tras la reciente aparición de R(k), que es un sistema de demostración entre Resolución y Frege con profundidad acotada, era importante estudiar cuan potente es y su relación con otros sistemas de demostración. Resolvemos un problema abierto propuesto por Krajícek, concretamente mostramos que R(2) no tiene la propiedad de la interpolación monónota factible. Para hacerlo, mostramos que R(2) es estrictamente más potente que Resolución.Una pregunta natural es averiguar si se pueden separar sucesivos niveles de R(k) o R(k) arbóreo. Mostramos separaciones exponenciales entre niveles sucesivos de lo que podemos llamar la jerarquía R(k) arbórea. Esto significa que hay formulas que requieren refutaciones de tamaño exponencial en R(k) arbóreo, pero tienen refutaciones de tamaño polinómico en R(k+1) arbóreo. Propusimos una nueva definición de espacio para Resolución mejorando la anterior de Kleine-Büning y Lettmann. Dimos resultados generales sobre el espacio para Resolución y Resolución arbórea y también una caracterización combinatoria del espacio para Resolución arbórea usando un juego con dos adversarios para fórmulas en FNC. La caracterización permite demostrar cotas inferiores de espacio para la Resolución arbórea sin necesidad de usar el concepto de Resolución o Resolución arbórea. Durante mucho tiempo no se supo si el espacio para Resolución y Resolución arbórea coincidían o no. Hemos demostrado que no coinciden al haber dado la primera separación entre el espacio para Resolución y Resolución arbórea.También hemos estudiado el espacio para R(k). Demostramos que al igual que pasaba con el tamaño, R(k) arbóreo también forma una jerarquía respecto alespacio. Por tanto, hay fórmulas que necesitan espacio casi lineal en R(k) arbóreo mientras que tienen refutaciones en R(k+1) arbóreo con espacio contante. Extendemos todas las cotas inferiores de espacio para Resolución conocidas a R(k) de una forma sencilla y unificada, que también sirve para Resolución, usando el concepto de satisfactibilidad dinámica presentado en esta obra.

    This work is a contribution to the field of Proof Complexity, which studies the complexity of proof systems in terms of the resources needed to prove or refute propositional formulas. Proof Complexity is an interesting field which has several connections to other fields of Computer Science like Computational Complexity or Automatic Theorem Proving among others. This work focuses in complexity measures for refutational proof systems for CNF formulas. We consider several proof systems, namely Resolution, R(k) and Cutting Planes and our results concern mainly to the size and space complexity measures. We improve previous size separations between treelike and general versions of Resolution and Cutting Planes. To do so we extend a size lower bound for monotone boolean circuits by Raz and McKenzie, to monotone real circuits. This kind of separations is interesting because some automated theorem provers rely on the treelike version of proof systems, so the separations show that is not always a good idea to restrict to the treelike version. After the recent apparition of R(k) which is a proof system lying between Resolution and bounded-depth Frege it was important to study how powerful it is and its relation with other proof systems. We solve an open problem posed by Krajícek, namely we show that R(2) does not have the feasible monotone interpolation property. To do so, we show that R(2) is strictly more powerful than Resolution. A natural question is to find out whether we can separate successive levels of R(k) or treelike R(k). We show exponential separations between successive levels of what we can call now the treelike R(k) hierarchy. That means that there are formulas that require exponential size treelike R(k) refutations whereas they have polynomial size treelike R(k+1) refutations. We have proposed a new definition for Resolution space improving a previous one from Kleine-Büning and Lettmann. We give general results for Resolution and treelike Resolution space and also a combinatorial characterization of treelike Resolution space via a Player-Adversary game over CNF formulas. The characterization allows to prove lower bounds for treelike Resolution space with no need to use the concept of Resolution or Resolution refutations at all. For a long time it was not known whether Resolution space and treelike Resolution space coincided or not. We have answered this question in the negative because we give the first space separation from Resolution to treelike Resolution. We have also studied space for R(k). We show that, as happened with respect to size, treelike R(k) forms a hierarchy respect to space. So, there are formulas that require nearly linear space for treelike R(k) whereas they have constant space treelike R(k+1) refutations. We extend all known Resolution space lower bounds to R(k) in an easier and unified way, that also holds for Resolution, using the concept of dynamical satisfiability introduced in this work.

  • Lower bounds for the weak pigeonhole principle and random formulas beyond resolution

     Atserias Peri, Albert; Bonet Carbonell, M. Luisa; Esteban Angeles, Juan Luis
    Information and computation
    Vol. 176, num. 2, p. 136-152
    Date of publication: 2002-08
    Journal article

     Share Reference managers Reference managers Open in new window

  • The complexity of resource-bounded propositional proofs  awarded activity

     Atserias Peri, Albert
    Department of Computer Science, Universitat Politècnica de Catalunya
    Theses

     Share Reference managers Reference managers Open in new window

  • On the automatizability of Resolution and related propositional proof systems

     Atserias Peri, Albert; Bonet Carbonell, M. Luisa
    Annual Conference of the European Association for Computer Science Logic
    p. 569-583
    DOI: 10.1007/3-540-45793-3_38
    Presentation's date: 2002
    Presentation of work at congresses

    View View Open in new window  Share Reference managers Reference managers Open in new window

  • Optimality of size-width tradeoffs fro resolution

     Maria, Luisa Bonet; Bonet Carbonell, M. Luisa; Galesi, Nicola
    Computational complexity
    Vol. 10, num. 4, p. 261-276
    Date of publication: 2001-12
    Journal article

     Share Reference managers Reference managers Open in new window

  • Lower bounds for the Weak Pigeonhole Principle beyond Resolution

     Atserias Peri, Albert; Bonet Carbonell, M. Luisa; Esteban Angeles, Juan Luis
    International Colloquium on Automata, Languages and Programming
    p. 1005-1016
    DOI: 10.1007/3-540-48224-5_81
    Presentation's date: 2001
    Presentation of work at congresses

    View View Open in new window  Share Reference managers Reference managers Open in new window

  • On the Relative Complexity of Resolution Refinements and Cutting Planes proof Systems

     Bonet Carbonell, M. Luisa; Esteban Angeles, Juan Luis; Galesi, Nicola; Johannsen, J
    SIAM journal on computing
    Vol. 30, num. 5, p. 1462-1484
    Date of publication: 2000-05
    Journal article

     Share Reference managers Reference managers Open in new window

  • On Interpolation and Automatization for Frege Proof Systems

     Bonet Carbonell, M. Luisa; Pitassi, T; Raz, R
    SIAM journal on computing
    Vol. 29, num. 6, p. 1939-1967
    Date of publication: 2000-01
    Journal article

     Share Reference managers Reference managers Open in new window

  • On the complexity of propositional proof systems

     Galesi, Nicola
    Department of Computer Science, Universitat Politècnica de Catalunya
    Theses

     Share Reference managers Reference managers Open in new window

  • The Width-size Method for General Resolution is Optimal

     Bonet Carbonell, M. Luisa; Galesi, Nicola
    Date: 1999-02
    Report

     Share Reference managers Reference managers Open in new window

  • Constructing Evolutionary Trees in the Presence of Polymorphic Characters

     Bonet Carbonell, M. Luisa; Phillips, Cynthia; Warnow, Tandy; Yooseph, Shibu
    SIAM journal on computing
    Vol. 29, num. 1, p. 103-131
    Date of publication: 1999-01
    Journal article

     Share Reference managers Reference managers Open in new window

  • Non-automatizability of bounded-depth Frege proofs

     Bonet Carbonell, M. Luisa; Domingo, Carlos; Gavaldà Mestre, Ricard; Maciel, Alexis; Pitassi, Toniann
    14th. Annual IEEE Conference on Computational Complexity
    p. 15-23
    Presentation of work at congresses

     Share Reference managers Reference managers Open in new window

  • Non-automatizability of bounded-depth Frege proofs

     Bonet Carbonell, M. Luisa
    14th. Annual IEEE Conference on Computational Complexity
    Presentation's date: 1999-05-04
    Presentation of work at congresses

     Share Reference managers Reference managers Open in new window

  • A Study of Proof Search Algorithms for Resolution and Polynomial Calculus

     Bonet Carbonell, M. Luisa; Galesi, Nicola
    40th Annual Symposium on Foundations of Computer Science
    p. 422-431
    Presentation of work at congresses

     Share Reference managers Reference managers Open in new window

  • Exponential Separations between Restricted Resolution and Cutting Planes proof systems

     Bonet Carbonell, M. Luisa; Galesi, Nicola; Esteban Angeles, Juan Luis
    Electronic colloquium on computational complexity
    num. TR98-035, p. 1-15
    Date of publication: 1998-06
    Journal article

     Share Reference managers Reference managers Open in new window

  • Bether Methods for Solving Parsimony and Compatibility

     Bonet Carbonell, M. Luisa; Steel, M; Warnow, T; Yooseph, S
    Journal of computational biology
    Vol. 5, num. 3, p. 391-407
    Date of publication: 1998-12
    Journal article

     Share Reference managers Reference managers Open in new window