Search Results

Documents authored by Nieuwenhuis, Robert

Document
DOI: 10.4230/LIPIcs.SAT.2024.22
Speeding up Pseudo-Boolean Propagation

Authors: Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Rui Zhao

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
Unit propagation is known to be one of the most time-consuming procedures inside CDCL-based SAT solvers. Not surprisingly, it has been studied in depth and the two-watched-literal scheme, enhanced with implementation details boosting its performance, has emerged as the dominant method. In pseudo-Boolean solvers, the importance of unit propagation is similar, but no dominant method exists: counter propagation and watched-based extensions are efficient for different types of constraints, which has opened the door to hybrid methods. However, probably due to the higher complexity of implementing pseudo-Boolean solvers, research efforts have not focused much on concrete implementation details for unit propagation but rather on higher-level aspects of other procedures, such as conflict analysis. In this paper, we present (i) a novel methodology to precisely assess the performance of propagation mechanisms, (ii) an evaluation of implementation variants of the propagation methods present in {RoundingSat} and (iii) a detailed analysis showing that hybrid methods outperform the ones based on a single technique. Our final contribution is to show that a carefully implemented hybrid propagation method is considerably faster than the preferred propagation mechanism in {RoundingSat}, and that this improvement leads to a better overall performance of the solver.
Cite as

Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Rui Zhao. Speeding up Pseudo-Boolean Propagation. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{nieuwenhuis_et_al:LIPIcs.SAT.2024.22,
  author =	{Nieuwenhuis, Robert and Oliveras, Albert and Rodr{\'\i}guez-Carbonell, Enric and Zhao, Rui},
  title =	{{Speeding up Pseudo-Boolean Propagation}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{22:1--22:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.22},
  URN =		{urn:nbn:de:0030-drops-205449},
  doi =		{10.4230/LIPIcs.SAT.2024.22},
  annote =	{Keywords: SAT, Pseudo-Boolean Solving, Implementation-level Details}
}
Document
DOI: 10.4230/DagRep.1.7.23
Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272)

Authors: Nikolaj Bjorner, Robert Nieuwenhuis, Helmut Veith, and Andrei Voronkov

Published in: Dagstuhl Reports, Volume 1, Issue 7 (2011)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 11272 "Decision Procedures in Soft, Hard and Bio-ware (Follow Up)". It was held as a follow-on for a seminar 10161, of the same title, that took place in late April 2010 during the initial eruption of Eyjafjallajökull. In spite of the travel disruptions caused by the eruption of the volcano, the original seminar received a respectable turnout by European, mainly German and Italian participants. Unfortunately, the eruption hindered participation from overseas or even more distant parts of Europe. This caused the seminar to cover only part of the original objective. The follow-on seminar focused on the remaining objectives, in particular to bio-ware and constraint solving methods.
Cite as

Nikolaj Bjorner, Robert Nieuwenhuis, Helmut Veith, and Andrei Voronkov. Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272). In Dagstuhl Reports, Volume 1, Issue 7, pp. 23-35, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@Article{bjorner_et_al:DagRep.1.7.23,
  author =	{Bjorner, Nikolaj and Nieuwenhuis, Robert and Veith, Helmut and Voronkov, Andrei},
  title =	{{Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272)}},
  pages =	{23--35},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2011},
  volume =	{1},
  number =	{7},
  editor =	{Bjorner, Nikolaj and Nieuwenhuis, Robert and Veith, Helmut and Voronkov, Andrei},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.1.7.23},
  URN =		{urn:nbn:de:0030-drops-32775},
  doi =		{10.4230/DagRep.1.7.23},
  annote =	{Keywords: Hardware and Software Verification, Bio-analysis, Satisfiability Modulo Theories, Dynamic Symbolic Execution, Interpolants}
}
Document
DOI: 10.4230/DagSemProc.10161.1
10161 Abstracts Collection – Decision Procedures in Software, Hardware and Bioware

Authors: Nikolaj Bjorner, Robert Nieuwenhuis, Helmut Veith, and Andrei Voronkov

Published in: Dagstuhl Seminar Proceedings, Volume 10161, Decision Procedures in Software, Hardware and Bioware (2010)

Abstract
From April 19th, 2010 to April 23rd, 2010, the Dagstuhl Seminar 10161 "Decision Procedures in Soft, Hard and Bio-ware" was held in Schloss Dagstuhl Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as links to slides and links to papers behind the presentations and papers produced as a result of the seminar are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

