The Silent (R)evolution of SAT
The propositional satisfiability problem (SAT) was the first problem to be shown NP-complete by Cook and Levin. SAT remained the embodiment of theoretical worst-case hardness. However, in stark contrast to its theoretical hardness, the SAT problem has emerged as an essential tool for efficiently sol...
| Main Authors: | , , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | English |
| Published: |
ACM|Communications of the ACM
2023
|
| Online Access: | https://hdl.handle.net/1721.1/150840 |
| _version_ | 1826213231140536320 |
|---|---|
| author | Hecher, Markus Fichte, Johannes Le Berre, Daniel Szeider, Stefan |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Hecher, Markus Fichte, Johannes Le Berre, Daniel Szeider, Stefan |
| author_sort | Hecher, Markus |
| collection | MIT |
| description | The propositional satisfiability problem (SAT) was the first problem to be shown NP-complete by Cook and Levin. SAT remained the embodiment of theoretical worst-case hardness. However, in stark contrast to its theoretical hardness, the SAT problem has emerged as an essential tool for efficiently solving a wide variety of computational problems. SAT solving technology has continuously advanced since a breakthrough around the millennium, which catapulted practical SAT solving by orders of magnitudes ahead. Today, the many flavors of SAT technology can be found in all areas of technological innovation. |
| first_indexed | 2024-09-23T15:45:31Z |
| format | Article |
| id | mit-1721.1/150840 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2024-09-23T15:45:31Z |
| publishDate | 2023 |
| publisher | ACM|Communications of the ACM |
| record_format | dspace |
| spelling | mit-1721.1/1508402024-01-05T21:10:50Z The Silent (R)evolution of SAT Hecher, Markus Fichte, Johannes Le Berre, Daniel Szeider, Stefan Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory The propositional satisfiability problem (SAT) was the first problem to be shown NP-complete by Cook and Levin. SAT remained the embodiment of theoretical worst-case hardness. However, in stark contrast to its theoretical hardness, the SAT problem has emerged as an essential tool for efficiently solving a wide variety of computational problems. SAT solving technology has continuously advanced since a breakthrough around the millennium, which catapulted practical SAT solving by orders of magnitudes ahead. Today, the many flavors of SAT technology can be found in all areas of technological innovation. 2023-06-01T20:15:09Z 2023-06-01T20:15:09Z 2023-05-24 2023-06-01T07:46:06Z Article http://purl.org/eprint/type/JournalArticle 0001-0782 https://hdl.handle.net/1721.1/150840 Hecher, Markus, Fichte, Johannes, Le Berre, Daniel and Szeider, Stefan. 2023. "The Silent (R)evolution of SAT." PUBLISHER_POLICY en https://doi.org/10.1145/3560469 Article is made available in accordance with the publisher's policy and may be subject to US copyright law. Please refer to the publisher's site for terms of use. The author(s) application/pdf ACM|Communications of the ACM Association for Computing Machinery |
| spellingShingle | Hecher, Markus Fichte, Johannes Le Berre, Daniel Szeider, Stefan The Silent (R)evolution of SAT |
| title | The Silent (R)evolution of SAT |
| title_full | The Silent (R)evolution of SAT |
| title_fullStr | The Silent (R)evolution of SAT |
| title_full_unstemmed | The Silent (R)evolution of SAT |
| title_short | The Silent (R)evolution of SAT |
| title_sort | silent r evolution of sat |
| url | https://hdl.handle.net/1721.1/150840 |
| work_keys_str_mv | AT hechermarkus thesilentrevolutionofsat AT fichtejohannes thesilentrevolutionofsat AT leberredaniel thesilentrevolutionofsat AT szeiderstefan thesilentrevolutionofsat AT hechermarkus silentrevolutionofsat AT fichtejohannes silentrevolutionofsat AT leberredaniel silentrevolutionofsat AT szeiderstefan silentrevolutionofsat |