Skip to content

Commit 1903c44

Browse files
committed
Merge branch 'main' of github.com:logic-and-learning-lab/Popper
2 parents 690d730 + 1707e6d commit 1903c44

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

README.md

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -139,16 +139,16 @@ To enable PI, add the setting `enable_pi.` to the bias file. However, predicate
139139
#### Solvers
140140
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:
141141

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

146146
You can download and compile these solvers from the [MaxSAT 2023 evaluation](https://maxsat-evaluations.github.io/2023/descriptions.html) website.
147147
**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.
148148

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

0 commit comments

Comments
 (0)