N-level Modulo-Based CNF encodings of Pseudo-Boolean constraints for MaxSAT

Research output: Contribution to journalArticle

Abstract

Many combinatorial problems in various fields can be translated to Maximum Satisfiability (MaxSAT) problems. Although the general problem is NP-hard, more and more practical problems may be solved due to the significant effort which has been devoted to the development of efficient solvers. The art of constraints encoding is as important as the art of devising algorithms for MaxSAT. In this paper, we present several encoding methods of pseudo-Boolean constraints into Boolean satisfiability problems in Conjunctive Normal Form (CNF) formula, which are based on the idea of modular arithmetic and only generate auxiliary variables for each unique combination of weights. These techniques are efficient in encoding and solving MaxSAT problems. In particular, our solvers won the partial MaxSAT industrial category from 2010 through 2012 and ranked second in the 2017 main weighted track of the MaxSAT evaluation. We prove the correctness and the pseudo-polynomial space complexity of our encodings and also give a heuristics of the base selection for modular arithmetic. Our experimental results show that our encoding compactly encodes the constraints, and the obtained clauses are efficiently handled by a state-of-the-art SAT solver.

Original languageEnglish
Pages (from-to)133-161
Number of pages29
JournalConstraints
Volume24
Issue number2
DOIs
Publication statusPublished - Apr 15 2019

Fingerprint

Conjunctive Normal Form
Modulo
Computational complexity
Encoding
Polynomials
Satisfiability Problem
Modular arithmetic
Boolean Satisfiability
Polynomial Complexity
Auxiliary Variables
Space Complexity
Combinatorial Problems
Correctness
NP-complete problem
Heuristics
Partial
Evaluation
Experimental Results

All Science Journal Classification (ASJC) codes

  • Software
  • Discrete Mathematics and Combinatorics
  • Computational Theory and Mathematics
  • Artificial Intelligence

Cite this

N-level Modulo-Based CNF encodings of Pseudo-Boolean constraints for MaxSAT. / Zha, Aolong; Koshimura, Miyuki; Fujita, Hiroshi.

In: Constraints, Vol. 24, No. 2, 15.04.2019, p. 133-161.

Research output: Contribution to journalArticle

@article{47e479d7b25047cb9231288087c9d416,
title = "N-level Modulo-Based CNF encodings of Pseudo-Boolean constraints for MaxSAT",
abstract = "Many combinatorial problems in various fields can be translated to Maximum Satisfiability (MaxSAT) problems. Although the general problem is NP-hard, more and more practical problems may be solved due to the significant effort which has been devoted to the development of efficient solvers. The art of constraints encoding is as important as the art of devising algorithms for MaxSAT. In this paper, we present several encoding methods of pseudo-Boolean constraints into Boolean satisfiability problems in Conjunctive Normal Form (CNF) formula, which are based on the idea of modular arithmetic and only generate auxiliary variables for each unique combination of weights. These techniques are efficient in encoding and solving MaxSAT problems. In particular, our solvers won the partial MaxSAT industrial category from 2010 through 2012 and ranked second in the 2017 main weighted track of the MaxSAT evaluation. We prove the correctness and the pseudo-polynomial space complexity of our encodings and also give a heuristics of the base selection for modular arithmetic. Our experimental results show that our encoding compactly encodes the constraints, and the obtained clauses are efficiently handled by a state-of-the-art SAT solver.",
author = "Aolong Zha and Miyuki Koshimura and Hiroshi Fujita",
year = "2019",
month = "4",
day = "15",
doi = "10.1007/s10601-018-9299-0",
language = "English",
volume = "24",
pages = "133--161",
journal = "Constraints",
issn = "1383-7133",
publisher = "Springer Netherlands",
number = "2",

}

TY - JOUR

T1 - N-level Modulo-Based CNF encodings of Pseudo-Boolean constraints for MaxSAT

AU - Zha, Aolong

AU - Koshimura, Miyuki

AU - Fujita, Hiroshi

PY - 2019/4/15

Y1 - 2019/4/15

N2 - Many combinatorial problems in various fields can be translated to Maximum Satisfiability (MaxSAT) problems. Although the general problem is NP-hard, more and more practical problems may be solved due to the significant effort which has been devoted to the development of efficient solvers. The art of constraints encoding is as important as the art of devising algorithms for MaxSAT. In this paper, we present several encoding methods of pseudo-Boolean constraints into Boolean satisfiability problems in Conjunctive Normal Form (CNF) formula, which are based on the idea of modular arithmetic and only generate auxiliary variables for each unique combination of weights. These techniques are efficient in encoding and solving MaxSAT problems. In particular, our solvers won the partial MaxSAT industrial category from 2010 through 2012 and ranked second in the 2017 main weighted track of the MaxSAT evaluation. We prove the correctness and the pseudo-polynomial space complexity of our encodings and also give a heuristics of the base selection for modular arithmetic. Our experimental results show that our encoding compactly encodes the constraints, and the obtained clauses are efficiently handled by a state-of-the-art SAT solver.

AB - Many combinatorial problems in various fields can be translated to Maximum Satisfiability (MaxSAT) problems. Although the general problem is NP-hard, more and more practical problems may be solved due to the significant effort which has been devoted to the development of efficient solvers. The art of constraints encoding is as important as the art of devising algorithms for MaxSAT. In this paper, we present several encoding methods of pseudo-Boolean constraints into Boolean satisfiability problems in Conjunctive Normal Form (CNF) formula, which are based on the idea of modular arithmetic and only generate auxiliary variables for each unique combination of weights. These techniques are efficient in encoding and solving MaxSAT problems. In particular, our solvers won the partial MaxSAT industrial category from 2010 through 2012 and ranked second in the 2017 main weighted track of the MaxSAT evaluation. We prove the correctness and the pseudo-polynomial space complexity of our encodings and also give a heuristics of the base selection for modular arithmetic. Our experimental results show that our encoding compactly encodes the constraints, and the obtained clauses are efficiently handled by a state-of-the-art SAT solver.

UR - http://www.scopus.com/inward/record.url?scp=85060064095&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85060064095&partnerID=8YFLogxK

U2 - 10.1007/s10601-018-9299-0

DO - 10.1007/s10601-018-9299-0

M3 - Article

AN - SCOPUS:85060064095

VL - 24

SP - 133

EP - 161

JO - Constraints

JF - Constraints

SN - 1383-7133

IS - 2

ER -