nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

DRMaxSAT with MaxHS: First Contact

verfasst von : Antonio Morgado, Alexey Ignatiev, Maria Luisa Bonet, Joao Marques-Silva, Sam Buss

Erschienen in: Theory and Applications of Satisfiability Testing – SAT 2019

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

The proof system of Dual-Rail MaxSAT (DRMaxSAT) was recently shown to be capable of efficiently refuting families of formulas that are well-known to be hard for resolution, concretely when the MaxSAT solving approach is either MaxSAT resolution or core-guided algorithms. Moreover, DRMaxSAT based on MaxSAT resolution was shown to be stronger than general resolution. Nevertheless, existing experimental evidence indicates that the use of MaxSAT algorithms based on the computation of minimum hitting sets (MHSes), i.e. MaxHS-like algorithms, are as effective, and often more effective, than core-guided algorithms and algorithms based on MaxSAT resolution. This paper investigates the use of MaxHS-like algorithms in the DRMaxSAT proof system. Concretely, the paper proves that the propositional encoding of the pigenonhole and doubled pigenonhole principles have polynomial time refutations when the DRMaxSAT proof system uses a MaxHS-like algorithm.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Revisiting Graph Width Measures for CNF-Encodings

Nächstes Kapitel Backing Backtracking

Despite ongoing efforts, and with the exception of families of problem instances known to be hard for resolution, the performance of implementations of proof systems stronger than resolution is still far from what CDCL SAT solvers achieve in practice.

The plots show the performance of the competitors for a specifically constructed PHP and 2PHP formulas, with \({\mathcal {P}}\) clauses being disabled. (The notation and rationale will be explained below. A reader can also refer to [9, 20] for details.)

Some of the (2)PHP instances are skipped in the plots. Please, refer to [9, 20] for details.

Ansótegui, C., Bonet, M.L., Levy, J.: SAT-based MaxSAT algorithms. Artif. Intell. 196, 77–105 (2013)MathSciNetCrossRef

Audemard, G., Katsirelos, G., Simon, L.: A restriction of extended resolution for clause learning SAT solvers. In: AAAI (2010)

Bacchus, F., Hyttinen, A., Järvisalo, M., Saikko, P.: Reduced cost fixing in MaxSAT. In: Beck, J.C. (ed.) CP 2017. LNCS, vol. 10416, pp. 641–651. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66158-2_41CrossRef

Berre, D.L., Parrain, A.: The Sat4j library, release 2.2. JSAT 7(2–3), 59–6 (2010)

Biere, A.: Lingeling, plingeling and treengeling entering the SAT competition 2013. In: Balint, A., Belov, A., Heule, M., Järvisalo, M. (eds.) Proceedings of SAT Competition 2013, Department of Computer Science Series of Publications B, vol. B-2013-1, pp. 51–52. University of Helsinki (2013)

Biere, A.: Lingeling essentials, a tutorial on design and implementation aspects of the SAT solver lingeling. In: Pragmatics of SAT workshop, p. 88 (2014)

Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)

Birnbaum, E., Lozinskii, E.L.: Consistent subsets of inconsistent systems: structure and behaviour. J. Exp. Theor. Artif. Intell. 15(1), 25–46 (2003)CrossRef

Bonet, M.L., Buss, S., Ignatiev, A., Marques-Silva, J., Morgado, A.: Maxsat resolution with the dual rail encoding. In: AAAI. pp. 6565–6572 (2018)

10.

Bonet, M.L., Levy, J., Manyà, F.: Resolution for Max-SAT. Artif. Intell. 171(8–9), 606–618 (2007)MathSciNetCrossRef

11.

Bryant, R.E., Beatty, D.L., Brace, K.S., Cho, K., Sheffler, T.J.: COSMOS: a compiled simulator for MOS circuits. In: DAC, pp. 9–16 (1987)

12.

Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Log. 44(1), 36–50 (1979)MathSciNetCrossRef

13.

Davies, J., Bacchus, F.: Solving MAXSAT by solving a sequence of simpler SAT instances. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 225–239. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-23786-7_19CrossRef

14.

Davies, J., Bacchus, F.: Exploiting the power of mip solvers in maxsat. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 166–181. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39071-5_13CrossRefMATH