Nikolaj Bjorner, Robert Nieuwenhuis, Helmut Veith, and Andrei Voronkov. 10161 Abstracts Collection – Decision Procedures in Software, Hardware and Bioware. In Decision Procedures in Software, Hardware and Bioware. Dagstuhl Seminar Proceedings, Volume 10161, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{bjorner_et_al:DagSemProc.10161.1,
  author =	{Bjorner, Nikolaj and Nieuwenhuis, Robert and Veith, Helmut and Voronkov, Andrei},
  title =	{{10161 Abstracts Collection – Decision Procedures in Software, Hardware and Bioware}},
  booktitle =	{Decision Procedures in Software, Hardware and Bioware},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10161},
  editor =	{Nikolaj Bjorner and Robert Nieuwenhuis and Helmut Veith and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10161.1},
  URN =		{urn:nbn:de:0030-drops-27421},
  doi =		{10.4230/DagSemProc.10161.1},
  annote =	{Keywords: Decision Procedures, Satisfiability Modulo Theories, Software Verification, Dynamic Symbolic Execution, Interpolants, Hardware Verification, Bio-analysis}
}
Document
DOI: 10.4230/DagSemProc.10161.2
10161 Executive Summary – Decision Procedures in Software, Hardware and Bioware

Authors: Nikolaj Bjorner, Robert Nieuwenhuis, Helmut Veith, and Andrei Voronkov

Published in: Dagstuhl Seminar Proceedings, Volume 10161, Decision Procedures in Software, Hardware and Bioware (2010)

Abstract
The main goal of the seminar Decision Procedures in Soft, Hard and Bio-ware was to bring together renowned as well as young aspiring researchers from two groups. The first group formed by researchers who develop both theory and efficient implementations of decision procedures. The second group comprising of researchers from application areas such as program analysis and testing, crypto-analysis, hardware verification, industrial planning and scheduling, and bio-informatics, who have worked with, and contributed to, high quality decision procedures. The purpose of the seminar was to heighten awareness between tool and theory developers for decision procedures with the array of applications found in software, hardware and biological systems analysis.
Cite as

Nikolaj Bjorner, Robert Nieuwenhuis, Helmut Veith, and Andrei Voronkov. 10161 Executive Summary – Decision Procedures in Software, Hardware and Bioware. In Decision Procedures in Software, Hardware and Bioware. Dagstuhl Seminar Proceedings, Volume 10161, pp. 1-6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{bjorner_et_al:DagSemProc.10161.2,
  author =	{Bjorner, Nikolaj and Nieuwenhuis, Robert and Veith, Helmut and Voronkov, Andrei},
  title =	{{10161 Executive Summary – Decision Procedures in Software, Hardware and Bioware }},
  booktitle =	{Decision Procedures in Software, Hardware and Bioware},
  pages =	{1--6},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10161},
  editor =	{Nikolaj Bjorner and Robert Nieuwenhuis and Helmut Veith and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10161.2},
  URN =		{urn:nbn:de:0030-drops-27369},
  doi =		{10.4230/DagSemProc.10161.2},
  annote =	{Keywords: Decision procedures, software, hardware, bioware}
}
Document
DOI: 10.4230/DagSemProc.07401.1
07401 Abstracts Collection – Deduction and Decision Procedures

Authors: Franz Baader, Byron Cook, Jürgen Giesl, and Robert Nieuwenhuis

Published in: Dagstuhl Seminar Proceedings, Volume 7401, Deduction and Decision Procedures (2007)

Abstract
From 01.10. to 05.10.2007, the Dagstuhl Seminar 07401 ``Deduction and Decision Procedures'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper.
Cite as

