Links
Project source
- GIT repository with project sources. See the readme file for details on compilation.
- The sources for download, bundled with glucose sources (tgz, zip)
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.