Search Results

Documents authored by Levy, Jordi

Document
DOI: 10.4230/LIPIcs.SAT.2023.5
Polynomial Calculus for MaxSAT

Authors: Ilario Bonacina, Maria Luisa Bonet, and Jordi Levy

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract
MaxSAT is the problem of finding an assignment satisfying the maximum number of clauses in a CNF formula. We consider a natural generalization of this problem to generic sets of polynomials and propose a weighted version of Polynomial Calculus to address this problem. Weighted Polynomial Calculus is a natural generalization of MaxSAT-Resolution and weighted Resolution that manipulates polynomials with coefficients in a finite field and either weights in ℕ or ℤ. We show the soundness and completeness of these systems via an algorithmic procedure. Weighted Polynomial Calculus, with weights in ℕ and coefficients in 𝔽₂, is able to prove efficiently that Tseitin formulas on a connected graph are minimally unsatisfiable. Using weights in ℤ, it also proves efficiently that the Pigeonhole Principle is minimally unsatisfiable.
Cite as

Ilario Bonacina, Maria Luisa Bonet, and Jordi Levy. Polynomial Calculus for MaxSAT. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bonacina_et_al:LIPIcs.SAT.2023.5,
  author =	{Bonacina, Ilario and Bonet, Maria Luisa and Levy, Jordi},
  title =	{{Polynomial Calculus for MaxSAT}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{5:1--5:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.5},
  URN =		{urn:nbn:de:0030-drops-184670},
  doi =		{10.4230/LIPIcs.SAT.2023.5},
  annote =	{Keywords: Polynomial Calculus, MaxSAT, Proof systems, Algebraic reasoning}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.9
Term-Graph Anti-Unification

Authors: Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

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.
Cite as

Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. Term-Graph Anti-Unification. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{baumgartner_et_al:LIPIcs.FSCD.2018.9,
  author =	{Baumgartner, Alexander and Kutsia, Temur and Levy, Jordi and Villaret, Mateu},
  title =	{{Term-Graph Anti-Unification}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{9:1--9:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.9},
  URN =		{urn:nbn:de:0030-drops-91797},
  doi =		{10.4230/LIPIcs.FSCD.2018.9},
  annote =	{Keywords: Cyclic term-graps, anti-unification, least general generalization}
}
Document
DOI: 10.4230/LIPIcs.RTA.2015.57
Nominal Anti-Unification

Authors: Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

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 alpha-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 where generalization of first-order terms is needed (inductive learning, clone detection, etc.), but bindings are involved.
Cite as

Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. Nominal Anti-Unification. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 57-73, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{baumgartner_et_al:LIPIcs.RTA.2015.57,
  author =	{Baumgartner, Alexander and Kutsia, Temur and Levy, Jordi and Villaret, Mateu},
  title =	{{Nominal Anti-Unification}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{57--73},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.57},
  URN =		{urn:nbn:de:0030-drops-51895},
  doi =		{10.4230/LIPIcs.RTA.2015.57},
  annote =	{Keywords: Nominal Anti-Unification, Term-in-context, Equivariance}
}
Document
DOI: 10.4230/LIPIcs.RTA.2013.113
A Variant of Higher-Order Anti-Unification

Authors: Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret

Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)

Abstract
We present a rule-based Huet's style anti-unification algorithm for simply-typed lambda-terms in eta-long beta-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 alpha-equivalence and variable renaming. The algorithm computes it in cubic time within linear space. It has been implemented and the code is freely available.
Cite as

Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. A Variant of Higher-Order Anti-Unification. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 113-127, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{baumgartner_et_al:LIPIcs.RTA.2013.113,
  author =	{Baumgartner, Alexander and Kutsia, Temur and Levy, Jordi and Villaret, Mateu},
  title =	{{A Variant of Higher-Order Anti-Unification}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{113--127},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.113},
  URN =		{urn:nbn:de:0030-drops-40579},
  doi =		{10.4230/LIPIcs.RTA.2013.113},
  annote =	{Keywords: higher-order anti-unification, higher-order patterns}
}
Document
DOI: 10.4230/LIPIcs.RTA.2011.219
Anti-Unification for Unranked Terms and Hedges

Authors: Temur Kutsia, Jordi Levy, and Mateu Villaret

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

Abstract
We study anti-unification for unranked terms and hedges that may contain term and hedge variables. The anti-unification problem of two hedges ~s_1 and ~s_2 is concerned with finding their generalization, a hedge ~q such that both ~s_1 and ~s_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 that is a parameter in the improved algorithm and selects certain common subsequences from the hedges to be generalized. Finally, we indicate a possible application of the algorithm in software engineering.
Cite as

Temur Kutsia, Jordi Levy, and Mateu Villaret. Anti-Unification for Unranked Terms and Hedges. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 219-234, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{kutsia_et_al:LIPIcs.RTA.2011.219,
  author =	{Kutsia, Temur and Levy, Jordi and Villaret, Mateu},
  title =	{{Anti-Unification for Unranked Terms and Hedges}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{219--234},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.219},
  URN =		{urn:nbn:de:0030-drops-31181},
  doi =		{10.4230/LIPIcs.RTA.2011.219},
  annote =	{Keywords: Anti-unification, generalization, unranked terms, hedges, software clones.}
}
Document
DOI: 10.4230/LIPIcs.RTA.2010.209
An Efficient Nominal Unification Algorithm

Authors: Jordi Levy and Mateu Villaret

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract
Nominal Unification is an extension of first-order unification where terms can contain binders and unification is performed modulo alpha-equivalence. Here we prove that the existence of nominal unifiers can be decided in quadratic time. First, we linearly-reduce nominal unification problems to a sequence of freshness and equalities between atoms, modulo a permutation, using ideas as Paterson and Wegman for first-order unification. Second, we prove that solvability of these reduced problems may be checked in quadratic time. Finally, we point out how using ideas of Brown and Tarjan for unbalanced merging, we could solve these reduced problems more efficiently.
Cite as

Jordi Levy and Mateu Villaret. An Efficient Nominal Unification Algorithm. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 209-226, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{levy_et_al:LIPIcs.RTA.2010.209,
  author =	{Levy, Jordi and Villaret, Mateu},
  title =	{{An Efficient Nominal Unification Algorithm}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{209--226},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.209},
  URN =		{urn:nbn:de:0030-drops-26544},
  doi =		{10.4230/LIPIcs.RTA.2010.209},
  annote =	{Keywords: Nominal logic, unification}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact