<script type="text/javascript">
<!--
document.write('<div id="oa_widget"></div>');
document.write('<script type="text/javascript" src="https://www.openaire.eu/index.php?option=com_openaire&view=widget&format=raw&projectId=undefined&type=result"></script>');
-->
</script>

COPY SCRIPT

For further information contact us at helpdesk@openaire.eu

Experimental Repository for "Certified CNF Translations for Pseudo-Boolean Solving"

Name: Experimental Repository for "Certified CNF Translations for Pseudo-Boolean Solving"
Keywords: CNF encoding, PB to CNF translation, pseudo-Boolean, proof logging, certified translation, 0-1 integer linear program, certifying algorithms, cutting planes, PB solving

Research datakeyboard_double_arrow_right Dataset 06 Jun 2022 English Publisher:Zenodo

Authors: Gocht, Stephan; Martins, Ruben; Nordström, Jakob; Oertel, Andy;

doi: 10.5281/zenodo.6610581 , 10.5281/zenodo.6610582

Experimental Repository for "Certified CNF Translations for Pseudo-Boolean Solving"

- Summary
- Subjects
- Metrics

Abstract

Experimental repository Directory structure: `instances`: The instances used for the experiments sorted by their category. `output_data`: Raw output data from the experiments. `plots`: Plots generated from our experiments; also contain the plots used in the paper. `results`: Collected data on running time and proof size for the encodings. `source_code`: The source code of our `kissat_fork` to output VeriPB proofs, the proof checker `VeriPB` and our certifying PB-to-CNF translation library `VeritasPBLib` as used for our experiments.

Related Organizations

University of Copenhagen
Denmark
Lund University
Sweden
Carnegie Mellon University
United States

Keywords

CNF encoding, PB to CNF translation, pseudo-Boolean, proof logging, certified translation, 0-1 integer linear program, certifying algorithms, cutting planes, PB solving

Impact byBIP!

	citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	0
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average

Usage byUsageCounts

visibility	views	41
download	downloads	5

41
views
5
downloads
Powered by

Found an issue? Give us feedback

visibility

download

Average