Search Results

Documents authored by Ganesh, Vijay

Document
DOI: 10.4230/LIPIcs.SAT.2023.18
Learning Shorter Redundant Clauses in SDCL Using MaxSAT

Authors: Albert Oliveras, Chunxiao Li, Darryl Wu, Jonathan Chung, and Vijay Ganesh

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

Abstract
In this paper we present the design and implementation of a Satisfaction-Driven Clause Learning (SDCL) SAT solver, MapleSDCL, which uses a MaxSAT-based technique that enables it to learn shorter, and hence better, redundant clauses. We also perform a thorough empirical evaluation of our method and show that our SDCL solver solves Mutilated Chess Board (MCB) problems significantly faster than CDCL solvers, without requiring any alteration to the branching heuristic used by the underlying CDCL SAT solver.
Cite as

Albert Oliveras, Chunxiao Li, Darryl Wu, Jonathan Chung, and Vijay Ganesh. Learning Shorter Redundant Clauses in SDCL Using MaxSAT. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{oliveras_et_al:LIPIcs.SAT.2023.18,
  author =	{Oliveras, Albert and Li, Chunxiao and Wu, Darryl and Chung, Jonathan and Ganesh, Vijay},
  title =	{{Learning Shorter Redundant Clauses in SDCL Using MaxSAT}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{18:1--18: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.18},
  URN =		{urn:nbn:de:0030-drops-184803},
  doi =		{10.4230/LIPIcs.SAT.2023.18},
  annote =	{Keywords: SAT, SDCL, MaxSAT}
}
Document
DOI: 10.4230/LIPIcs.SAT.2023.27
Limits of CDCL Learning via Merge Resolution

Authors: Marc Vinyals, Chunxiao Li, Noah Fleming, Antonina Kolokolova, and Vijay Ganesh

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

Abstract
In their seminal work, Atserias et al. and independently Pipatsrisawat and Darwiche in 2009 showed that CDCL solvers can simulate resolution proofs with polynomial overhead. However, previous work does not address the tightness of the simulation, i.e., the question of how large this overhead needs to be. In this paper, we address this question by focusing on an important property of proofs generated by CDCL solvers that employ standard learning schemes, namely that the derivation of a learned clause has at least one inference where a literal appears in both premises (aka, a merge literal). Specifically, we show that proofs of this kind can simulate resolution proofs with at most a linear overhead, but there also exist formulas where such overhead is necessary or, more precisely, that there exist formulas with resolution proofs of linear length that require quadratic CDCL proofs.
Cite as

Marc Vinyals, Chunxiao Li, Noah Fleming, Antonina Kolokolova, and Vijay Ganesh. Limits of CDCL Learning via Merge Resolution. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 27:1-27:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{vinyals_et_al:LIPIcs.SAT.2023.27,
  author =	{Vinyals, Marc and Li, Chunxiao and Fleming, Noah and Kolokolova, Antonina and Ganesh, Vijay},
  title =	{{Limits of CDCL Learning via Merge Resolution}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{27:1--27:19},
  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.27},
  URN =		{urn:nbn:de:0030-drops-184894},
  doi =		{10.4230/LIPIcs.SAT.2023.27},
  annote =	{Keywords: proof complexity, resolution, merge resolution, CDCL, learning scheme}
}
Document
DOI: 10.4230/DagRep.12.10.84
Theory and Practice of SAT and Combinatorial Solving (Dagstuhl Seminar 22411)

Authors: Olaf Beyersdorff, Armin Biere, Vijay Ganesh, Jakob Nordström, and Andy Oertel

Published in: Dagstuhl Reports, Volume 12, Issue 10 (2023)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 22411 "Theory and Practice of SAT and Combinatorial Solving". The purpose of this workshop was to explore the Boolean satisfiability (SAT) problem, which plays a fascinating dual role in computer science. By the theory of NP-completeness, this problem captures thousands of important applications in different fields, and a rich mathematical theory has been developed showing that all these problems are likely to be infeasible to solve in the worst case. But real-world problems are typically not worst-case, and in recent decades exceedingly efficient algorithms based on so-called conflict-driven clause learning (CDCL) have turned SAT solvers into highly practical tools for solving large-scale real-world problems in a wide range of application areas. Analogous developments have taken place for problems beyond NP such as SAT-based optimization (MaxSAT), pseudo-Boolean optimization, satisfiability modulo theories (SMT) solving, quantified Boolean formula (QBF) solving, constraint programming, and mixed integer programming, where the conflict-driven paradigm has sometimes been added to other powerful techniques. The current state of the art in combinatorial solving presents a host of exciting challenges at the borderline between theory and practice. Can we gain a deeper scientific understanding of the techniques and heuristics used in modern combinatorial solvers and why they are so successful? Can we develop tools for rigorous analysis of the potential and limitations of these algorithms? Can computational complexity theory be extended to shed light on real-world settings that go beyond worst case? Can more powerful methods of reasoning developed in theoretical research be harnessed to yield improvements in practical performance? And can state-of-the-art combinatorial solvers be enhanced to not only solve problems, but also provide verifiable proofs of correctness for the solutions they produce? This workshop gathered leading applied and theoretical researchers working on SAT and combinatorial optimization more broadly in order to stimulate an exchange of ideas and techniques. We see great opportunities for fruitful interplay between theory and practice in these areas, as well as for technology transfer between different paradigms in combinatorial optimization, and our assessment is that this workshop demonstrated very convincingly that a more vigorous interaction has potential for major long-term impact in computer science, as well for applications in industry.
Cite as

Olaf Beyersdorff, Armin Biere, Vijay Ganesh, Jakob Nordström, and Andy Oertel. Theory and Practice of SAT and Combinatorial Solving (Dagstuhl Seminar 22411). In Dagstuhl Reports, Volume 12, Issue 10, pp. 84-105, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{beyersdorff_et_al:DagRep.12.10.84,
  author =	{Beyersdorff, Olaf and Biere, Armin and Ganesh, Vijay and Nordstr\"{o}m, Jakob and Oertel, Andy},
  title =	{{Theory and Practice of SAT and Combinatorial Solving (Dagstuhl Seminar 22411)}},
  pages =	{84--105},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2023},
  volume =	{12},
  number =	{10},
  editor =	{Beyersdorff, Olaf and Biere, Armin and Ganesh, Vijay and Nordstr\"{o}m, Jakob and Oertel, Andy},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.12.10.84},
  URN =		{urn:nbn:de:0030-drops-178212},
  doi =		{10.4230/DagRep.12.10.84},
  annote =	{Keywords: Boolean satisfiability (SAT), SAT solving, computational complexity, proof complexity, combinatorial solving, combinatorial optimization, constraint programming, mixed integer linear programming}
}
Document
DOI: 10.4230/DagRep.12.7.80
Machine Learning and Logical Reasoning: The New Frontier (Dagstuhl Seminar 22291)

Authors: Sébastien Bardin, Somesh Jha, and Vijay Ganesh

Published in: Dagstuhl Reports, Volume 12, Issue 7 (2023)

Abstract
Machine learning (ML) and logical reasoning have been the two key pillars of AI since its inception, and yet, there has been little interaction between these two sub-fields over the years. At the same time, each of them has been very influential in their own way. ML has revolutionized many sub-fields of AI including image recognition, language translation, and game playing, to name just a few. Independently, the field of logical reasoning (e.g., SAT/SMT/CP/first-order solvers and knowledge representation) has been equally impactful in many contexts in software engineering, verification, security, AI, and mathematics. Despite this progress, there are new problems, as well as opportunities, on the horizon that seem solvable only via a combination of ML and logic. One such problem that requires one to consider combinations of logic and ML is the question of reliability, robustness, and security of ML models. For example, in recent years, many adversarial attacks against ML models have been developed, demonstrating their extraordinary brittleness. How can we leverage logic-based methods to analyze such ML systems with the aim of ensuring their reliability and security? What kind of logical language do we use to specify properties of ML models? How can we ensure that ML models are explainable and interpretable? In the reverse direction, ML methods have already been successfully applied to making solvers more efficient. In particular, solvers can be modeled as complex combinations of proof systems and ML optimization methods, wherein ML-based heuristics are used to optimally select and sequence proof rules. How can we further deepen this connection between solvers and ML? Can we develop tools that automatically construct proofs for higher mathematics? This Dagstuhl seminar seeks to answer these and related questions, with the aim of bringing together the many world-leading scientists who are conducting pioneering research at the intersection of logical reasoning and ML, enabling development of novel solutions to problems deemed impossible otherwise.
Cite as

Sébastien Bardin, Somesh Jha, and Vijay Ganesh. Machine Learning and Logical Reasoning: The New Frontier (Dagstuhl Seminar 22291). In Dagstuhl Reports, Volume 12, Issue 7, pp. 80-111, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{bardin_et_al:DagRep.12.7.80,
  author =	{Bardin, S\'{e}bastien and Jha, Somesh and Ganesh, Vijay},
  title =	{{Machine Learning and Logical Reasoning: The New Frontier (Dagstuhl Seminar 22291)}},
  pages =	{80--111},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2023},
  volume =	{12},
  number =	{7},
  editor =	{Bardin, S\'{e}bastien and Jha, Somesh and Ganesh, Vijay},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.12.7.80},
  URN =		{urn:nbn:de:0030-drops-176131},
  doi =		{10.4230/DagRep.12.7.80},
  annote =	{Keywords: Logic for ML, ML-based heuristics for solvers, SAT/SMT/CP solvers and theorem provers, Security, reliability and privacy of ML-based systems}
}
Document
DOI: 10.4230/DagRep.5.4.98
Theory and Practice of SAT Solving (Dagstuhl Seminar 15171)

Authors: Armin Biere, Vijay Ganesh, Martin Grohe, Jakob Nordström, and Ryan Williams

Published in: Dagstuhl Reports, Volume 5, Issue 4 (2015)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 15171 "Theory and Practice of SAT Solving". The purpose of this workshop was to explore one of the most significant problems in all of computer science, namely that of computing whether formulas in propositional logic are satisfiable or not. This problem is believed to be intractable in general (by the theory of NP-completeness). However, the last two decades have seen dramatic developments in algorithmic techniques, and today so-called SAT solvers are routinely and successfully used to solve large-scale real-world instances in a wide range of application areas. A surprising aspect of this development is that the best current SAT solvers are still to a large extent based on methods from the early 1960s, which can often handle formulas with millions of variables but may also get hopelessly stuck on formulas with just a few hundred variables. The fundamental question of when SAT solvers perform well or badly, and what underlying mathematical properties of the formulas influence SAT solver performance, remains very poorly understood. Another intriguing aspect is that much stronger mathematical methods of reasoning about propositional logic formulas are known today, in particular methods based on algebra and geometry, and these methods would seem to have great potential based on theoretical studies. However, attempts at harnessing the power of such methods have conspicuously failed to deliver any significant improvements in practical performance. This workshop gathered leading researchers in applied and theoretical areas of SAT and computational complexity to stimulate an increased exchange of ideas between these two communities. We see great opportunities for fruitful interplay between theoretical and applied research in this area, and believe that this workshop showed beyond doubt that a more vigorous interaction between the two has potential for major long-term impact in computer science, as well for applications in industry.
Cite as

Armin Biere, Vijay Ganesh, Martin Grohe, Jakob Nordström, and Ryan Williams. Theory and Practice of SAT Solving (Dagstuhl Seminar 15171). In Dagstuhl Reports, Volume 5, Issue 4, pp. 98-122, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{biere_et_al:DagRep.5.4.98,
  author =	{Biere, Armin and Ganesh, Vijay and Grohe, Martin and Nordstr\"{o}m, Jakob and Williams, Ryan},
  title =	{{Theory and Practice of SAT Solving (Dagstuhl Seminar 15171)}},
  pages =	{98--122},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{5},
  number =	{4},
  editor =	{Biere, Armin and Ganesh, Vijay and Grohe, Martin and Nordstr\"{o}m, Jakob and Williams, Ryan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.5.4.98},
  URN =		{urn:nbn:de:0030-drops-53520},
  doi =		{10.4230/DagRep.5.4.98},
  annote =	{Keywords: SAT, Boolean SAT solvers, SAT solving, conflict-driven clause learning, Gr\"{o}bner bases, pseudo-Boolean solvers, proof complexity, computational complexity, parameterized complexity}
}
Document
DOI: 10.4230/DagRep.4.10.98
Symbolic Execution and Constraint Solving (Dagstuhl Seminar 14442)

Authors: Christian Cadar, Vijay Ganesh, Raimondas Sasnauskas, and Koushik Sen

Published in: Dagstuhl Reports, Volume 4, Issue 10 (2015)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 14442 "Symbolic Execution and Constraint Solving", whose main goals were to bring together leading researchers in the fields of symbolic execution and constraint solving, foster greater communication between these two communities and exchange ideas about new research directions in these fields. There has been a veritable revolution over the last decade in the symbiotic fields of constraint solving and symbolic execution. Even though key ideas behind symbolic execution were introduced more than three decades ago, it was only recently that these techniques became practical as a result of significant advances in constraint satisfiability and scalable combinations of concrete and symbolic execution. Thanks to these advances, testing and analysis techniques based on symbolic execution are having a major impact on many sub-fields of software engineering, computer systems, security, and others. New applications such as program and document repair are being enabled, while older applications such as model checking are being super-charged. Additionally, significant and fast-paced advances are being made in research at the intersection of traditional program analysis, symbolic execution and constraint solving. Therefore, this seminar brought together researchers in these varied fields in order to further facilitate collaborations that take advantage of this unique and fruitful confluence of ideas from the fields of symbolic execution and constraint solving.
Cite as

Christian Cadar, Vijay Ganesh, Raimondas Sasnauskas, and Koushik Sen. Symbolic Execution and Constraint Solving (Dagstuhl Seminar 14442). In Dagstuhl Reports, Volume 4, Issue 10, pp. 98-114, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{cadar_et_al:DagRep.4.10.98,
  author =	{Cadar, Christian and Ganesh, Vijay and Sasnauskas, Raimondas and Sen, Koushik},
  title =	{{Symbolic Execution and Constraint Solving (Dagstuhl Seminar 14442)}},
  pages =	{98--114},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2015},
  volume =	{4},
  number =	{10},
  editor =	{Cadar, Christian and Ganesh, Vijay and Sasnauskas, Raimondas and Sen, Koushik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.4.10.98},
  URN =		{urn:nbn:de:0030-drops-48940},
  doi =		{10.4230/DagRep.4.10.98},
  annote =	{Keywords: Symbolic Execution, Software Testing, Automated Program Analysis, Constraint Solvers}
}
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 About DROPS Imprint Privacy Contact