- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- BIRS Workshop Lecture Videos /
- Towards Faster Conflict-Driven Pseudo-Boolean Solving
Open Collections
BIRS Workshop Lecture Videos
BIRS Workshop Lecture Videos
Towards Faster Conflict-Driven Pseudo-Boolean Solving Nordstrom, Jakob
Description
The last 20 years have seen dramatic improvements in the performance
of algorithms for Boolean satisfiability---so-called SAT solvers---and
today conflict-driven clause learning (CDCL) solvers are routinely
used in a wide range of application areas. One serious short-coming
of CDCL, however, is that the underlying method of reasoning is quite
weak. A tantalizing solution is to instead use stronger
pseudo-Boolean (PB) reasoning (a.k.a. 0-1 integer linear programming),
but so far the promise of exponential gains in performance has mostly
failed to materialize---the increased theoretical strength seems hard
to harness algorithmically, and in many applications CDCL-based
methods are still superior.
In this talk, we will discuss conflict-driven search and how to lift
it from clauses to pseudo-Boolean linear constraints. We will survey
the "classic" method in [Chai and Kuehlmann '05] based on saturation,
and then describe a relatively new approach from [Elffers and
Nordström '18] instead using division. We will also try to highlight
some of the obstacles that remain along the path to truly efficient
pseudo-Boolean solvers.
Item Metadata
| Title |
Towards Faster Conflict-Driven Pseudo-Boolean Solving
|
| Creator | |
| Publisher |
Banff International Research Station for Mathematical Innovation and Discovery
|
| Date Issued |
2018-08-28T09:04
|
| Description |
The last 20 years have seen dramatic improvements in the performance
of algorithms for Boolean satisfiability---so-called SAT solvers---and
today conflict-driven clause learning (CDCL) solvers are routinely
used in a wide range of application areas. One serious short-coming
of CDCL, however, is that the underlying method of reasoning is quite
weak. A tantalizing solution is to instead use stronger
pseudo-Boolean (PB) reasoning (a.k.a. 0-1 integer linear programming),
but so far the promise of exponential gains in performance has mostly
failed to materialize---the increased theoretical strength seems hard
to harness algorithmically, and in many applications CDCL-based
methods are still superior.
In this talk, we will discuss conflict-driven search and how to lift it from clauses to pseudo-Boolean linear constraints. We will survey the "classic" method in [Chai and Kuehlmann '05] based on saturation, and then describe a relatively new approach from [Elffers and Nordström '18] instead using division. We will also try to highlight some of the obstacles that remain along the path to truly efficient pseudo-Boolean solvers. |
| Extent |
65.0
|
| Subject | |
| Type | |
| File Format |
video/mp4
|
| Language |
eng
|
| Notes |
Author affiliation: KTH Royal Institute of Technology
|
| Series | |
| Date Available |
2019-03-31
|
| Provider |
Vancouver : University of British Columbia Library
|
| Rights |
Attribution-NonCommercial-NoDerivatives 4.0 International
|
| DOI |
10.14288/1.0377703
|
| URI | |
| Affiliation | |
| Peer Review Status |
Unreviewed
|
| Scholarly Level |
Faculty
|
| Rights URI | |
| Aggregated Source Repository |
DSpace
|
Item Media
Item Citations and Data
Rights
Attribution-NonCommercial-NoDerivatives 4.0 International