Showing 1–4 of 4 results for author: Metodi, A

Boolean Equi-propagation for Concise and Efficient SAT Encodings of Combinatorial Problems

Authors: Amit Metodi, Michael Codish, Peter James Stuckey

Abstract: We present an approach to propagation-based SAT encoding of combinatorial problems, Boolean equi-propagation, where constraints are modeled as Boolean functions which propagate information about equalities between Boolean literals. This information is then applied to simplify the CNF encoding of the constraints. A key factor is that considering only a small fragment of a constraint model at one… ▽ More We present an approach to propagation-based SAT encoding of combinatorial problems, Boolean equi-propagation, where constraints are modeled as Boolean functions which propagate information about equalities between Boolean literals. This information is then applied to simplify the CNF encoding of the constraints. A key factor is that considering only a small fragment of a constraint model at one time enables us to apply stronger, and even complete, reasoning to detect equivalent literals in that fragment. Once detected, equivalences apply to simplify the entire constraint model and facilitate further reasoning on other fragments. Equi-propagation in combination with partial evaluation and constraint simplification provide the foundation for a powerful approach to SAT-based finite domain constraint solving. We introduce a tool called BEE (Ben-Gurion Equi-propagation Encoder) based on these ideas and demonstrate for a variety of benchmarks that our approach leads to a considerable reduction in the size of CNF encodings and subsequent speed-ups in SAT solving times. △ Less

Submitted 3 February, 2014; originally announced February 2014.

Comments: arXiv admin note: text overlap with arXiv:1206.3883

Journal ref: Journal Of Artificial Intelligence Research, Volume 46, pages 303-341, 2013

Compiling Finite Domain Constraints to SAT with BEE: the Director's Cut

Authors: Michael Codish, Yoav Fekete, Amit Metodi

Abstract: BEE is a compiler which facilitates solving finite domain constraints by encoding them to CNF and applying an underlying SAT solver. In BEE constraints are modeled as Boolean functions which propagate information about equalities between Boolean literals. This information is then applied to simplify the CNF encoding of the constraints. We term this process equi-propagation. A key factor is that co… ▽ More BEE is a compiler which facilitates solving finite domain constraints by encoding them to CNF and applying an underlying SAT solver. In BEE constraints are modeled as Boolean functions which propagate information about equalities between Boolean literals. This information is then applied to simplify the CNF encoding of the constraints. We term this process equi-propagation. A key factor is that considering only a small fragment of a constraint model at one time enables to apply stronger, and even complete reasoning to detect equivalent literals in that fragment. Once detected, equivalences propagate to simplify the entire constraint model and facilitate further reasoning on other fragments. BEE is described in several recent papers. In this paper, after a quick review of BEE, we elaborate on two undocumented details of the implementation: the hybrid encoding of cardinality constraints and complete equi-propagation. We thendescribe on-going work aimed to extend BEE to consider binary representation of numbers. △ Less

Submitted 19 August, 2013; originally announced August 2013.

Comments: Part of WLPE 2013 proceedings (arXiv:1308.2055)

Report number: WLPE/2013/1

Compiling Finite Domain Constraints to SAT with BEE

Authors: Amit Metodi, Michael Codish

Abstract: We present BEE, a compiler which enables to encode finite domain constraint problems to CNF. Using BEE both eases the encoding process for the user and also performs transformations to simplify constraints and optimize their encoding to CNF. These optimizations are based primarily on equi-propagation and on partial evaluation, and also on the idea that a given constraint may have various possible… ▽ More We present BEE, a compiler which enables to encode finite domain constraint problems to CNF. Using BEE both eases the encoding process for the user and also performs transformations to simplify constraints and optimize their encoding to CNF. These optimizations are based primarily on equi-propagation and on partial evaluation, and also on the idea that a given constraint may have various possible CNF encodings. Often, the better encoding choice is made after constraint simplification. BEE is written in Prolog and integrates directly with a SAT solver through a suitable Prolog interface. We demonstrate that constraint simplification is often highly beneficial when solving hard finite domain constraint problems. A BEE implementation is available with this paper. △ Less

Submitted 18 June, 2012; originally announced June 2012.

Boolean Equi-propagation for Optimized SAT Encoding

Authors: Amit Metodi, Michael Codish, Vitaly Lagoon, Peter J. Stuckey

Abstract: We present an approach to propagation based solving, Boolean equi-propagation, where constraints are modelled as propagators of information about equalities between Boolean literals. Propagation based solving applies this information as a form of partial evaluation resulting in optimized SAT encodings. We demonstrate for a variety of benchmarks that our approach results in smaller CNF encodings an… ▽ More We present an approach to propagation based solving, Boolean equi-propagation, where constraints are modelled as propagators of information about equalities between Boolean literals. Propagation based solving applies this information as a form of partial evaluation resulting in optimized SAT encodings. We demonstrate for a variety of benchmarks that our approach results in smaller CNF encodings and leads to speed-ups in solving times. △ Less

Submitted 24 April, 2011; originally announced April 2011.