Franz Baader, Byron Cook, Jürgen Giesl, and Robert Nieuwenhuis. 07401 Abstracts Collection – Deduction and Decision Procedures. In Deduction and Decision Procedures. Dagstuhl Seminar Proceedings, Volume 7401, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{baader_et_al:DagSemProc.07401.1,
  author =	{Baader, Franz and Cook, Byron and Giesl, J\"{u}rgen and Nieuwenhuis, Robert},
  title =	{{07401 Abstracts Collection – Deduction and Decision Procedures}},
  booktitle =	{Deduction and Decision Procedures},
  pages =	{1--20},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7401},
  editor =	{Franz Baader and Byron Cook and J\"{u}rgen Giesl and Robert Nieuwenhuis},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07401.1},
  URN =		{urn:nbn:de:0030-drops-12521},
  doi =		{10.4230/DagSemProc.07401.1},
  annote =	{Keywords: Decision Procedures, Deduction, Boolean Satisfiability, First-Order Logic, Integer Arithmetic, Combination of Theories, Satisfiability Modulo Theories Rewrite Systems, Formal Verification, Model Finding}
}
Document
DOI: 10.4230/DagSemProc.07401.2
07401 Executive Summary – Deduction and Decision Procedures

Authors: Franz Baader, Byron Cook, Jürgen Giesl, and Robert Nieuwenhuis

Published in: Dagstuhl Seminar Proceedings, Volume 7401, Deduction and Decision Procedures (2007)

Abstract
Formal logic provides a mathematical foundation for many areas of computer science. Significant progress has been made in the challenge of making computers perform non-trivial logical reasoning. be it fully automatic, or in interaction with humans. In the last years it has become more and more evident that theory-specific reasoners, and in particular decision procedures, are extremely important in many applications of such deduction tools. General-purpose reasoning methods such as resolution or paramodulation alone are not efficient enough to handle the needs of real-world applications. % For this reason, the focus of this seminar was on decision procedures, their integration into general-purpose theorem provers, and the application of the integrated tools in computer science.
Cite as

Franz Baader, Byron Cook, Jürgen Giesl, and Robert Nieuwenhuis. 07401 Executive Summary – Deduction and Decision Procedures. In Deduction and Decision Procedures. Dagstuhl Seminar Proceedings, Volume 7401, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{baader_et_al:DagSemProc.07401.2,
  author =	{Baader, Franz and Cook, Byron and Giesl, J\"{u}rgen and Nieuwenhuis, Robert},
  title =	{{07401 Executive Summary – Deduction and Decision Procedures}},
  booktitle =	{Deduction and Decision Procedures},
  pages =	{1--3},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7401},
  editor =	{Franz Baader and Byron Cook and J\"{u}rgen Giesl and Robert Nieuwenhuis},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07401.2},
  URN =		{urn:nbn:de:0030-drops-12515},
  doi =		{10.4230/DagSemProc.07401.2},
  annote =	{Keywords: Formal Logic, Deduction, Artificial Intelligence}
}
Document
DOI: 10.4230/DagSemProc.05431.1
05431 Abstracts Collection – Deduction and Applications

Authors: Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, and Andrei Voronkov

Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)

Abstract
From 23.10.05 to 28.10.05, the Dagstuhl Seminar 05431 ``Deduction and Applications'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, and Andrei Voronkov. 05431 Abstracts Collection – Deduction and Applications. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, pp. 1-23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{baader_et_al:DagSemProc.05431.1,
  author =	{Baader, Franz and Baumgartner, Peter and Nieuwenhuis, Robert and Voronkov, Andrei},
  title =	{{05431 Abstracts Collection – Deduction and Applications}},
  booktitle =	{Deduction and Applications},
  pages =	{1--23},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5431},
  editor =	{Franz Baader and Peter Baumgartner and Robert Nieuwenhuis and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05431.1},
  URN =		{urn:nbn:de:0030-drops-5625},
  doi =		{10.4230/DagSemProc.05431.1},
  annote =	{Keywords: Formal logic, deduction, artificial intelligence}
}
Document
DOI: 10.4230/DagSemProc.05431.2
05431 Executive Summary – Deduction and Applications

Authors: Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, and Andrei Voronkov

Published in: Dagstuhl Seminar Proceedings, Volume 5431, Deduction and Applications (2006)

Abstract
Formal logic provides a mathematical foundation for many areas of computer science. Logical languages are used as specification language within, e.g., program development and verification, hardware design and verification, relational databases, and many subfields of Artificial Intelligence. Automated Deduction is concerned with the design and implementation of algorithms based on logical deduction for solving problems in these areas. The last years have seen considerable improvements concerning both basic automated deduction technology and its (real-world) applications. Accordingly, the goal of the seminar was to bring together researchers from both sides in order to get an overview of the state of the art, and also to get ideas how to advance automated deduction from an application oriented point of view.
Cite as

Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, and Andrei Voronkov. 05431 Executive Summary – Deduction and Applications. In Deduction and Applications. Dagstuhl Seminar Proceedings, Volume 5431, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{baader_et_al:DagSemProc.05431.2,
  author =	{Baader, Franz and Baumgartner, Peter and Nieuwenhuis, Robert and Voronkov, Andrei},
  title =	{{05431 Executive Summary – Deduction and Applications}},
  booktitle =	{Deduction and Applications},
  pages =	{1--3},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5431},
  editor =	{Franz Baader and Peter Baumgartner and Robert Nieuwenhuis and Andrei Voronkov},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05431.2},
  URN =		{urn:nbn:de:0030-drops-5100},
  doi =		{10.4230/DagSemProc.05431.2},
  annote =	{Keywords: Formal logic, deduction, artificial intelligence}
}
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