THE SOLUTION OF DISCRETE CONSTRAINT PROBLEMS USING BOOLEAN MODELS - The Use of Ternary Vectors for Parallel SAT-Solving

Christian Posthoff, Bernd Steinbach

2010

Abstract

The use of Boolean models for discrete constraint problems has been tried at several occasions, it was, however, not recognized as efficient (Rossi et al., 2006). The solution methods were dominated by using decision trees together with depth-first or breadth-first search and/or resolution algorithms. In this paper we will show the use of ternary vectors for the solution of SAT-problems and all the problems that can be modeled by means of SAT-equations. They are an appropriate data structure representing sets of Boolean vectors. They also allow to include problem-relevant knowledge into the problem-solving process at an early point of time. The respective set operations (mainly the intersection) can be executed in a bit-parallel way (64 bits at present). For larger problems the processing can be transferred to processors working fully in parallel. There is no need for any search algorithms. The approach always finds all solutions of the problem without consideration of special cases (i.e. no solution, one solution, all solutions). Some examples are used to illustrate the approach or have been published before (Sudoku, Queen's problems on the chessboard, node bases in graphs, graph-coloring problems).

Paper Citation

in Harvard Style

Posthoff C. and Steinbach B. (2010). THE SOLUTION OF DISCRETE CONSTRAINT PROBLEMS USING BOOLEAN MODELS - The Use of Ternary Vectors for Parallel SAT-Solving . In Proceedings of the 2nd International Conference on Agents and Artificial Intelligence - Volume 1: ICAART, ISBN 978-989-674-021-4, pages 487-493. DOI: 10.5220/0002703804870493

in Bibtex Style

@conference{icaart10,
author={Christian Posthoff and Bernd Steinbach},
title={THE SOLUTION OF DISCRETE CONSTRAINT PROBLEMS USING BOOLEAN MODELS - The Use of Ternary Vectors for Parallel SAT-Solving},
booktitle={Proceedings of the 2nd International Conference on Agents and Artificial Intelligence - Volume 1: ICAART,},
year={2010},
pages={487-493},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0002703804870493},
isbn={978-989-674-021-4},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 2nd International Conference on Agents and Artificial Intelligence - Volume 1: ICAART,
TI - THE SOLUTION OF DISCRETE CONSTRAINT PROBLEMS USING BOOLEAN MODELS - The Use of Ternary Vectors for Parallel SAT-Solving
SN - 978-989-674-021-4
AU - Posthoff C.
AU - Steinbach B.
PY - 2010
SP - 487
EP - 493
DO - 10.5220/0002703804870493