org.kahina.logic.sat.io.minisat

Class MiniSAT

java.lang.Object

org.kahina.logic.sat.io.minisat.MiniSAT

public class MiniSAT
extends java.lang.Object

Field Summary

Fields

Modifier and Type	Field and Description
static int	FREEZE
static int	UNFREEZE

Constructor Summary

Constructors

Constructor and Description
MiniSAT()

Method Summary

Methods

Modifier and Type	Method and Description
static void	createFreezeFile(int[] freezeVariables, java.io.File freezeFile, int offsetID)
static java.util.List<java.lang.Integer>	findUnsatisfiableCore(MUCStatistics stat, MiniSATFiles files)
static CompleteAssignment	getCompleteModel()
static CompleteAssignment	getCompleteModel(java.io.File resultFile)
static java.util.List<java.lang.Integer>	getImpliedUnits(CnfSatInstance instance, java.util.List<java.lang.Integer> setVars)
static java.util.List<java.lang.Integer>	getLearnedUnitClauses(java.io.File unitFile)
static PartialAssignment	getPartialModel(java.io.File resultFile)
static java.util.List<java.lang.Integer>	getRelevantAssumptions(int[] freezeVariables, int offsetID)
static java.util.List<java.lang.Integer>	getRelevantAssumptions(int offsetID, java.io.File proofFile)
static java.util.Set<java.lang.Integer>	getResolutionVariables(java.io.File proofFile)
static java.util.List<java.lang.Integer>	getVarRelevanceOrdering(java.io.File proofFile)
static boolean	isSatisfiable(java.io.File cnfFile, java.io.File tmpResultFile)
static boolean	minisatFoundOnPath()
static void	solve(java.io.File inputFile, java.io.File resultFile, java.io.File freezeFile)
static void	solve(java.io.File inputFile, java.io.File proofFile, java.io.File resultFile, java.io.File freezeFile)
static boolean	solveAndDeriveUnits(java.io.File cnfFile, java.io.File tmpResultFile, java.io.File unitsFile) Solves a SAT instance and writes the learned unit clauses out into a file.
static boolean	solveWithRefutationVariables(CnfSatInstance instance, java.io.File proofFile, java.io.File resultFile)
static java.lang.Boolean	wasUnsatisfiable()
static boolean	wasUnsatisfiable(java.io.File resultFile)

Methods inherited from class java.lang.Object

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

Field Detail

UNFREEZE

public static final int UNFREEZE

See Also:

Constant Field Values

FREEZE

public static final int FREEZE

See Also:

Constant Field Values

Constructor Detail

MiniSAT

public MiniSAT()

Method Detail

minisatFoundOnPath

public static boolean minisatFoundOnPath()

isSatisfiable

public static boolean isSatisfiable(java.io.File cnfFile,
                    java.io.File tmpResultFile)
                             throws java.util.concurrent.TimeoutException,
                                    java.lang.InterruptedException,
                                    java.io.IOException,
                                    ResultNotRetrievableException

Throws:

java.util.concurrent.TimeoutException

java.lang.InterruptedException

java.io.IOException

ResultNotRetrievableException

solveAndDeriveUnits

public static boolean solveAndDeriveUnits(java.io.File cnfFile,
                          java.io.File tmpResultFile,
                          java.io.File unitsFile)
                                   throws java.util.concurrent.TimeoutException,
                                          java.lang.InterruptedException,
                                          java.io.IOException,
                                          ResultNotRetrievableException

Solves a SAT instance and writes the learned unit clauses out into a file. Requires a custom variant of MiniSAT to be installed!

Parameters:

cnfFile - the SAT instance file (in DIMACS CNF format)

tmpResultFile - the temporary file in which the result is to be stored

unitsFile - the file where to store the units

Returns:

whether the SAT instance was satisfiable or not; units are written to unitsFile

Throws:

java.util.concurrent.TimeoutException

java.lang.InterruptedException

java.io.IOException

ResultNotRetrievableException

getImpliedUnits

public static java.util.List<java.lang.Integer> getImpliedUnits(CnfSatInstance instance,
                                                java.util.List<java.lang.Integer> setVars)
                                                         throws ResultNotRetrievableException

Throws:

ResultNotRetrievableException

solveWithRefutationVariables

public static boolean solveWithRefutationVariables(CnfSatInstance instance,
                                   java.io.File proofFile,
                                   java.io.File resultFile)
                                            throws java.util.concurrent.TimeoutException,
                                                   java.lang.InterruptedException,
                                                   java.io.IOException,
                                                   ResultNotRetrievableException

Throws:

java.util.concurrent.TimeoutException

java.lang.InterruptedException

java.io.IOException

ResultNotRetrievableException

findUnsatisfiableCore

public static java.util.List<java.lang.Integer> findUnsatisfiableCore(MUCStatistics stat,
                                                      MiniSATFiles files)
                                                               throws java.util.concurrent.TimeoutException,
                                                                      java.lang.InterruptedException,
                                                                      ResultNotRetrievableException

Throws:

java.util.concurrent.TimeoutException

java.lang.InterruptedException

ResultNotRetrievableException

solve

public static void solve(java.io.File inputFile,
         java.io.File resultFile,
         java.io.File freezeFile)
                  throws java.util.concurrent.TimeoutException

Throws:

java.util.concurrent.TimeoutException

solve

public static void solve(java.io.File inputFile,
         java.io.File proofFile,
         java.io.File resultFile,
         java.io.File freezeFile)
                  throws java.util.concurrent.TimeoutException

Throws:

java.util.concurrent.TimeoutException

wasUnsatisfiable

public static java.lang.Boolean wasUnsatisfiable()
                                          throws ResultNotRetrievableException

Throws:

ResultNotRetrievableException

getCompleteModel

public static CompleteAssignment getCompleteModel()

getCompleteModel

public static CompleteAssignment getCompleteModel(java.io.File resultFile)

getPartialModel

public static PartialAssignment getPartialModel(java.io.File resultFile)

wasUnsatisfiable

public static boolean wasUnsatisfiable(java.io.File resultFile)
                                throws ResultNotRetrievableException

Throws:

ResultNotRetrievableException

getResolutionVariables

public static java.util.Set<java.lang.Integer> getResolutionVariables(java.io.File proofFile)

getVarRelevanceOrdering

public static java.util.List<java.lang.Integer> getVarRelevanceOrdering(java.io.File proofFile)

getRelevantAssumptions

public static java.util.List<java.lang.Integer> getRelevantAssumptions(int[] freezeVariables,
                                                       int offsetID)

getLearnedUnitClauses

public static java.util.List<java.lang.Integer> getLearnedUnitClauses(java.io.File unitFile)

getRelevantAssumptions

public static java.util.List<java.lang.Integer> getRelevantAssumptions(int offsetID,
                                                       java.io.File proofFile)

createFreezeFile

public static void createFreezeFile(int[] freezeVariables,
                    java.io.File freezeFile,
                    int offsetID)