Author name cluster

Amir Aavani

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

1 author row

LPAR Conference 2012 Conference Paper

Enfragmo: A System for Modelling and Solving Search Problems with Logic

Amir Aavani
Xiongnan (Newman) Wu
Shahab Tasharrofi
Eugenia Ternovska
David G. Mitchell

Abstract In this paper, we present the Enfragmo system for specifying and solving combinatorial search problems. It supports natural specification of problems by providing users with a rich language, based on an extension of first order logic. Enfragmo takes as input a problem specification and a problem instance and produces a propositional CNF formula representing solutions to the instance, which is sent to a SAT solver. Because the specification language is high level, Enfragmo provides combinatorial problem solving capability to users without expertise in use of SAT solvers or algorithms for solving combinatorial problems. Here, we describe the specification language and implementation of Enfragmo, and give experimental evidence that its performance is comparable to that of related systems.

Details

SAT Conference 2011 Conference Paper

Translating Pseudo-Boolean Constraints into CNF

Amir Aavani

Abstract A Pseudo-Boolean constraint (PB-constraint) is a generalization of a clause. A PB-constraint is an inequality (equality) on a linear combination of Boolean literals \(\left(\sum_{i=1}^n a_il_i\ OP\ b\right)\) where a 1, ⋯ a n and b are constant integers, l 1, ⋯, l n are literals and OP is a comparison operator. The left-hand side of a PB-constraint under assignment \(\mathcal{A}\) is equal to the sum of the coefficients whose corresponding literals are mapped to true by \(\mathcal{A}\). This kind of constraints has been widely used in expressing NP-complete problems. Several approaches have been proposed to translate a PB-constraint to CNF, [3], [2].

Details