Skip to content

Commit

Permalink
Merge branch 'main' of github.com:logic-and-learning-lab/Popper
Browse files Browse the repository at this point in the history
  • Loading branch information
andrewcropper committed Jun 25, 2024
2 parents 690d730 + 1707e6d commit 1903c44
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -139,16 +139,16 @@ To enable PI, add the setting `enable_pi.` to the bias file. However, predicate
#### Solvers
Popper uses various MaxSAT solvers. By default, Popper uses the [RC2](https://alexeyignatiev.github.io/assets/pdf/imms-jsat19-preprint.pdf) exact solver provided by PySAT. Popper also supports these solvers:

- UWrMaxSat (exact)
- [UWrMaxSat](https://github.com/marekpiotrow/UWrMaxSat) (exact)
- WMaxCDCL (exact)
- NuWLS (anytime)
- [NuWLS](https://ojs.aaai.org/index.php/AAAI/article/view/25505) (anytime)

You can download and compile these solvers from the [MaxSAT 2023 evaluation](https://maxsat-evaluations.github.io/2023/descriptions.html) website.
**We strongly recommend using the anytime NuWLS** solver as it greatly improves the performance of Popper. To use them, ensure that the solver is available on your path. See the [install solvers](solvers.md) file for help.

#### Performance tips
- Transform your BK to Datalog, which allows Popper to perform preprocessing on the BK
- Use one of the MaxSAT solvers, above, especially the NuWLS anytime solver.
- Try the NuWLS anytime solver.
- Use 6 variables or fewer
- Avoid recursion and predicate invention

Expand Down

0 comments on commit 1903c44

Please sign in to comment.