Modern SAT solvers are designed to handle problems expressed in Conjunctive Normal Form (CNF) so that non-CNF problems must be CNF-ized upfront, typically by using variants of either Tseitin or Plaisted and Greenbaum transformations. When passing from solving to enumeration, however, the capability of producing partial satisfying assignments that are as small as possible becomes crucial, which raises the question of whether such CNF encodings are also effective for enumeration. In this paper, we investigate both theoretically and empirically the effectiveness of CNF conversions for disjoint SAT enumeration. On the negative side, we show that: (i) Tseitin transformation prevents the solver from producing short partial assignments, thus seriously affecting the effectiveness of enumeration; (ii) Plaisted and Greenbaum transformation overcomes this problem only in part. On the positive side, we show that combining Plaisted and Greenbaum transformation with NNF preprocessing upfront - which is typically not used in solving - can fully overcome the problem and can drastically reduce both the number of partial assignments and the execution time.

On CNF Conversion for Disjoint SAT Enumeration / Masina, Gabriele; Spallitta, Giuseppe; Sebastiani, Roberto. - ELETTRONICO. - 271:(2023), pp. 1501-1516. (Intervento presentato al convegno 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023) tenutosi a Alghero, Italia nel 4th-8th July 2023) [10.4230/lipics.sat.2023.15].

On CNF Conversion for Disjoint SAT Enumeration

Masina, Gabriele
;
Spallitta, Giuseppe
;
Sebastiani, Roberto
2023-01-01

Abstract

Modern SAT solvers are designed to handle problems expressed in Conjunctive Normal Form (CNF) so that non-CNF problems must be CNF-ized upfront, typically by using variants of either Tseitin or Plaisted and Greenbaum transformations. When passing from solving to enumeration, however, the capability of producing partial satisfying assignments that are as small as possible becomes crucial, which raises the question of whether such CNF encodings are also effective for enumeration. In this paper, we investigate both theoretically and empirically the effectiveness of CNF conversions for disjoint SAT enumeration. On the negative side, we show that: (i) Tseitin transformation prevents the solver from producing short partial assignments, thus seriously affecting the effectiveness of enumeration; (ii) Plaisted and Greenbaum transformation overcomes this problem only in part. On the positive side, we show that combining Plaisted and Greenbaum transformation with NNF preprocessing upfront - which is typically not used in solving - can fully overcome the problem and can drastically reduce both the number of partial assignments and the execution time.
2023
Leibniz International Proceedings in Informatics (LIPIcs)
Dagstuhl, Germany
Schloss Dagstuhl - Leibniz-Zentrum für Informatik
978-3-95977-286-0
Masina, Gabriele; Spallitta, Giuseppe; Sebastiani, Roberto
On CNF Conversion for Disjoint SAT Enumeration / Masina, Gabriele; Spallitta, Giuseppe; Sebastiani, Roberto. - ELETTRONICO. - 271:(2023), pp. 1501-1516. (Intervento presentato al convegno 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023) tenutosi a Alghero, Italia nel 4th-8th July 2023) [10.4230/lipics.sat.2023.15].
File in questo prodotto:
File Dimensione Formato  
LIPIcs-SAT-2023-15.pdf

accesso aperto

Descrizione: Proceedings paper
Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Creative commons
Dimensione 2.03 MB
Formato Adobe PDF
2.03 MB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/389369
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? ND
social impact