Timeline for Mathematica vs. state-of-the-art SAT solvers
Current License: CC BY-SA 4.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 28, 2023 at 18:24 | comment | added | Steffen Jaeschke | SAT Competition did change, at present it is: SAT Competition. | |
| S Jul 24, 2019 at 8:01 | history | bounty ended | CommunityBot | ||
| S Jul 24, 2019 at 8:01 | history | notice removed | CommunityBot | ||
| Jul 20, 2019 at 10:28 | comment | added | Ronald Monson |
... for use in verifying unsatisfiability claims but which seems absent as an option in SatisfiabilityInstances?). Alternatively, providing some benchmarks in the question would allow comparative answers - a natural starting point might be the paper’s SAT encodings generated by a WL-version of the (19-line C) encodings provided by the authors in the file Ptn-encode.
|
|
| Jul 20, 2019 at 10:27 | comment | added | Ronald Monson | ... the SAT (CNF) instances that encode the unavoidablity of monochromatic pythagorean triples are reminiscent of random CNF formulae). To compare Mathematica’s SATSolver you could use the benchmarks provided in the 2018 SAT Competition where, given this competition’s history Maple’s SATSolver(s) seems to be laying down the gauntlet which might pique WRI’s interest … (Another indicator of state-of-the-art solvers is the ability to generate so-called DRAT proof files ... | |
| Jul 20, 2019 at 10:26 | comment | added | Ronald Monson | Mathematica claims "industrial strength" Boolean computation so its SATSolver should be doing better than "brute force". On the other hand, SATSolvers tend to specialise on formulae type (satisfiable, unsatisfiable, random, etc) or available resources (time, space, parallelization) or especially, exploiting a domain's structure, so it might be optimistic to hope for leading-edge performance across the board (curiously, in Heule, Kullman and Marek’s breakthrough paper mentioned in the OP’s introduction, after colouring the natural numbers red and blue ... | |
| S Jul 16, 2019 at 6:35 | history | bounty started | Mario Krenn | ||
| S Jul 16, 2019 at 6:35 | history | notice added | Mario Krenn | Authoritative reference needed | |
| Jul 14, 2019 at 13:07 | history | edited | Henrik Schumacher | CC BY-SA 4.0 |
deleted 5 characters in body
|
| Jul 14, 2019 at 12:59 | comment | added | Szabolcs | But it should be easy to put problems into a conjunctive normal form, export them, and ty other SAT solvers. | |
| Jul 14, 2019 at 12:56 | comment | added | Szabolcs | I am not very familiar with SAT solvers, but I did experiment with other solvers (such as glucose) when developing the graph colouring functionality of IGraph/M. Using them did not give a consistent or significant speedup compared to using Mathematica's. | |
| Jul 14, 2019 at 9:00 | history | tweeted | twitter.com/StackMma/status/1150329220163416064 | ||
| Jul 14, 2019 at 3:17 | history | edited | Mario Krenn | CC BY-SA 4.0 |
added 312 characters in body
|
| Jul 14, 2019 at 3:07 | history | asked | Mario Krenn | CC BY-SA 4.0 |