See details on new features:
https://wiki.objectweb.org/sat4j/Wiki.jsp?page=WhatsNewInSAT4J1.6

Updated Javadoc:
www.sat4j.org/r16/doc/
-----------------------------------
http://www.sat4j.org/doc.php
sat4j software analysis
-----------------------------------

http://www.iiia.csic.es/~maxsat06/
MAXSAT competition

Dimacs CNF format
http://www.intellektik.informatik.tu-darmstadt.de/SATLIB/benchm.html


http://www.satlive.org/

@article{10.1109/CVPR.2005.515,
author = {Ya Zhang and Hongyuan Zha and Chao-Hisen Chu and Xiang Ji},
title = {Protein Interaction Inference as a MAX-SAT Problem},
journal = {cvprw},
volume = {0},
year = {2005},
issn = {1063-6919},
pages = {146},
doi = {http://doi.ieeecomputersociety.org/10.1109/CVPR.2005.515},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}

 	 	 	
			  	Artificial intelligence methods and tools for systems biology
				Dubitzky W., Azuaje F., Dubitzky W.,  Springer-Verlag New York, Inc., Secaucus, NJ, 2004. 221 pp. Type: Book
				Systems biology, a new and promising field of science that has many applications in different disciplines, is the topic of this book. It deals particularly with information and knowledge in an intelligent way. The book contains a collection of...
					Nov 28 2005 	 
								
								  	Configuration landscape analysis and backbone guided local search: part I: satisfiability and maximum satisfiability
									Zhang W.  Artificial Intelligence 158(1): 1-26, 2004. Type: Article
									This paper discusses the well-known nondeterministic polynomial time (NP) complete combinatorial and decision problems: the Boolean satisfiability (SAT) and the maximum satisfiability (Max-SAT = k-SAT) set of clauses of some...
										Feb 9 2005 	 
												

CS 289, Fall 2004, Stuart Russell
Reading List for Knowledge Representation and Reasoning


================
Medic: SAT-compilation of planning problems

The Medic planner encodes a planning problem as a propositional logic (CNF) formula, finds a satisfying truth assignment for that formula, and then translates the assignment into a plan which solves the original planning problem. The Medic system is described in the IJCAI '97 paper Tradeoffs in Automatic SAT-Compilation of Planning Problems.

Medic was the first tool for compiling a problem into SAT, or logical satisfiability. (The idea was due to Kautz and Selman, but this is the first implementation.) Such a transformation is valuable because much research has addressed making SAT compilation very fast. Today, solving problems by reducing them to SAT is a very common technique used in all fields of computer science.

medic.tar.gz, 2 Jan 2000. by Michael Ernst
----------------
@inproceedings{DBLP:conf/sat/LynceM06,
author    = {In{\^e}s Lynce and
Jo{\~a}o Marques-Silva},
title     = {SAT in Bioinformatics: Making the Case with Haplotype Inference.},
booktitle = {SAT},
year      = {2006},
pages     = {136-141},
ee        = {http://dx.doi.org/10.1007/11814948_16},
crossref  = {DBLP:conf/sat/2006},
bibsource = {DBLP, http://dblp.uni-trier.de}
}
@proceedings{DBLP:conf/sat/2006,
editor    = {Armin Biere and
Carla P. Gomes},
title     = {Theory and Applications of Satisfiability Testing - SAT
2006, 9th International Conference, Seattle, WA, USA, August
12-15, 2006, Proceedings},
booktitle = {SAT},
publisher = {Springer},
series    = {Lecture Notes in Computer Science},
volume    = {4121},
year      = {2006},
isbn      = {3-540-37206-7},
bibsource = {DBLP, http://dblp.uni-trier.de}
}