SAT solvers are used in a wide variety of applications, including hardware and software verification, planning and combinatorial design. Given a propositional formula, standard SAT solvers are able to decide whether it is satisfiable or not. In the first case, a model is returned as a witness of satisfiability. The returned model is typically selected according to an internal heuristic and no control on the assignment is offered to the final user. This paper serves as a description for our tool minipref, a SAT solver extended to provide an optimal model with respect to a given preference over literals.
Minipref: A tool for preferences in SAT
Dodaro C.;
2020-01-01
Abstract
SAT solvers are used in a wide variety of applications, including hardware and software verification, planning and combinatorial design. Given a propositional formula, standard SAT solvers are able to decide whether it is satisfiable or not. In the first case, a model is returned as a witness of satisfiability. The returned model is typically selected according to an internal heuristic and no control on the assignment is offered to the final user. This paper serves as a description for our tool minipref, a SAT solver extended to provide an optimal model with respect to a given preference over literals.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
