org.sat4j.specs

Interface UnitPropagationListener

All Known Subinterfaces:

ICDCL<D>, IPBCDCLSolver<D>

All Known Implementing Classes:

PBSolver, PBSolverCautious, PBSolverClause, PBSolverCP, PBSolverResCP, PBSolverResolution, PBSolverWithImpliedClause, Solver

public interface UnitPropagationListener

Interface providing the unit propagation capability. Note that this interface was in the package org.sat4j.minisat.core prior to release 2.3.4. It was moved here because of the dependency from UnitClauseProvider.

Author:

leberre

Method Summary

Modifier and Type	Method and Description
boolean	enqueue(int p) satisfies a literal
boolean	enqueue(int p, Constr from) satisfies a literal
void	unset(int p) Unset a unit clause.

Method Detail

enqueue

boolean enqueue(int p)

satisfies a literal

Parameters:

p - a literal

Returns:

true if the assignment looks possible, false if a conflict occurs.

enqueue

boolean enqueue(int p,
                Constr from)

satisfies a literal

Parameters:

p - a literal

from - a reason explaining why p should be satisfied.

Returns:

true if the assignment looks possible, false if a conflict occurs.

unset

void unset(int p)

Unset a unit clause. The effect of such method is to unset all truth values on the stack until the given literal is found (that literal included).

Parameters:

p -

Since:

2.1