Package org.jacop.satwrapper

Class SatTranslation

java.lang.Object

org.jacop.satwrapper.SatTranslation

public class SatTranslation
extends java.lang.Object

SatTranslation defines SAT clauses for typical logical constraints

Version:

4.8

Field Summary

Fields

Modifier and Type	Field	Description
(package private) SatWrapper	clauses
boolean	debug
(package private) long	numberClauses
(package private) Store	store

Constructor Summary

Constructors

Constructor	Description
SatTranslation(Store store)

Method Summary

Modifier and Type	Method	Description
(package private) java.lang.String	clauseToString(int[] clause)
void	generate_allZero_reif(IntVar[] as, IntVar c)
void	generate_and(IntVar[] a, IntVar c)
void	generate_clause(IntVar[] a1, IntVar[] a2)
void	generate_clause_reif(IntVar[] a, IntVar[] b, IntVar r)
void	generate_eq(IntVar a, IntVar b)
void	generate_eq_reif(IntVar a, IntVar b, IntVar c)
void	generate_implication(IntVar a, IntVar b)
void	generate_implication_reif(IntVar a, IntVar b, IntVar c)
void	generate_le(IntVar a, IntVar b)
void	generate_le_reif(IntVar a, IntVar b, IntVar c)
void	generate_lt(IntVar a, IntVar b)
void	generate_lt_reif(IntVar a, IntVar b, IntVar c)
void	generate_neq_reif(IntVar a, IntVar b, IntVar c)
void	generate_not(IntVar a, IntVar b)
void	generate_or(IntVar[] a, IntVar c)
void	generate_xor(IntVar[] a, IntVar c)	To represent XOR function in CNF one needs to have 2^{n-1} clauses, where n is the size of your XOR function :( Our method cuts list to 3 or 2 element parts, generates XOR for them and composesd them back to the original XOR.
void	generate_xor(IntVar a, IntVar b, IntVar c)
void	generate_xor(IntVar a, IntVar b, IntVar c, IntVar d)
void	impose()
long	numberClauses()

Methods inherited from class java.lang.Object

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

Field Detail

debug

public boolean debug

clauses

SatWrapper clauses

store

Store store

numberClauses

long numberClauses

Constructor Detail

SatTranslation

public SatTranslation(Store store)

Method Detail

generate_clause

public void generate_clause(IntVar[] a1,
                            IntVar[] a2)

generate_clause_reif

public void generate_clause_reif(IntVar[] a,
                                 IntVar[] b,
                                 IntVar r)

generate_or

public void generate_or(IntVar[] a,
                        IntVar c)

generate_and

public void generate_and(IntVar[] a,
                         IntVar c)

generate_xor

public void generate_xor(IntVar[] a,
                         IntVar c)

To represent XOR function in CNF one needs to have 2^{n-1} clauses, where n is the size of your XOR function :( Our method cuts list to 3 or 2 element parts, generates XOR for them and composesd them back to the original XOR. Further improvements possible, if using 4-7 decompositions.

Parameters:

a - parameters to be xor'ed

c - result

generate_xor

public void generate_xor(IntVar a,
                         IntVar b,
                         IntVar c)

generate_xor

public void generate_xor(IntVar a,
                         IntVar b,
                         IntVar c,
                         IntVar d)

generate_eq

public void generate_eq(IntVar a,
                        IntVar b)

generate_le

public void generate_le(IntVar a,
                        IntVar b)

generate_lt

public void generate_lt(IntVar a,
                        IntVar b)

generate_eq_reif

public void generate_eq_reif(IntVar a,
                             IntVar b,
                             IntVar c)

generate_neq_reif

public void generate_neq_reif(IntVar a,
                              IntVar b,
                              IntVar c)

generate_le_reif

public void generate_le_reif(IntVar a,
                             IntVar b,
                             IntVar c)

generate_lt_reif

public void generate_lt_reif(IntVar a,
                             IntVar b,
                             IntVar c)

generate_not

public void generate_not(IntVar a,
                         IntVar b)

generate_implication

public void generate_implication(IntVar a,
                                 IntVar b)

generate_implication_reif

public void generate_implication_reif(IntVar a,
                                      IntVar b,
                                      IntVar c)

generate_allZero_reif

public void generate_allZero_reif(IntVar[] as,
                                  IntVar c)

impose

public void impose()

numberClauses

public long numberClauses()

clauseToString

java.lang.String clauseToString(int[] clause)