org.sat4j.tools

Class Backbone

java.lang.Object

org.sat4j.tools.Backbone

public class Backbone
extends Object

The aim of this class is to compute efficiently the literals implied by the set of constraints (also called backbone or unit implicates). The work has been done in the context of ANR BR4CP.

Author:

leberre

Method Summary

Methods

Modifier and Type	Method and Description
static IVecInt	compute(ISolver solver) Computes the backbone of a formula following the algorithm described in João Marques-Silva, Mikolás Janota, Inês Lynce: On Computing Backbones of Propositional Theories.
static IVecInt	compute(ISolver solver, int[] implicant)
static IVecInt	compute(ISolver solver, int[] implicant, IVecInt assumptions)
static IVecInt	compute(ISolver solver, IVecInt assumptions) Computes the backbone of a formula following the algorithm described in João Marques-Silva, Mikolás Janota, Inês Lynce: On Computing Backbones of Propositional Theories.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Detail

compute

public static IVecInt compute(ISolver solver)
                       throws TimeoutException

Computes the backbone of a formula following the algorithm described in João Marques-Silva, Mikolás Janota, Inês Lynce: On Computing Backbones of Propositional Theories. ECAI 2010: 15-20 We use Sat4j's ability to compute prime implicants instead of models to simplify the model at each step.

Parameters:

solver -

Returns:

Throws:

TimeoutException

compute

public static IVecInt compute(ISolver solver,
              IVecInt assumptions)
                       throws TimeoutException

Computes the backbone of a formula following the algorithm described in João Marques-Silva, Mikolás Janota, Inês Lynce: On Computing Backbones of Propositional Theories. ECAI 2010: 15-20 We use Sat4j's ability to compute prime implicants instead of models to simplify the model at each step.

Parameters:

solver -

assumptions -

Returns:

Throws:

TimeoutException

compute

public static IVecInt compute(ISolver solver,
              int[] implicant)
                       throws TimeoutException

Throws:

TimeoutException

compute

public static IVecInt compute(ISolver solver,
              int[] implicant,
              IVecInt assumptions)
                       throws TimeoutException

Throws:

TimeoutException