Article

Reducing chaos in SAT-like search: finding solutions close to a given one

Authors:

Ignasi Abío,

Morgan Deters,

Robert Nieuwenhuis,

Peter J. StuckeyAuthors Info & Claims

SAT'11: Proceedings of the 14th international conference on Theory and application of satisfiability testing

Pages 273 - 286

Published: 19 June 2011 Publication History

Publisher Site

Abstract

Motivated by our own industrial users, we attack the following challenge that is crucial in many practical planning, scheduling or timetabling applications. Assume that a solver has found a solution for a given hard problem and, due to unforeseen circumstances (e.g., rescheduling), or after an analysis by a committee, a few more constraints have to be added and the solver has to be re-run. Then it is almost always important that the new solution is "close" to the original one.

The activity-based variable selection heuristics used by SAT solvers make search chaotic, i.e., extremely sensitive to the initial conditions. Therefore, re-running with just one additional clause added at the end of the input usually gives a completely different solution. We show that naive approaches for finding close solutions do not work at all, and that solving the Boolean optimization problem is far too inefficient: to find a reasonably close solution, state-of-the-art tools typically require much more time than was needed to solve the original problem.

Here we propose the first (to our knowledge) approach that obtains close solutions quickly. In fact, it typically finds the optimal (i.e., closest) solution in only 25% of the time the solver took in solving the original problem. Our approach requires no deep theoretical or conceptual innovations. Still, it is non-trivial to come up with and will certainly be valuable for researchers and practitioners facing the same problem.

References

[1]

Ansótegui, C., Bonet, M.L., Levy, J.: Solving (weighted) partial maxsat through satisfiability testing. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 427-440. Springer, Heidelberg (2007)

Digital Library

Google Scholar

[2]

Bailleux, O., Marquis, P.: Some computational aspects of distance-sat. J. Autom. Reasoning 37(4), 231-260 (2006)

Digital Library

Google Scholar

[3]

Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem-Proving. Comm. of the ACM, CACM 5(7), 394-397 (1962)

Digital Library

Google Scholar

[4]

Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502-518. Springer, Heidelberg (2004)

Google Scholar

[5]

Goldberg, E., Novikov, Y.: BerkMin: A Fast and Robust SAT-Solver. In: 2002 Conference on Design, Automation, and Test in Europe, DATE 2002, pp. 142-149. IEEE Computer Society, Los Alamitos (2002)

Digital Library

Google Scholar

[6]

Hebrard, E., Hnich, B., O'Sullivan, B., Walsh, T.: Finding diverse and similar solutions in constraint programming. In: 20th National Conf. on Artificial Intelligence (AAAI), pp. 372-377 (2005)

Digital Library

Google Scholar

[7]

Heras, F., Larrosa, J., Oliveras, A.: MiniMaxSAT: An efficient Weighted Max-SAT Solver. J. Artificial Intell. Research 31, 1-32 (2008)

Digital Library

Google Scholar

[8]

Larrosa, J., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: Branch and bound for boolean optimization and the generation of optimality certificates. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 453-466. Springer, Heidelberg (2009)

Digital Library

Google Scholar

[9]

Larrosa, J., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: A framework for certified boolean branch-and-bound optimization. J. Autom. Reasoning 46(1), 81-102 (2011)

Digital Library

Google Scholar

[10]

Manquinho, V., Marques-Silva, J.: Satisfiability-based algorithms for boolean optimization. Ann. Math. Artif. Intell. 40(3-4), 353-372 (2004)

Digital Library

Google Scholar

[11]

Manquinho, V., Silva, J.M., Planes, J.: Algorithms for weighted boolean optimization. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 495-508. Springer, Heidelberg (2007)

Digital Library

Google Scholar

[12]

Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM, JACM 53(6), 937-977 (2006)

Digital Library

Google Scholar

[13]

Ohrimenko, O., Stuckey, P.J., Codish, M.: Propagation via lazy clause generation. Constraints 14(3), 357-391 (2009)

Digital Library

Google Scholar

[14]

Pipatsrisawat, K., Darwiche, A.: On modern clause-learning satisfiability solvers. J. Autom. Reason. 44(3), 277-301 (2010)

Digital Library

Google Scholar

Cited By

View all

Chu GStuckey P(2012)Inter-instance Nogood Learning in Constraint ProgrammingProceedings of the 18th International Conference on Principles and Practice of Constraint Programming - Volume 751410.5555/2969951.2969975(238-247)Online publication date: 8-Oct-2012
https://dl.acm.org/doi/10.5555/2969951.2969975
Abío IStuckey P(2012)Conflict Directed Lazy DecompositionProceedings of the 18th International Conference on Principles and Practice of Constraint Programming - Volume 751410.5555/2969951.2969964(70-85)Online publication date: 8-Oct-2012
https://dl.acm.org/doi/10.5555/2969951.2969964

Reducing chaos in SAT-like search: finding solutions close to a given one
1. Theory of computation
  1. Theory and algorithms for application domains
    1. Machine learning theory
      1. Reinforcement learning

Recommendations

Stochastic local search for incremental SAT

The boolean satisfiability problem (SAT) is stated as follows: given a boolean formula in CNF, find a truth assignment that satisfies its clauses. In this paper, we present a general framework based on stochastic local search and the structure of the ...
Clause elimination for SAT and QSAT

The famous archetypical NP-complete problem of Boolean satisfiability (SAT) and its PSPACE-complete generalization of quantified Boolean satisfiability (QSAT) have become central declarative programming paradigms through which real-world instances of ...
Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T)

We first introduce Abstract DPLL, a rule-based formulation of the Davis--Putnam--Logemann--Loveland (DPLL) procedure for propositional satisfiability. This abstract framework allows one to cleanly express practical DPLL algorithms and to formally reason ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

SAT'11: Proceedings of the 14th international conference on Theory and application of satisfiability testing

June 2011

378 pages

ISBN:9783642215803

Editors:
Karem A. Sakallah
University of Michigan, Department of EECS, Ann Arbor, MI
,
Laurent Simon
Université Orsay Paris-Sud 11, LRI / INRIA, Orsay cedex

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 19 June 2011

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 17 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Chu GStuckey P(2012)Inter-instance Nogood Learning in Constraint ProgrammingProceedings of the 18th International Conference on Principles and Practice of Constraint Programming - Volume 751410.5555/2969951.2969975(238-247)Online publication date: 8-Oct-2012
https://dl.acm.org/doi/10.5555/2969951.2969975
Abío IStuckey P(2012)Conflict Directed Lazy DecompositionProceedings of the 18th International Conference on Principles and Practice of Constraint Programming - Volume 751410.5555/2969951.2969964(70-85)Online publication date: 8-Oct-2012
https://dl.acm.org/doi/10.5555/2969951.2969964

Abstract

References

Cited By

Recommendations

Stochastic local search for incremental SAT

Clause elimination for SAT and QSAT

Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T)

Comments

Information

Published In

Sponsors

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations