DIGITAL.CSIChttps://digital.csic.esThe DSpace digital repository system captures, stores, indexes, preserves, and distributes digital research material.Tue, 18 Feb 2020 10:35:13 GMT2020-02-18T10:35:13Z50251- On the complexity of bounded second-order unification and stratified context unificationhttp://hdl.handle.net/10261/138237Title: On the complexity of bounded second-order unification and stratified context unification
Authors: Levy, Jordi; Schmidt-Schauss, Manfred; Villaret, Mateu
Abstract: Bounded Second-Order Unification is a decidable variant of undecidable Second-Order Unification. Stratified Context Unification is a decidable restriction of Context Unification, whose decidability is a long-standing open problem. This paper is a join of two separate previous, preliminary papers on NP-completeness of Bounded Second-Order Unification and Stratified Context Unification. It clarifies some omissions in these papers, joins the algorithmic parts that construct a minimal solution, and gives a clear account of a method of using singleton tree grammars for compression that may have potential usage for other algorithmic questions in related areas. © The Author 2010. Published by Oxford University Press. All rights reserved.
Wed, 19 Oct 2016 15:51:15 GMThttp://hdl.handle.net/10261/1382372016-10-19T15:51:15Z
- On the Limits of Second-Order Unificationhttp://hdl.handle.net/10261/131941Title: On the Limits of Second-Order Unification
Authors: Levy, Jordi
Abstract: Second-Order Unification is a problem that naturally arises when applying automated deduction techniques with variables denoting predicates. The problem is undecidable, but a considerable effort has been made in order to find decidable fragments, and understand the deep reasons of its complexity. Two variants of the problem, Bounded Second-Order Unification and Linear Second-Order Unification ¿where the use of bound variables in the instantiations is restricted¿, have been extensively studied in the last two decades. In this paper we summarize some decidability/undecidability/complexity results, trying to focus on those that could be more interesting for a wider audience, and involving less technical details.
Tue, 10 May 2016 15:06:24 GMThttp://hdl.handle.net/10261/1319412016-05-10T15:06:24Z
- Nominal unification from a higher-order perspectivehttp://hdl.handle.net/10261/134595Title: Nominal unification from a higher-order perspective
Authors: Levy, Jordi; Villaret, Mateu
Abstract: Nominal logic is an extension of first-order logic with equality, name-binding, renaming via name-swapping and freshness of names. Contrarily to lambda-terms, in nominal terms, bindable names, called atoms, and instantiable variables are considered as distinct entities. Moreover, atoms are capturable by instantiations, breaking a fundamental principle of the lambda-calculus. Despite these differences, nominal unification can be seen from a higher-order perspective. From this view, we show that nominal unification can be quadratically reduced to a particular fragment of higher-order unification problems: higher-order pattern unification. We also prove that the translation preserves most generality of unifiers. © 2012 ACM 1529-3785/2012/04-ART10 $10.00.
Thu, 07 Jul 2016 16:19:49 GMThttp://hdl.handle.net/10261/1345952016-07-07T16:19:49Z
- Improving WPM2 for (Weighted) Partial MaxSAThttp://hdl.handle.net/10261/133441Title: Improving WPM2 for (Weighted) Partial MaxSAT
Authors: Ansotegui, Carlos; Bonet, Maria Luisa; Gabas, Joel; Levy, Jordi
Abstract: 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.
Tue, 14 Jun 2016 13:18:19 GMThttp://hdl.handle.net/10261/1334412016-06-14T13:18:19Z
- On the undecidability of second-order unificationhttp://hdl.handle.net/10261/161159Title: On the undecidability of second-order unification
Authors: Levy, Jordi; Veanes, Margus
Abstract: There is a close relationship between word unification and second-order unification. This similarity has been exploited, for instance, in order to prove decidability of monadic second-order unification and decidability of linear second-order unification when no second-order variable occurs more than twice. The attempt to prove the second result for (nonlinear) second-order unification failed and led instead to a natural reduction from simultaneous rigid E-unification to this second-order unification. This reduction is the first main result of this paper, and it is the starting point for proving some novel results about the undecidability of second-order unification presented in the rest of the paper. We prove that second-order unification is undecidable in the following three cases: (1) each second-order variable occurs at most twice and there are only two second-order variables; (2) there is only one second-order variable and it is unary; (3) the following conditions (i)-(iv) hold for some fixed integer n: (i) the arguments of all second-order variables are ground terms of size <n, (ii) the arity of all second-order variables is <n, (iii) the number of occurrences of second-order variables is ≤5, (iv) there is either a single second-order variable or there are two second-order variables and no first-order variables. © 2000 Academic Press.
Wed, 21 Feb 2018 18:21:38 GMThttp://hdl.handle.net/10261/1611592018-02-21T18:21:38Z
- On the relation between Context and Sequence Unificationhttp://hdl.handle.net/10261/161155Title: On the relation between Context and Sequence Unification
Authors: Kutsia, Temur; Levy, Jordi; Villaret, Mateu
Abstract: Both Sequence and Context Unification generalize the same problem: Word Unification. Besides that, Sequence Unification solves equations between unranked terms involving sequence variables, and seems to be appealing for information extraction in XML documents, program transformation, knowledge representation, and rule-based programming. It is decidable. Context Unification deals with the same problem for ranked terms involving context variables, and has applications in computational linguistics and program transformation. Its decidability is a long-standing open question. In this work we study a relation between these two problems. We introduce a variant (restriction) of Context Unification, called Left-Hole Context Unification (LHCU), to which Sequence Unification is P-reduced: We define a partial currying procedure to translate Sequence Unification problems into Left-Hole Context Unification problems, and prove the soundness of the translation. Furthermore, a precise characterization of the shape of the unifiers allows us to easily reduce Left-Hole Context Unification to (the decidable problem of) Word Unification with Regular Constraints, obtaining then a new decidability proof for Sequence Unification. Finally, we define an extension of Sequence Unification (ESU) and, closing the circle, prove the inter-P-reducibility of LHCU and ESU. © 2009 Elsevier Ltd. All rights reserved.
Wed, 21 Feb 2018 17:16:40 GMThttp://hdl.handle.net/10261/1611552018-02-21T17:16:40Z
- Exploiting subproblem optimization in SAT-based MaxSAT algorithmshttp://hdl.handle.net/10261/155497Title: Exploiting subproblem optimization in SAT-based MaxSAT algorithms
Authors: Ansotegui, Carlos; Gabas, Joel; Levy, Jordi
Abstract: The Maximum Satisfiability (MaxSAT) problem is an optimization variant of the Satisfiability (SAT) problem. Several combinatorial optimization problems can be translated into a MaxSAT formula. Among exact MaxSAT algorithms, SAT-based MaxSAT algorithms are the best performing approaches for real-world problems. We have extended the WPM2 algorithm by adding several improvements. In particular, we show that by solving some subproblems of the original MaxSAT instance we can dramatically increase the efficiency of WPM2. This led WPM2 to achieve the best overall results at the international MaxSAT Evaluation 2013 (MSE13) on industrial instances. Then, we present additional techniques and heuristics to further exploit the information retrieved from the resolution of the subproblems. We exhaustively analyze the impact of each improvement what contributes to our understanding of why they work. This architecture allows to convert exact algorithms into efficient incomplete algorithms. The resulting solver had the best results on industrial instances at the incomplete track of the latest international MSE. © 2015, Springer Science+Business Media New York.
Fri, 22 Sep 2017 11:18:31 GMThttp://hdl.handle.net/10261/1554972017-09-22T11:18:31Z
- Nominal Unification of Higher Order Expressions with Recursive Lethttp://hdl.handle.net/10261/156078Title: Nominal Unification of Higher Order Expressions with Recursive Let
Authors: Schmidt-Schauss, Manfred; Kutsia, Temur; Levy, Jordi; Villaret, Mateu
Abstract: A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in non-deterministic polynomial time. We also explore specializations like nominal letrec-matching for plain expressions and for DAGs and determine their complexity. © Springer International Publishing AG 2017.
Wed, 04 Oct 2017 13:11:13 GMThttp://hdl.handle.net/10261/1560782017-10-04T13:11:13Z
- Monadic second-order unification Is NP-completehttp://hdl.handle.net/10261/160942Title: Monadic second-order unification Is NP-complete
Authors: Levy, Jordi; Schmidt-Schauss, Manfred; Villaret, Mateu
Abstract: Monadic Second-Order Unification (MSOU) is Second-Order Unification where all function constants occurring in the equations are unary. Here we prove that the problem of deciding whether a set of monadic equations has a unifier is NP-complete. We also prove that Monadic Second-Order Matching is also NP-complete. © Springer-Verlag 2004.
Mon, 19 Feb 2018 13:24:33 GMThttp://hdl.handle.net/10261/1609422018-02-19T13:24:33Z
- Simplifying the signature in second-order unificationhttp://hdl.handle.net/10261/162487Title: Simplifying the signature in second-order unification
Authors: Levy, Jordi; Villaret, Mateu
Abstract: Second-Order Unification is undecidable even for very specialized fragments. The signature plays a crucial role in these fragments. If all symbols are monadic, then the problem is NP-complete, whereas it is enough to have just one binary constant to lose decidability. In this work we reduce Second-Order Unification to Second-Order Unification with a signature that contains just one binary function symbol and constants. The reduction is based on partially currying the equations by using the binary function symbol for explicit application. Our work simplifies the study of Second-Order Unification and some of its variants, like Context Unification and Bounded Second-Order Unification. © 2009 Springer-Verlag.
Mon, 19 Mar 2018 14:37:44 GMThttp://hdl.handle.net/10261/1624872018-03-19T14:37:44Z
- Bi-Rewrite Systemshttp://hdl.handle.net/10261/160137Title: Bi-Rewrite Systems
Authors: Levy, Jordi; Agusti, Jaume
Abstract: In this article we propose an extension of term rewriting techniques to automate the deduction in monotone pre-order theories. To prove an inclusionabfrom a given setIof them, we generate fromI, using a completion procedure, abi-rewrite system, that is, a pair of rewrite relations and , and seek a common termcsuch thatacandbc. Each component of the bi-rewrite system and is allowed to be a subset of the corresponding inclusion relation or defined by the theory ofI. In order to assure the decidability and completeness of such proof procedure we study the termination and commutation of and . The proof of the commutation property is based on a critical pair lemma, using anextendeddefinition of critical pair. We also extend the existing techniques of rewriting modulo equalities to bi-rewriting modulo a set of inclusions. Although we center our attention on the completion process á la Knuth–Bendix, the same notion of extended critical pairs is suitable to be applied to the so-called unfailing completion procedures. The completion process is illustrated by means of an example corresponding to the theory of the union operator. We show that confluence ofextendedcritical pairs may be ensured addingrule schemes. Such rule schemes contain variables denoting schemes of expressions, instead of expressions. We propose the use of thelinear second-order typedλ-calculustocodifythese expression schemes. Although the general second-order unification problem is only semi-decidable, the second-order unification problems we need to solve during the completion process are decidable.
Mon, 05 Feb 2018 11:28:37 GMThttp://hdl.handle.net/10261/1601372018-02-05T11:28:37Z
- Nominal Anti-Unificationhttp://hdl.handle.net/10261/159866Title: Nominal Anti-Unification
Authors: Baumgartner, Alexander; Kutsia, Temur; Levy, Jordi; Villaret, Mateu
Abstract: We study nominal anti-unification, which is concerned with computing least general generalizations for given terms-in-context. In general, the problem does not have a least general solution, but if the set of atoms permitted in generalizations is finite, then there exists a least general generalization which is unique modulo variable renaming and α-equivalence. We present an algorithm that computes it. The algorithm relies on a subalgorithm that constructively decides equivariance between two terms-in-context. We prove soundness and completeness properties of both algorithms and analyze their complexity. Nominal anti-unification can be applied to problems were generalization of first-order terms is needed (inductive learning, clone detection, etc.), but bindings are involved. © Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret.
Tue, 30 Jan 2018 13:26:19 GMThttp://hdl.handle.net/10261/1598662018-01-30T13:26:19Z
- A Variant of Higher-Order Anti-Unificationhttp://hdl.handle.net/10261/133270Title: A Variant of Higher-Order Anti-Unification
Authors: Baumgartner, Alexander; Kutsia, Temur; Levy, Jordi; Villaret, Mateu
Abstract: We present a rule-based Huet's style anti-unification algorithm for simply-typed lambda-terms in η-long -normal form, which computes a least general higher-order pattern generalization. For a pair of arbitrary terms of the same type, such a generalization always exists and is unique modulo α-equivalence and variable renaming. The algorithm computes it in cubic time within linear space. It has been implemented and the code is freely available. © Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret; licensed under Creative Commons License CC-BY 24th International Conference on Rewriting Techniques and Applications (RTA'13).
Thu, 09 Jun 2016 16:45:25 GMThttp://hdl.handle.net/10261/1332702016-06-09T16:45:25Z
- Higher-Order Pattern Anti-Unification in Linear Timehttp://hdl.handle.net/10261/155170Title: Higher-Order Pattern Anti-Unification in Linear Time
Authors: Baumgartner, Alexander; Kutsia, Temur; Levy, Jordi; Villaret, Mateu
Abstract: We present a rule-based Huet’s style anti-unification algorithm for simply typed lambda-terms, which computes a least general higher-order pattern generalization. For a pair of arbitrary terms of the same type, such a generalization always exists and is unique modulo α-equivalence and variable renaming. With a minor modification, the algorithm works for untyped lambda-terms as well. The time complexity of both algorithms is linear.
Fri, 15 Sep 2017 13:02:18 GMThttp://hdl.handle.net/10261/1551702017-09-15T13:02:18Z
- Anti-unification for unranked terms and hedgeshttp://hdl.handle.net/10261/131203Title: Anti-unification for unranked terms and hedges
Authors: Kutsia, Temur; Levy, Jordi; Villaret, Mateu
Abstract: We study anti-unification for unranked terms and hedges that may contain term and hedge variables. The anti-unification problem of two hedges -1 and -2 is concerned with finding their generalization, a hedge q such that both -1 and -2 are instances of q under some substitutions. Hedge variables help to fill in gaps in generalizations, while term variables abstract single (sub)terms with different top function symbols. First, we design a complete and minimal algorithm to compute least general generalizations. Then, we improve the efficiency of the algorithm by restricting possible alternatives permitted in the generalizations. The restrictions are imposed with the help of a rigidity function, which is a parameter in the improved algorithm and selects certain common subsequences from the hedges to be generalized. The obtained rigid anti-unification algorithm is further made more precise by permitting combination of hedge and term variables in generalizations. Finally, we indicate a possible application of the algorithm in software engineering. © 2013 The Author(s).
Mon, 18 Apr 2016 15:54:25 GMThttp://hdl.handle.net/10261/1312032016-04-18T15:54:25Z
- The complexity of monadic second-order unificationhttp://hdl.handle.net/10261/162907Title: The complexity of monadic second-order unification
Authors: Levy, Jordi; Schmidt-Schauss, Manfred; Villaret, Mateu
Abstract: Monadic second-order unification is second-order unification where all function constants occurring in the equations are unary. Here we prove that the problem of deciding whether a set of monadic equations has a unifier is NP-complete, where we use the technique of compressing solutions using singleton context-free grammars. We prove that monadic second-order matching is also NP-complete. © 2008 Society for Industrial and Applied Mathematics.
Mon, 26 Mar 2018 11:48:30 GMThttp://hdl.handle.net/10261/1629072018-03-26T11:48:30Z
- Resolution procedures for multiple-valued optimizationhttp://hdl.handle.net/10261/133776Title: Resolution procedures for multiple-valued optimization
Authors: Ansotegui, Carlos; Bonet, Maria Luisa; Levy, Jordi; Manyà, Felip
Abstract: 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. From the logical perspective, our aim is to define complete inference systems taking as a starting point the resolution-style calculi defined for the Boolean CNF case. The result is the definition of two sound and complete resolution-style rules, called signed binary resolution and signed parallel resolution for maximum satisfiability. From the practical perspective, our main motivation is to use the language of signed clausal forms along with the newly defined inference systems as a generic approach to solve combinatorial optimization problems, and not just for solving decision problems as so far. The result is the establishment of a link between signed logic and constraint programming that provides a concise and elegant logical framework for weighted constraint programming. Â© 2012 Elsevier Inc. All rights reserved.
Mon, 20 Jun 2016 15:45:14 GMThttp://hdl.handle.net/10261/1337762016-06-20T15:45:14Z
- SAT-based MaxSAT algorithmshttp://hdl.handle.net/10261/133779Title: SAT-based MaxSAT algorithms
Authors: Ansotegui, Carlos; Bonet, Maria Luisa; Levy, Jordi
Abstract: Many industrial optimization problems can be translated to MaxSAT. Although the general problem is NP hard, like SAT, many practical problems may be solved using modern MaxSAT solvers. In this paper we present several algorithms specially designed to deal with industrial or real problems. All of them are based on the idea of solving MaxSAT through successive calls to a SAT solver. We show that this SAT-based technique is efficient in solving industrial problems. In fact, all state-of-the-art MaxSAT solvers that perform well in industrial instances are based on this technique. In particular, our solvers won the 2009 partial MaxSAT and the 2011 weighted partial MaxSAT industrial categories of the MaxSAT evaluation. We prove the correctness of all our algorithms. We also present a complete experimental study comparing the performance of our algorithms with latest MaxSAT solvers. © 2013 Elsevier B.V.
Mon, 20 Jun 2016 16:25:40 GMThttp://hdl.handle.net/10261/1337792016-06-20T16:25:40Z
- Expressing Program Requirements Using Refinement Latticeshttp://hdl.handle.net/10261/160421Title: Expressing Program Requirements Using Refinement Lattices
Authors: Robertson, Dave; Agusti, Jaume; Hesketh, Jane; Levy, Jordi
Abstract: Requirements capture is a term used in software engineering, referring to the process of obtaining a problem description ¿ a high level account of the problem which a user wants to solve. This description is then used to control the generation of a program appropriate to the solution of this problem. Reliable requirements capture is seen as a key component of future automated program construction systems, since even small amounts of information about the type of problem being tackled can often vastly reduce the space of appropriate application programs. Many special purpose requirements capture systems exist but few of these are logic based and all of them operate in tightly constrained domains. In previous research, we have used a combination of order sorted logic (for problem description) and Prolog (for the generated program) in an attempt to provide a more general purpose requirements capture system. However, in our earlier systems the connection between the problem description and the resulting program was obtained using ad hoc methods requiring considerable amounts of domain¿specific information, thus limiting the domain of application of the system. We are experimenting with languages which provide a formal connection between problem description and application program, thus eliminating the need for domain¿specific information in the translation process. This paper introduces a formal language for requirements capture which bridges the gap between an order sorted logic of problem description and the Prolog programming language. The meaning of a Prolog predicate is often characterised according to the set of bindings which can be obtained for its arguments. It is therefore possible to develop a hierarchical arrangement of predicates by comparing the sets of results obtained for stipulated variables. Using this hierarchical structure, we provide proof rules which may be used to support part of the requirements capture process. We describe the notation used for the refinement lattice; define its relationship to Prolog and demonstrate how the language can be used to support requirements capture. An interactive system for extracting Prolog programs from our refinement hierarchies, using an algorithm similar to the one described in this paper, has been implemented.
Fri, 09 Feb 2018 14:30:31 GMThttp://hdl.handle.net/10261/1604212018-02-09T14:30:31Z
- Term-graph anti-unificationhttp://hdl.handle.net/10261/197617Title: Term-graph anti-unification
Authors: Baumgartner, Alexander; Kutsia, Temur; Levy, Jordi; Villaret, Mateu
Abstract: We study anti-unification for possibly cyclic, unranked term-graphs and develop an algorithm, which computes a minimal complete set of generalizations for them. For bisimilar graphs the algorithm computes the join in the lattice generated by a functional bisimulation. These results generalize anti-unification for ranked and unranked terms to the corresponding term-graphs, and solve also anti-unification problems for rational terms and dags. Our results open a way to widen anti-unification based code clone detection techniques from a tree representation to a graph representation of the code.
Description: Trabajo presentado en el 3rd International Conference on Formal Structures for Computation and Deduction (FSCD), celebrado en Oxford (Inglaterra), del 9 al 12 de julio de 2018
Fri, 10 Jan 2020 10:51:25 GMThttp://hdl.handle.net/10261/1976172020-01-10T10:51:25Z
- Resolution for Max-SAThttp://hdl.handle.net/10261/162447Title: Resolution for Max-SAT
Authors: Bonet, Maria Luisa; Levy, Jordi; Manyà, Felip
Abstract: Max-SAT is the problem of finding an assignment minimizing the number of unsatisfied clauses in a CNF formula. We propose a resolution-like calculus for Max-SAT and prove its soundness and completeness. We also prove the completeness of some refinements of this calculus. From the completeness proof we derive an exact algorithm for Max-SAT and a time upper bound. We also define a weighted Max-SAT resolution-like rule, and show how to adapt the soundness and completeness proofs of the Max-SAT rule to the weighted Max-SAT rule. Finally, we give several particular Max-SAT problems that require an exponential number of steps of our Max-SAT rule to obtain the minimal number of unsatisfied clauses of the combinatorial principle. These results are based on the corresponding resolution lower bounds for those particular problems. © 2007 Elsevier B.V. All rights reserved.
Mon, 19 Mar 2018 12:28:00 GMThttp://hdl.handle.net/10261/1624472018-03-19T12:28:00Z
- Generating SAT instances with community structurehttp://hdl.handle.net/10261/139428Title: Generating SAT instances with community structure
Authors: Giráldez-Crú, Jesús; Levy, Jordi
Abstract: Nowadays, modern SAT solvers are able to efficiently solve many industrial, or real-world, SAT instances. However, the process of development and testing of new SAT solving techniques is conditioned to the finite and reduced number of known industrial benchmarks. Therefore, new models of random SAT instances generation that capture realistically the features of real-world problems can be beneficial to the SAT community. In many works, the structure of industrial instances has been analyzed representing them as graphs and studying some of their properties, like modularity. In this work, we use the notion of modularity to define a new model of generation of random SAT instances with community structure, called Community Attachment. For high values of modularity (i.e., clear community structure), we realistically model pseudo-industrial random SAT formulas. This model also generates SAT instances very similar to classical random formulas using a low value of modularity. We also prove that the phase transition point, if exists, is independent on the modularity. We evaluate the adequacy of this model to real industrial SAT problems in terms of SAT solvers performance, and show that modern solvers do actually exploit this community structure. Finally, we use this generator to observe the connections between the modularity of the instance and some components of the solver, such as the variable branching heuristics or the clause learning mechanism.
Wed, 26 Oct 2016 15:31:04 GMThttp://hdl.handle.net/10261/1394282016-10-26T15:31:04Z
- Locality in Random SAT Instanceshttp://hdl.handle.net/10261/164747Title: Locality in Random SAT Instances
Authors: Giráldez-Crú, Jesús; Levy, Jordi
Abstract: Despite the success of CDCL SAT solvers solving industrial problems, there are still many open questions to explain such success. In this context, the generation of random SAT instances having computational properties more similar to real-world problems becomes crucial. Such generators are possibly the best tool to analyze families of instances and solvers behaviors on them. In this paper, we present a random SAT instances generator based on the notion of locality. We show that this is a decisive dimension of attractiveness among the variables of a formula, and how CDCL SAT solvers take advantage of it. To the best of our knowledge, this is the first random SAT model that generates both scale-free structure and community structure at once.
Fri, 11 May 2018 11:54:46 GMThttp://hdl.handle.net/10261/1647472018-05-11T11:54:46Z
- A Modularity-Based Random SAT Instances Generatorhttp://hdl.handle.net/10261/158291Title: A Modularity-Based Random SAT Instances Generator
Authors: Giráldez-Crú, Jesús; Levy, Jordi
Abstract: Nowadays, many industrial SAT instances can be solved efficiently by modern SAT solvers. However, the number of real-world instances is finite. Therefore, the process of development and test of SAT solving techniques can benefit of new models of random formulas that capture more realistically the features of real-world problems. In many works, the structure of industrial instances has been analyzed representing them as graphs and studying some of their properties, like modularity. In this paper, we use modularity, or community structure, to define a new model of pseudo-industrial random SAT instances, called Community Attachment. We prove that the phase transition point, if exists, is independent on the modularity. We evaluate the adequacy of this model to real industrial problems in terms of SAT solvers performance, and show that modern solvers do actually exploit this community structure.
Mon, 18 Dec 2017 16:12:44 GMThttp://hdl.handle.net/10261/1582912017-12-18T16:12:44Z
- The Fractal Dimension of SAT Formulashttp://hdl.handle.net/10261/132347Title: The Fractal Dimension of SAT Formulas
Authors: Ansotegui, Carlos; Bonet, Maria Luisa; Giráldez-Crú, Jesús; Levy, Jordi
Abstract: 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.
Wed, 18 May 2016 16:03:30 GMThttp://hdl.handle.net/10261/1323472016-05-18T16:03:30Z