Optimal base encodings for pseudo-Boolean constraints

DOI10.1007/978-3-642-19835-9_16MaRDI QIDQ3000648zbMATH OpenOpenAlexFDO

Authors Michael Codish, Yoav Fekete, Carsten Fuhs, Peter Schneider-Kamp

Publication date 19 May 2011

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1007.4935

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Abstract: This paper formalizes the optimal base problem, presents an algorithm to solve it, and describes its application to the encoding of Pseudo-Boolean constraints to SAT. We demonstrate the impact of integrating our algorithm within the Pseudo-Boolean constraint solver MINISAT+. Experimentation indicates that our algorithm scales to bases involving numbers up to 1,000,000, improving on the restriction in MINISAT+ to prime numbers up to 17. We show that, while for many examples primes up to 17 do suffice, encoding with respect to optimal bases reduces the CNF sizes and improves the subsequent SAT solving time for many examples.

Recommendations

• \(N\)-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT
• Simplifying pseudo-Boolean constraints in residual number systems
• scientific article; zbMATH DE number 5139168
• New Encodings of Pseudo-Boolean Constraints into CNF
• PBLib -- a library for encoding pseudo-Boolean constraints into CNF

Cites work

• scientific article; zbMATH DE number 5139161 (Why is no real title available?)
• scientific article; zbMATH DE number 5139165 (Why is no real title available?)
• scientific article; zbMATH DE number 5139168 (Why is no real title available?)
• scientific article; zbMATH DE number 3473265 (Why is no real title available?)
• Logic-based 0-1 constraint programming
• New Encodings of Pseudo-Boolean Constraints into CNF
• On the number of ordered factorizations of natural numbers
• Optimal base encodings for pseudo-Boolean constraints
• Sum-of-digits function for certain nonstationary bases

Cited in

(9)

• SAT encodings for pseudo-Boolean constraints together with at-most-one constraints
• Optimal base encodings for pseudo-Boolean constraints
• PBLib -- a library for encoding pseudo-Boolean constraints into CNF
• Improving the normalization of weight rules in answer set programs
• Simplifying pseudo-Boolean constraints in residual number systems
• BDDs for pseudo-Boolean constraints -- revisited
• Rewriting optimization statements in answer-set programs
• Learning to select SAT encodings for pseudo-Boolean and linear Integer constraints
• \(N\)-level modulo-based CNF encodings of pseudo-Boolean constraints for MaxSAT

Describes a project that uses

Uses Software

• MIPLIB
• OPBDP

This page was built for publication: Optimal base encodings for pseudo-Boolean constraints

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3000648)