View Related Documents

Abstract

This paper describes how to model and solve boolean satisfiability problems with the constraint logic programming language CHIP. Although CHIP has not been developed as a specialised propositional calculus prover, it can solve these problems quite efficiently. Several different methods of describing satisfiability problems in CHIP are presented and compared. This flexibility of modelling is a major advantage of CHIP over closed problem solvers. We have evaluated various sets of benchmarks taken from [31] [16] [21]. With one exception, CHIP performs as well or better as specialised programs on these examples. We also shortly discuss an alternative modeling technique using finite domain variables not restricted to 0/1 values.

Fulltext Preview

Image of the first page of the fulltext document