Foundations of Automated Deduction and Satisflability, iDEAS TIN2004-04343
Luisa Bonet Carbonell · 2007
The project is about searching for new algorithms to show the satisflability of Boolean formulas. It is also about studying which proof systems are the most e‐cient to show their unsatisflability. Both directions have aplications in the flelds of circuit veriflcation, program veriflcation with model checking, automated deduction, and others. The satisflability problem is a particular case of the constraint satisfaction problem. The decisional form of both problems is NP-Complete. Constraint satisfaction problems appear in a large variety of practical situations, such as scheduling, temporal reasoning, machine vision, etc., so their study is important. We will study this topic both from the point of view of verifying satisflability, and from the point of view of showing the unsatisflability of constraints via proof systems. For that we will need to deflne proof systems that will work with domains more general than 0/1. This is a new and promising approach, because it brings to the fleld of constraint satisfaction problems the techniques from proof complexity and flnite model theory that had not been used before in this