Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Unsatisfiability Proofs for Parity Reasoning in SAT
Speaker:Adrián Rebola Pardo
coming from:International Max Planck Research School for Computer Science - IMPRS
Speakers Bio:
Event Type:PhD Application Talk
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:Public Audience
Language:English
Date, Time and Location
Date:Monday, 26 October 2015
Time:11:20
Duration:90 Minutes
Location:Saarbrücken
Building:E1 4
Room:024
Abstract
The advent of increasingly efficient SAT solvers came with a remarkable

increase    in code complexity.   To  increase   the  reliability  of  solvers,
unsatisfiability witnesses in the form of proofs can be emitted for standard
CDCL-style solving. However, extensions of this system need to generate
ad hoc proof fragments that must be integrated in the full proof. When this
is not possible, users must decide whether to disable proof generation or
disable extensions such as inprocessing rules.
In this talk, I introduce two translations between a proof system for parity
constraints and the state-of-the-art DRAT proof system for CNF formulae.
These translations allow the generation of unsatisfiability proofs for SAT
solvers coupled with parity reasoning modules, which was an unsolved
problem.

Contact
Name(s):Andrea Ruffing
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Note:
Attachments, File(s):

Created by:Andrea Ruffing/MPI-INF, 10/23/2015 07:00 PMLast modified by:Uwe Brahm/MPII/DE, 11/24/2016 04:13 PM
  • Andrea Ruffing, 10/23/2015 07:01 PM -- Created document.