# Project PCCompile

## Experimental data

Data sets used to carry out the experiments, generated with the modularity-based random SAT instances generator (see the paper by Jesús Giráldez-Cru and Jordi Levy).

## Presentations

The pdf of the presentation at KOCOON Workshop in Arras 16-19 December, 2019.

# Project description

## PCCompile

The main part of the project is a tool named pccompile. It can be used to check if a formula is propagation complete (PC) or unit refutation complete (URC). If a formula is not PC or URC, pccompile can compile the formula into an equivalent PC or URC formula.

The overall approach to compilation is iterative. We use SAT solver (the underlying solver is glucose) to check if a formula is PC or URC. If not, the SAT call provides an empowering clauses which witnesses the fact that the formula is not PC or URC. The clause is then added to the formula.

For compilation into a PC formula, two algorithms are available:

Incremental
The empowering clause found by a SAT call is processed (e.g. replaced by a prime subimplicate) and added to the formula.
Learning
We use a relation between semantic relation $$\varphi\land\alpha\models l$$ and a Horn formula which models this relation. Then, we use a learning algorithm by Angluin et al. (1992), in particular we use its variant described by Arias et al. (2015).

For a little bit more details, see the pdf of the presentation at KOCOON Workshop in Arras 16-19 December, 2019.