On Solving ExactlyOneSAT In this paper, we aim at studying the ExactlyOneSAT problem (in short EOSAT). This problem consists in deciding whether a given CNF formula admits a model so that each clause has exactly one satisfied literal. The contribution of this work is twofold. Firstly, we introduce a tractable class in EOSAT, which is defined by a property that has to be satisfied by combinations of clauses. This class can be seen as a counterpart of tractable classes in the maximum independent set problem. Secondly, we propose graphbased approaches for reducing the number of variables and clauses of EOSAT instances, which consequently allow for reducing the search space. We provide an experimental study for evaluating these approach by showing its interest in the context of the graph coloring problem.

The SATCAS Method for Combinatorial Search with Applications to Best Matrices In this paper, we provide an overview of the SATCAS method that combines satisfiability checkers (SAT solvers) and computer algebra systems (CAS) to resolve combinatorial conjectures, and present new results visavis best matrices. The SATCAS method is a variant of the Davisunicode8211Putnamunicode8211Logemannunicode8211Loveland operatornameDPLL(T) architecture, where the T solver is replaced by a CAS. We describe how the SATCAS method has been previously used to resolve many open problems from graph theory, combinatorial design theory, and number theory, showing that the method has broad applications across a variety of fields. Additionally, we apply the method to construct the largest best matrices yet known and present new skew Hadamard matrices constructed from best matrices. We show the best matrix conjecture (that best matrices exist in all orders of the form r2r1) which was previously known to hold for rleq6 also holds for r7. We also confirmed the results of the exhaustive searches that have been previously completed for rleq6.