incQuBE

| project staff | description | publications |

Within a cooperation with Star-lab (University of Genova, Italy), the search-based QBF solver QuBE7 has been extended to support assumptions and incremental solving, resulting into incQuBE. This extension includes a modification in the conflict analysis and learning procedure for correctly dealing with assumptions. Moreover, it supports don't touch literals, that is a partial preprocessing approach for simplifying a circuit without removing the output lines. This feature is used when coupled with a bounded model checker, to the purpose of reducing the size of the transition relations.