DROPS

Document

DOI: 10.4230/LIPIcs.CP.2023.9

Guiding Backtrack Search by Tracking Variables During Constraint Propagation

Authors: Gilles Audemard, Christophe Lecoutre, and Charles Prud'homme

Published in: LIPIcs, Volume 280, 29th International Conference on Principles and Practice of Constraint Programming (CP 2023)

Abstract

It is well-known that variable ordering heuristics play a central role in solving efficiently Constraint Satisfaction Problem (CSP) instances. From the early 80’s, and during more than two decades, the dynamic variable ordering heuristic selecting the variable with the smallest domain was clearly prevailing. Then, from the mid 2000’s, some adaptive heuristics have been introduced: their principle is to collect some useful information during the search process in order to take better informed decisions. Among those adaptive heuristics, wdeg/dom (and its variants) remains particularly robust. In this paper, we introduce an original heuristic based on the midway processing of failing executions of constraint propagation: this heuristic called pick/dom tracks the variables that are directly involved in the process of constraint propagation, when ending with a conflict. The robustness of this new heuristic is demonstrated from a large experimentation conducted with the constraint solver ACE. Interestingly enough, one can observe some complementary between the early, midway and late forms of processing of conflicts.

Cite as

Gilles Audemard, Christophe Lecoutre, and Charles Prud'homme. Guiding Backtrack Search by Tracking Variables During Constraint Propagation. In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{audemard_et_al:LIPIcs.CP.2023.9,
  author =	{Audemard, Gilles and Lecoutre, Christophe and Prud'homme, Charles},
  title =	{{Guiding Backtrack Search by Tracking Variables During Constraint Propagation}},
  booktitle =	{29th International Conference on Principles and Practice of Constraint Programming (CP 2023)},
  pages =	{9:1--9:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-300-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{280},
  editor =	{Yap, Roland H. C.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2023.9},
  URN =		{urn:nbn:de:0030-drops-190461},
  doi =		{10.4230/LIPIcs.CP.2023.9},
  annote =	{Keywords: Variable Ordering Heuristics, Variable Weighting}
}

Document

DOI: 10.4230/LIPIcs.SAT.2022.28

A New Exact Solver for (Weighted) Max#SAT

Authors: Gilles Audemard, Jean-Marie Lagniez, and Marie Miceli

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

Abstract

We present and evaluate d4Max, an exact approach for solving the Weighted Max#SAT problem. The Max#SAT problem extends the model counting problem (#SAT) by considering a tripartition of the variables {X, Y, Z}, and consists in maximizing over X the number of assignments to Y that can be extended to a solution with some assignment to Z. The Weighted Max#SAT problem is an extension of the Max#SAT problem with weights associated on each interpretation. We test and compare our approach with other state-of-the-art solvers on the challenging task in probabilistic inference of finding the marginal maximum a posteriori probability (MMAP) of a given subset of the variables in a Bayesian network and on exist-random quantified SSAT benchmarks. The results clearly show the overall superiority of d4Max in term of speed and number of instances solved. Moreover, we experimentally show that, in general, d4Max is able to quickly spot a solution that is close to optimal, thereby opening the door to an efficient anytime approach.

Cite as

Gilles Audemard, Jean-Marie Lagniez, and Marie Miceli. A New Exact Solver for (Weighted) Max#SAT. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 28:1-28:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{audemard_et_al:LIPIcs.SAT.2022.28,
  author =	{Audemard, Gilles and Lagniez, Jean-Marie and Miceli, Marie},
  title =	{{A New Exact Solver for (Weighted) Max#SAT}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{28:1--28:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.28},
  URN =		{urn:nbn:de:0030-drops-167022},
  doi =		{10.4230/LIPIcs.SAT.2022.28},
  annote =	{Keywords: Max#SAT, EMaj-SAT, Weighted Projected Model Counting, SSAT}
}

Search Results

Documents authored by Audemard, Gilles

Guiding Backtrack Search by Tracking Variables During Constraint Propagation

Abstract

Cite as

A New Exact Solver for (Weighted) Max#SAT

Abstract

Cite as

Thanks for your feedback!

Could not send message