Now showing items 1-10 of 10

  • A new algorithm for Weighted Partial MaxSAT 

    Ansótegui, Carlos; Bonet Carbonell, M. Luisa; Levy Díaz, Jordi (2011)
    Conference report
    Restricted access - publisher's policy
    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.
  • Efficiently calculating evolutionary tree measures using SAT 

    Bonet Carbonell, M. Luisa; John, Katherine St. (2009)
    Article
    Open Access
    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, ...
  • Exponential separation between tree-like and dag-like Cutting Planes proof systems 

    Bonet Carbonell, M. Luisa; Esteban Ángeles, Juan Luis; Galesi, Nicola; Johannsen, Jan (1997-12)
    External research report
    Open Access
    We prove an exponential lower bound for tree-like Cutting Planes refutations of a set of clauses which has polynomial size resolution refutations. This implies an exponential separation between tree-like and dag-like ...
  • Improving WPM2 for (weighted) partial MaxSAT 

    Ansótegui Gil, Carlos; Bonet Carbonell, M. Luisa; Gabàs, Joel; Levy Díaz, Jordi (Springer, 2013)
    Conference report
    Restricted access - publisher's policy
    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 ...
  • Linear lower bounds and simulations in Frege systems with substitutions 

    Bonet Carbonell, M. Luisa; Galesi, Nicola (1996-10)
    External research report
    Open Access
    Our work concerns Frege systems, substitution Frege systems (sF), renaming Frege systems, top/bottom-Frege systems and extended Frege systems (eF). Urquhart shows that tautologies associated to a binary strings ...
  • Quasipolynomial size frege proofs of Frankl's Theorem on the trace of sets 

    Aisenberg, James; Bonet Carbonell, M. Luisa; Buss, Sam (2016-06-01)
    Article
    Open Access
    We extend results of Bonet, Buss and Pitassi on Bondy's Theorem and of Nozaki, Arai and Arai on Bollobas' Theorem by proving that Frankl's Theorem on the trace of sets has quasipolynomial size Frege proofs. For constant ...
  • Short proofs of the Kneser-Lovász coloring principle 

    Aisenberg, James; Bonet Carbonell, M. Luisa; Buss, Sam; Craciun, Adrian; Istrate, Gabriel (2018-08)
    Article
    Restricted access - publisher's policy
    We prove that propositional translations of the Kneser–Lovász theorem have polynomial size extended Frege proofs and quasi-polynomial size Frege proofs for all fixed values of k. We present a new counting-based combinatorial ...
  • The fractal dimension of SAT formulas 

    Ansótegui Gil, Carlos; Bonet Carbonell, M. Luisa; Giráldez Crú, Jesús; Levy Díaz, Jordi (Springer, 2014)
    Conference report
    Restricted access - publisher's policy
    Modern SAT solvers have experienced a remarkable progress on solving industrial instances. Most of the techniques have been developed after an intensive experimental process. It is believed that these techniques exploit ...
  • The Width-size method for general resolution is optimal 

    Bonet Carbonell, M. Luisa; Galesi, Nicola (1999-02)
    External research report
    Open Access
    The Width-Size Method for resolution was recently introduced by Ben-Sasson and Wigderson (BSW): Short Proofs are Narrow - Resolution Made Simple STOC 99). They found a trade-off between two complexity measures for ...
  • Towards industrial-like random SAT instances 

    Ansótegui Gil, Carlos; Bonet Carbonell, M. Luisa; Levy Díaz, Jordi (AAAI Press. Association for the Advancement of Artificial Intelligence, 2009)
    Conference report
    Restricted access - publisher's policy
    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 ...