Many of the existing knowledge compilation tools focus on the purely propositional logic setting. These propositional tools are also usable for applications that involve a background theory. For instance, weighted model integration (WMI) is a task that may involve linear real arithmetic formulas such as (x + y > 2).

Variable Ordering heuristics

The variable ordering heuristics used within knowledge compilers typically focus on obtaining succinct representations. When these compilers are used within the WMI application however, the goals are different due to the integration operation. We studied this in our conference publication Ordering Variables for Weighted Model Integration, and proposed several new heuristics that significantly improve the run time required for solving WMI tasks. You can find relevant code at the pywmi and BU-MiF repositories.


@inproceedings{Derkinderen2020order,
  author       = {Vincent Derkinderen and
                  Evert Heylen and
                  Pedro {Zuidberg Dos Martires} and
                  Samuel Kolb and
                  Luc {De Raedt}},
  title        = {Ordering Variables for Weighted Model Integration},
  booktitle    = {{UAI}},
  series       = {Proceedings of Machine Learning Research},
  volume       = {124},
  pages        = {879--888},
  publisher    = {{AUAI} Press},
  year         = {2020}
}

Theory aware knowledge compilation

The use of purely propositional tools for tasks that involve background theories introduces inefficiencies. For example, the propositional tools might not realise that (x < 0) and (x > 1) are mutually exclusive constraints, unless the user explicitly encodes this information and passes it to the tool.

We therefore investigated several approaches to knowledge compilation that is theory aware, and specifically advocate for a top-down compiler based on the traces of exchaustive DPLL(T) search. More information on this is provided in our article Top-Down Knowledge Compilation for Counting Modulo Theories


@article{Derkinderen2023modcomp,
  author       = {Vincent Derkinderen and
                  Pedro {Zuidberg Dos Martires} and
                  Samuel Kolb and
                  Paolo Morettin},
  title        = {Top-Down Knowledge Compilation for Counting Modulo Theories},
  journal      = {CoRR},
  volume       = {abs/2306.04541},
  year         = {2023}
}