15.

Davies, J., Bacchus, F.: Postponing optimization to speed Up MAXSAT solving. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 247–262. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40627-0_21CrossRef

16.

Eén, N., Sörensson, N.: Translating pseudo-boolean constraints into SAT. JSAT 2(1–4), 1–26 (2006)MATH

17.

Elffers, J., Nordström, J.: Divide and conquer: towards faster pseudo-boolean solving. In: IJCAI, pp. 1291–1299 (2018). www.ijcai.org

18.

Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 252–265. Springer, Heidelberg (2006). https://doi.org/10.1007/11814948_25CrossRef

19.

Huang, J.: Extended clause learning. Artif. Intell. 174(15), 1277–1284 (2010)MathSciNetCrossRef

20.

Ignatiev, A., Morgado, A., Marques-Silva, J.: On Tackling the limits of resolution in SAT solving. In: Gaspers, S., Walsh, T. (eds.) SAT 2017. LNCS, vol. 10491, pp. 164–183. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66263-3_11CrossRefMATH

21.

Kiesl, B., Rebola-Pardo, A., Heule, M.J.H.: Extended resolution simulates DRAT. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 516–531. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94205-6_34CrossRef

22.

Koshimura, M., Zhang, T., Fujita, H., Hasegawa, R.: QMaxSAT: a partial Max-SAT solver. JSAT 8(1/2), 95–100 (2012)MathSciNetMATH

23.

Larrosa, J., Heras, F., de Givry, S.: A logical approach to efficient Max-SAT solving. Artif. Intell. 172(2–3), 204–233 (2008)MathSciNetCrossRef

24.

Li, C.M., Manyà, F.: MaxSAT. In: Biere et al. [7], pp. 613–631

25.

Marques-Silva, J., Planes, J.: On using unsatisfiability for solving maximum satisfiability CoRR abs/0712.1097 (2007)

26.

Martins, R., Joshi, S., Manquinho, V., Lynce, I.: Incremental cardinality constraints for MaxSAT. In: O’Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 531–548. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10428-7_39CrossRef

27.

Martins, R., Manquinho, V., Lynce, I.: Open-WBO: a modular MaxSAT solver^,. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 438–445. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-09284-3_33CrossRef

28.

Morgado, A., Dodaro, C., Marques-Silva, J.: Core-guided MaxSAT with soft cardinality constraints. In: O’Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 564–573. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10428-7_41CrossRef

29.

Morgado, A., Heras, F., Liffiton, M.H., Planes, J., Marques-Silva, J.: Iterative and core-guided MaxSAT solving: a survey and assessment. Constraints 18(4), 478–534 (2013)MathSciNetCrossRef

30.

Morgado, A., Ignatiev, A., Marques-Silva, J.: MSCG: robust core-guided MaxSAT solving. JSAT 9, 129–134 (2015)MathSciNet

31.

Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided MaxSAT resolution. In: AAAI, pp. 2717–2723 (2014)

32.

Palopoli, L., Pirri, F., Pizzuti, C.: Algorithms for selective enumeration of prime implicants. Artif. Intell. 111(1–2), 41–72 (1999)MathSciNetCrossRef

33.

Reiter, R.: A theory of diagnosis from first principles. Artif. Intell. 32(1), 57–95 (1987)MathSciNetCrossRef

34.

Saikko, P., Berg, J., Järvisalo, M.: LMHS: a SAT-IP hybrid MaxSAT solver. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 539–546. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-40970-2_34CrossRefMATH

35.

Sinz, C.: Towards an optimal CNF encoding of boolean cardinality constraints. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 827–831. Springer, Heidelberg (2005). https://doi.org/10.1007/11564751_73CrossRefMATH

Titel: DRMaxSAT with MaxHS: First Contact
verfasst von: Antonio Morgado
Alexey Ignatiev
Maria Luisa Bonet
Joao Marques-Silva
Sam Buss
Verlag: Springer International Publishing
Buch: Theory and Applications of Satisfiability Testing – SAT 2019
Print ISBN: 978-3-030-24257-2

Electronic ISBN: 978-3-030-24258-9

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-24258-9_17

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner