Commits · master · Jakub Janků / vw-passat

Jun 13, 2024
- fix: make sure all proof data is written out · fec85a72
  Jakub Janků authored Jun 13, 2024
  
  fec85a72
- use clap for parsing args · 00cdf6fc
  Jakub Janků authored Jun 13, 2024
  
  00cdf6fc
- fix possible overflow in cube generation · e5ad8991
  Jakub Janků authored Jun 13, 2024
  
  e5ad8991
- fix formatting of test files · 25afa6e6
  Jakub Janků authored Jun 13, 2024
  
  25afa6e6
May 19, 2024
- add final remarks to readme · 4689b0ee
  Jakub Janků authored May 19, 2024
  
  4689b0ee
May 18, 2024
- add new results · 479a0009
  Jakub Janků authored May 18, 2024
  
  479a0009
- use one codegen unit, abort on panic · 575ff7ce
  Jakub Janků authored May 18, 2024
  
  575ff7ce
- use much less aggressive restart multiplier · 1ffe19d3
  Jakub Janků authored May 18, 2024
  
  1ffe19d3
- add performance analysis script and current results · c07e53bc
  Jakub Janků authored May 18, 2024
  
  c07e53bc
May 17, 2024
- add basic clause minimization · 62d28dd1
  Jakub Janků authored Apr 21, 2024
  
  62d28dd1
- add clause forgetting · 967157f9
  Jakub Janků authored Apr 04, 2024
  
  967157f9
- extend readme with implemented functionality · 86b5863b
  Jakub Janků authored May 17, 2024
  
  86b5863b
- refer to --help in readme · 1b37e107
  Jakub Janků authored May 17, 2024
  
  1b37e107
- test proofs for sat formulas · a93822d9
  Jakub Janků authored Apr 25, 2024
```
Older drat-trim must be used, see
https://github.com/marijnheule/drat-trim/issues/35
```
  a93822d9
- optionally write benchmark results to a csv · 7f5a31fb
  Jakub Janků authored May 17, 2024
  
  7f5a31fb
- allow specifying -j in benchmarks · f9901e31
  Jakub Janků authored May 17, 2024
  
  f9901e31
Apr 21, 2024
- add phase saving · 37528013
  Jakub Janků authored Apr 21, 2024
  
  37528013
- add optional proof generation · 5c42f783
  Jakub Janků authored Apr 16, 2024
  
  5c42f783
Apr 20, 2024
- move io.rs to io/mod.rs · ad88f838
  Jakub Janků authored Apr 15, 2024
  
  ad88f838
- allow setting the number of used threads via cli · 28b9af91
  Jakub Janků authored Apr 20, 2024
  
  28b9af91
- improve argument parsing · 51cb5136
  Jakub Janků authored Apr 20, 2024
  
  51cb5136
Apr 15, 2024
- fix: dedup input clauses · 5a71a942
  Jakub Janků authored Apr 15, 2024
  
  5a71a942
Apr 02, 2024
- add parallelism · e172b3ec
  Jakub Janků authored Apr 02, 2024
  
  e172b3ec
Mar 30, 2024
- expand tests to clauses with 100 vars · a4b9a98b
  Jakub Janků authored Mar 30, 2024
  
  a4b9a98b
- add ci test job · 77fddafd
  Jakub Janků authored Mar 30, 2024
  
  77fddafd
Mar 29, 2024
- add varmap · b66e175e
  Jakub Janků authored Mar 29, 2024
  
  b66e175e
- rename chooser to evsids · 780841b8
  Jakub Janků authored Mar 29, 2024
  
  780841b8
- move var type to types · f3518561
  Jakub Janků authored Mar 29, 2024
  
  f3518561
- split solver into submodules · 7d236079
  Jakub Janků authored Mar 29, 2024
  
  7d236079
- implement restarts · de2d4bf0
  Jakub Janků authored Mar 29, 2024
  
  de2d4bf0
- benchmark: add dir filtering · 337d9171
  Jakub Janků authored Mar 29, 2024
  
  337d9171
Mar 26, 2024
- implement evsids · a03da5f8
  Jakub Janků authored Mar 26, 2024
  
  a03da5f8
Mar 25, 2024
- apply clippy suggestions · 3602d2c6
  Jakub Janků authored Mar 25, 2024
  
  3602d2c6
- add a simple benchmarking script · 69d90b0a
  Jakub Janků authored Mar 25, 2024
```
plus more data to test on.
```
  69d90b0a
Mar 24, 2024
- fix: setup watched literals for learnt clauses · 7c6d73bb
  Jakub Janků authored Mar 24, 2024
  
  7c6d73bb
- fix: handle percent sign in satlib's cnf files · 8c693690
  Jakub Janků authored Mar 24, 2024
  
  8c693690
- test solver using satlib's uniform random benchmark · 84d6389f
  Jakub Janků authored Mar 24, 2024
```
https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html
```
  84d6389f
- readme: add build/run instructions · cccabb40
  Jakub Janků authored Mar 24, 2024
  
  cccabb40
- add initial cdcl impl · ce43178f
  Jakub Janků authored Mar 24, 2024
```
Likely contains some issues.
```
  ce43178f
Mar 23, 2024
- refactor: group assignment, trail, and decisions · 2a66b378
  Jakub Janků authored Mar 23, 2024
  
  2a66b378