In this paper, we describe and evaluate three different techniques for translating pseudoboolean constraints (linear constraints over boolean variables) into clauses that can be h...
Many SAT instances can be decomposed into connected components either initially after preprocessing or during the solution phase when new unit conflict clauses are learned. This o...
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 p...
A family of satisfiable benchmark instances in conjunctive normal form is introduced. The instances are constructed by transforming a random regular graph into a system of linear ...
This paper analyzes the SAT05 solver competition on industrial instances. We carefully investigate the performance of solvers from the competition and demonstration categories. We...
This paper introduces a new hybrid method for efficiently integrating Pseudo-Boolean (PB) constraints into generic SAT solvers in order to solve PB satisfiability and optimization...
Cutting planes are a well-known, widely used, and very effective technique for Integer Linear Programming (ILP). However, cutting plane techniques are seldom used in PseudoBoolean...
An analysis of the SAT 2005 sub-competition on random instances is given. This year this (sub-)competition set-up was geared to establish a basic setting, focusing on the instance...
In this note we construct a family of SAT-instance based on Eulerian graphs which are aimed at being hard for resolution based SAT-solvers. We discuss some experiments made with i...
The first evaluation of pseudo-Boolean solvers was organized as a subtrack of the SAT 2005 competition. The first goal of this event is to take a snapshot of the current state of ...