Linear Ordering in the SAT Encoding of the All-Different Constraint over Bit-Vectors

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F15%3A10319561" target="_blank" >RIV/00216208:11320/15:10319561 - isvavai.cz</a>

Výsledek na webu

<a href="http://www.cs.nmsu.edu/ALP/2015/03/linear-ordering-in-the-sat-encoding-of-the-all-different-constraint-over-bit-vectors/" target="_blank" >http://www.cs.nmsu.edu/ALP/2015/03/linear-ordering-in-the-sat-encoding-of-the-all-different-constraint-over-bit-vectors/</a>

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Linear Ordering in the SAT Encoding of the All-Different Constraint over Bit-Vectors

Popis výsledku v původním jazyce

A novel eager encoding of the ALLDIFFERENT constraint over bit-vectors is presented in this short paper. It is based on 1-to-1 mapping of the input bit-vectors to a linearly ordered set of auxiliary bit-vectors. Experiments with four SAT solvers showed that the new encoding could be solved order of magnitudes faster than the standard encoding in a hard unsatisfiable case.

Název v anglickém jazyce

Linear Ordering in the SAT Encoding of the All-Different Constraint over Bit-Vectors

Popis výsledku anglicky

A novel eager encoding of the ALLDIFFERENT constraint over bit-vectors is presented in this short paper. It is based on 1-to-1 mapping of the input bit-vectors to a linearly ordered set of auxiliary bit-vectors. Experiments with four SAT solvers showed that the new encoding could be solved order of magnitudes faster than the standard encoding in a hard unsatisfiable case.

Druh

O - Ostatní výsledky

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2015

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů