You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

A Translation of Pseudo-Boolean Constraints to SAT

Issue title: SAT 2005 Competitions and Evaluations

Guest editors: Daniel Le Berre and Laurent Simon

Article type: Research Article

Authors: Bailleux, Oliviera | Boufkhad, Yacineb | Roussel, Olivierc

Affiliations: [a] Université de Bourgogne – LERSIA, Avenue Alain Savary – BP 47870, F-21078 Dijon Cedex – France. E-mail: [email protected] | [b] LIAFA – Université Denis Diderot – Case 7014, 2, place Jussieu, F-75251 Paris Cedex 05 – France. E-mail: [email protected] | [c] CRIL, rue de l’Université – SP 16, F-62307 Lens Cedex – France. E-mail: [email protected]

Keywords: pseudo-Boolean, SAT translation

DOI: 10.3233/SAT190021

Journal: Journal on Satisfiability, Boolean Modeling and Computation, vol. 2, no. 1-4, pp. 191-200, 2006

Received 1 October 2005
|
Revision received 1 January 2006
|
Published: 1 March 2006
Get PDF open access

Abstract

This paper introduces a new CNF encoding of pseudo-Boolean constraints, which allows unit propagation to maintain generalized arc consistency. In the worst case, the size of the produced formula can be exponentially related to the size of the input constraint, but some important classes of pseudo-Boolean constraints, including Boolean cardinality constraints, are encoded in polynomial time and size. The proposed encoding was integrated in a solver based on the zChaff SAT solver and submitted to the PB05 evaluation. The results provide new perspectives in the field of full CNF approach of pseudo-Boolean constraints solving.

Show more