A B C D E F G H I J L M N O P R S T U V W X

O

obj - Variable in class org.sat4j.minisat.core.Handle

ObjectiveFunction - Class in org.sat4j.opt

Abstraction for an Objective Function for Pseudo Boolean Optimization.

ObjectiveFunction(IVecInt, IVec<BigInteger>) - Constructor for class org.sat4j.opt.ObjectiveFunction

oldGetBacktrackLevel(int) - Method in class org.sat4j.minisat.constraints.pb.ConflictMap

oldIsAssertive(int) - Method in class org.sat4j.minisat.constraints.pb.ConflictMap

onCurrentDecisionLevelLiteral(int) - Method in interface org.sat4j.minisat.core.AssertingClauseGenerator

hook method called when a literal from the current decision lelvel is found.

onCurrentDecisionLevelLiteral(int) - Method in class org.sat4j.minisat.uip.DecisionUIP

onCurrentDecisionLevelLiteral(int) - Method in class org.sat4j.minisat.uip.FirstUIP

onFinish(ISolver, IVec<Var>) - Method in class org.sat4j.reader.csp.BinarySupportEncoding

onFinish(ISolver, IVec<Var>) - Method in class org.sat4j.reader.csp.DirectEncoding

onFinish(ISolver, IVec<Var>) - Method in interface org.sat4j.reader.csp.Encoding

onFinish(ISolver, IVec<Var>) - Method in class org.sat4j.reader.csp.GeneralizedSupportEncoding

onInit(ISolver, IVec<Var>) - Method in class org.sat4j.reader.csp.BinarySupportEncoding

onInit(ISolver, IVec<Var>) - Method in class org.sat4j.reader.csp.DirectEncoding

onInit(ISolver, IVec<Var>) - Method in interface org.sat4j.reader.csp.Encoding

onInit(ISolver, IVec<Var>) - Method in class org.sat4j.reader.csp.GeneralizedSupportEncoding

onNogood(ISolver, IVec<Var>, Map<Evaluable, Integer>) - Method in class org.sat4j.reader.csp.BinarySupportEncoding

onNogood(ISolver, IVec<Var>, Map<Evaluable, Integer>) - Method in class org.sat4j.reader.csp.DirectEncoding

onNogood(ISolver, IVec<Var>, Map<Evaluable, Integer>) - Method in interface org.sat4j.reader.csp.Encoding

onNogood(ISolver, IVec<Var>, Map<Evaluable, Integer>) - Method in class org.sat4j.reader.csp.GeneralizedSupportEncoding

onRestart() - Method in interface org.sat4j.minisat.core.RestartStrategy

Hook method called when a restart occurs (once the solver has backtracked to top decision level).

onRestart() - Method in class org.sat4j.minisat.restarts.ArminRestarts

onRestart() - Method in class org.sat4j.minisat.restarts.LubyRestarts

onRestart() - Method in class org.sat4j.minisat.restarts.MiniSATRestarts

onSupport(ISolver, IVec<Var>, Map<Evaluable, Integer>) - Method in class org.sat4j.reader.csp.BinarySupportEncoding

onSupport(ISolver, IVec<Var>, Map<Evaluable, Integer>) - Method in class org.sat4j.reader.csp.DirectEncoding

onSupport(ISolver, IVec<Var>, Map<Evaluable, Integer>) - Method in interface org.sat4j.reader.csp.Encoding

onSupport(ISolver, IVec<Var>, Map<Evaluable, Integer>) - Method in class org.sat4j.reader.csp.GeneralizedSupportEncoding

OPBReader2005 - Class in org.sat4j.reader

"Official" reader for the Pseudo Boolean evaluation 2005.

OPBReader2005(ISolver) - Constructor for class org.sat4j.reader.OPBReader2005

OPBReader2006 - Class in org.sat4j.reader

Reader complying to the PB06 input format.

OPBReader2006(ISolver) - Constructor for class org.sat4j.reader.OPBReader2006

OPBReader2007 - Class in org.sat4j.reader

OPBReader2007(ISolver) - Constructor for class org.sat4j.reader.OPBReader2007

OR - Static variable in class org.sat4j.reader.ExtendedDimacsReader

OR - Static variable in class org.sat4j.tools.ExtendedDimacsArrayReader

OR - Static variable in class org.sat4j.tools.ExtendedDimacsArrayToDimacsConverter

or(int, IVecInt) - Method in class org.sat4j.tools.GateTranslator

translate y <=> x1 \/ x2 \/ ... \/ xn into clauses.

org.sat4j - package org.sat4j

Contain a command line launcher for the SAT solvers.

org.sat4j.core - package org.sat4j.core

Implementation of the data structures available in org.sat4j.specs.

org.sat4j.minisat - package org.sat4j.minisat

Implementation of the MiniSAT specification in Java.

org.sat4j.minisat.constraints - package org.sat4j.minisat.constraints

Implementations of various constraints for MiniSAT.

org.sat4j.minisat.constraints.card - package org.sat4j.minisat.constraints.card

Implementations of cardinality contraints.

org.sat4j.minisat.constraints.cnf - package org.sat4j.minisat.constraints.cnf

Implementations of clausal contraints.

org.sat4j.minisat.constraints.pb - package org.sat4j.minisat.constraints.pb

Implementations of pseudo boolean contraints.

org.sat4j.minisat.core - package org.sat4j.minisat.core

Implementation of the MiniSAT solver skeleton.

org.sat4j.minisat.learning - package org.sat4j.minisat.learning

Various learning strategies.

org.sat4j.minisat.orders - package org.sat4j.minisat.orders

Various heuristics to select the next variable to branch on.

org.sat4j.minisat.restarts - package org.sat4j.minisat.restarts

org.sat4j.minisat.uip - package org.sat4j.minisat.uip

Various ways to compute an asserting clause (containing one Unique Implication Point).

org.sat4j.opt - package org.sat4j.opt

Built-in optimization framework.

org.sat4j.reader - package org.sat4j.reader

Some utility classes to read problems from plain text files.

org.sat4j.reader.csp - package org.sat4j.reader.csp

Classes needed for CSP to SAT translation.

org.sat4j.specs - package org.sat4j.specs

Those classes are intented for users dealing with SAT solvers as blackboxes.

org.sat4j.tools - package org.sat4j.tools

Tools to be used on top of an ISolver.

OriginalWLClause - Class in org.sat4j.minisat.constraints.cnf

OriginalWLClause(IVecInt, ILits) - Constructor for class org.sat4j.minisat.constraints.cnf.OriginalWLClause