On finding minimum satisfying assignments

Alexey Ignatiev, Alessandro Previti, Joao Marques-Silva

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

1 Citation (Scopus)

Abstract

Given a Satisfiability Modulo Theories (SMT) formula, a minimum satisfying assignment (MSA) is a partial assignment of minimum size that ensures the formula is satisfied. Minimum satisfying assignments find a number of practical applications that include software and hardware verification, among others. Recent work proposes the use of branch-and-bound search for computing MSAs. This paper proposes a novel counterexample-guided implicit hitting set approach for computing one MSA. Experimental results show significant performance gains over existing approaches.

Original languageEnglish
Title of host publicationPrinciples and Practice of Constraint Programming
Subtitle of host publication22nd International Conference, CP 2016 Toulouse, France, September 5–9, 2016 Proceedings
EditorsMichel Rueher
Place of PublicationCham Switzerland
PublisherSpringer
Pages287-297
Number of pages11
ISBN (Electronic)9783319449531
ISBN (Print)9783319449524
DOIs
Publication statusPublished - 2016
Externally publishedYes
EventInternational Conference on Principles and Practice of Constraint Programming 2016 - Toulouse, France
Duration: 5 Sep 20169 Sep 2016
Conference number: 22d
http://cp2016.a4cp.org/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume9892
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Conference on Principles and Practice of Constraint Programming 2016
Abbreviated titleCP 2016
Country/TerritoryFrance
CityToulouse
Period5/09/169/09/16
Internet address

Cite this