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 values of the parameter t, we prove that Frankl's Theorem has polynomial size AC(0)-Frege proofs from instances of the pigeonhole principle.
Ansótegui, C.; Bonet, M.; Giráldez, J.; Levy, J. International Joint Conference on Automated Reasoning p. 107-121 DOI: 10.1007/978-3-319-08587-6_8 Data de presentació: 2014-07-19 Presentació treball a congrés
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 underlying structure of industrial instances. However, there is not a precise definition of the notion of structure. Recently, there have been some attempts to analyze this structure in terms of complex networks, with the long-term aim of explaining the success of SAT solving techniques, and possibly improving them. We study the fractal dimension of SAT instances with the aim of complementing the model that describes the structure of industrial instances. We show that many industrial families of formulas are self-similar, with a small fractal dimension. We also show how this dimension is affected by the addition of learnt clauses during the execution of SAT solvers.
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.
Ansótegui, C.; Bonet, M.; Gabàs, J.; Levy, J. International Conference on Principles and Practice of Constraint Programming p. 117-132 DOI: 10.1007/978-3-642-40627-0_12 Data de presentació: 2013-09-16 Presentació treball a congrés
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.
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-
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.
Ansótegui, C.; Bonet, M.; Li, C.; Levy, J. International Conference of the Catalan Association for Artificial Intelligence p. 173-184 DOI: 10.3233/978-1-61499-139-7-173 Data de presentació: 2012 Presentació treball a congrés
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.
Ansótegui, C.; Bonet, M.; Levy, J. International Conference on Principles and Practice of Constraint Programming p. 127-141 DOI: 10.1007/978-3-642-04244-7_13 Data de presentació: 2009-09 Presentació treball a congrés
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
Ansótegui, C.; Bonet, M.; Levy, J. International Conference on Theory and Applications of Satisfiability Testing p. 427-440 DOI: 10.1007/978-3-642-02777-2_39 Data de presentació: 2009-07 Presentació treball a congrés
Bonet, M.; St. John, K. International Conference on Theory and Applications of Satisfiability Testing p. 4-17 DOI: 10.1007/978-3-642-02777-2_3 Data de presentació: 2009-06-30 Presentació treball a congrés
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).
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 al espacio. 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.
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 Resolution refutations: the size (i.e. the number
of clauses) and the width (i.e. the size of the largest
clause). Using this trade-off they reduced
the problem of giving lower bounds on the size to that of giving lower
bounds on the width and gave a unified method to obtain all previously
known lower bounds on the size of Resolution refutations. Moreover,
the use of the width as a complexity measure for Resolution proofs
suggested a new very simple algorithm for searching for Resolution
proof. Here we face with the following question (also stated as an open
problem in BSW): can the size-width
trade-off be improved in the case of unrestricted resolution ? We
give a negative answer to this question showing that the result of
BSW is optimal. Our result, also holds for the most commonly
used restrictions of Resolution like Regular, Davis-Putnam, Positive,
Negative and Linear.
A consequence of our result is that the width-based algorithm
proposed by BSW for searching for Resolution proofs cannot be
used to show the automatizability of Resolution and its restrictions.