Tyck till om SwePub Sök
här!
Sökning: onr:"swepub:oai:gup.ub.gu.se/74331" >
Translating Pseudo-...
Translating Pseudo-Boolean Constraints into SAT
-
- Een, Niklas, 1973 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- Sörensson, Niklas, 1977 (författare)
- Gothenburg University,Göteborgs universitet,Institutionen för data- och informationsteknik, datavetenskap (GU),Department of Computer Science and Engineering, Computing Science (GU),University of Gothenburg
-
(creator_code:org_t)
- 2005
- 2005
- Engelska.
-
Ingår i: Journal on Satisfiability, Boolean Modeling and Computation, Special Volume on the SAT 2005 competitions and evaluationsEditors: Daniel Le Berre and Laurent Simon. - 1574-0617. ; 2, s. 1-26
- Relaterad länk:
-
https://gup.ub.gu.se...
-
visa fler...
-
https://research.cha...
-
visa färre...
Abstract
Ämnesord
Stäng
- In this paper, we describe and evaluate three different techniques for translating pseudo-boolean constraints (linear constraints over boolean variables) into clauses that can be handled by a standard SAT-solver. We show that by applying a proper mix of translation techniques, a SAT-solver can perform on a par with the best existing native pseudo-boolean solvers. This is particularly valuable in those cases where the constraint problem of interest is naturally expressed as a SAT problem, except for a handful of constraints.Translating those constraints to get a pure clausal problem will take full advantage of the latest improvements in SAT research. A particularly interesting result of this work is the efficiency of sorting networks to express pseudo-boolean constraints. Although tangential to this presentation, the result gives a suggestion as to how synthesis tools may be modified to produce arithmetic circuits more suitable for SAT based reasoning.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- pseudo-Boolean
- SAT-solver
- SAT translation
- integer linear programming
- integer linear programming
Publikations- och innehållstyp
- ref (ämneskategori)
- art (ämneskategori)
Hitta via bibliotek
Till lärosätets databas